Publish checked powerset foundation fact

1 files changed, 4 insertions, 0 deletions

diff --git a/data/felix-prelude.tex b/data/felix-prelude.tex
index cdf55d1..299e4d5 100644
--- a/data/felix-prelude.tex
+++ b/data/felix-prelude.tex
@@ -26,6 +26,10 @@
     For all $a,b,x$ we have $x \in \upair{a}{b}$ iff $x = a$ or $x = b$.
 \end{proposition}
 
+\begin{proposition}\label{pow_iff}
+    For all $A,B$ we have $B \in \pow{A}$ iff for all $x$ if $x \in B$, then $x \in A$.
+\end{proposition}
+
 \begin{proposition}\label{unions_iff}
     For all $A,x$ we have $x \in \unions{A}$ iff there exists $B \in A$ such that $x \in B$.
 \end{proposition}