Metamath Proof Explorer

Theorem wfaxext

Description: The class of well-founded sets models the axiom of Extensionality ax-ext . Part of Corollaray II.2.5 of Kunen2 p. 112. (Contributed by Eric Schmidt, 11-Sep-2025)

Ref Expression
Assertion wfaxext ⊢ ∀ x ∈ ⋃ R1 On ∀ y ∈ ⋃ R1 On ∀ z ∈ ⋃ R1 On z ∈ x ↔ z ∈ y → x = y

Proof

Step Hyp Ref Expression
1 trwf ⊢ Tr ⁡ ⋃ R1 On
2 traxext ⊢ Tr ⁡ ⋃ R1 On → ∀ x ∈ ⋃ R1 On ∀ y ∈ ⋃ R1 On ∀ z ∈ ⋃ R1 On z ∈ x ↔ z ∈ y → x = y
3 1 2 ax-mp ⊢ ∀ x ∈ ⋃ R1 On ∀ y ∈ ⋃ R1 On ∀ z ∈ ⋃ R1 On z ∈ x ↔ z ∈ y → x = y