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 |