Description: The class of well-founded sets models the Axiom of Separation ax-sep . Actually, our statement is stronger, since it is an instance of Separation only when all quantifiers in ph are relativized to W . Part of Corollary II.2.5 of Kunen2 p. 112. (Contributed by Eric Schmidt, 29-Sep-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | wfax.1 | ||
Assertion | wfaxsep |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wfax.1 | ||
2 | ssclaxsep | ||
3 | pwwf | ||
4 | r1elssi | ||
5 | 3 4 | sylbi | |
6 | 1 | eleq2i | |
7 | 1 | sseq2i | |
8 | 5 6 7 | 3imtr4i | |
9 | 2 8 | mprg |