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 | |- W = U. ( R1 " On ) |
|
| Assertion | wfaxext | |- A. x e. W A. y e. W ( A. z e. W ( z e. x <-> z e. y ) -> x = y ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wfax.1 | |- W = U. ( R1 " On ) |
|
| 2 | trwf | |- Tr U. ( R1 " On ) |
|
| 3 | treq | |- ( W = U. ( R1 " On ) -> ( Tr W <-> Tr U. ( R1 " On ) ) ) |
|
| 4 | 1 3 | ax-mp | |- ( Tr W <-> Tr U. ( R1 " On ) ) |
| 5 | 2 4 | mpbir | |- Tr W |
| 6 | traxext | |- ( Tr W -> A. x e. W A. y e. W ( A. z e. W ( z e. x <-> z e. y ) -> x = y ) ) |
|
| 7 | 5 6 | ax-mp | |- A. x e. W A. y e. W ( A. z e. W ( z e. x <-> z e. y ) -> x = y ) |