Description: The class of well-founded sets models the axiom of Extensionality ax-ext . Part of Corollary II.2.5 of Kunen2 p. 112. (Contributed by Eric Schmidt, 11-Sep-2025) (Revised by Eric Schmidt, 29-Sep-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | wfax.1 | ||
Assertion | wfaxext |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wfax.1 | ||
2 | trwf | ||
3 | treq | ||
4 | 1 3 | ax-mp | |
5 | 2 4 | mpbir | |
6 | traxext | ||
7 | 5 6 | ax-mp |