Metamath Proof Explorer


Theorem wfaxext

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 𝑊 = ( 𝑅1 “ On )
Assertion wfaxext 𝑥𝑊𝑦𝑊 ( ∀ 𝑧𝑊 ( 𝑧𝑥𝑧𝑦 ) → 𝑥 = 𝑦 )

Proof

Step Hyp Ref Expression
1 wfax.1 𝑊 = ( 𝑅1 “ On )
2 trwf Tr ( 𝑅1 “ On )
3 treq ( 𝑊 = ( 𝑅1 “ On ) → ( Tr 𝑊 ↔ Tr ( 𝑅1 “ On ) ) )
4 1 3 ax-mp ( Tr 𝑊 ↔ Tr ( 𝑅1 “ On ) )
5 2 4 mpbir Tr 𝑊
6 traxext ( Tr 𝑊 → ∀ 𝑥𝑊𝑦𝑊 ( ∀ 𝑧𝑊 ( 𝑧𝑥𝑧𝑦 ) → 𝑥 = 𝑦 ) )
7 5 6 ax-mp 𝑥𝑊𝑦𝑊 ( ∀ 𝑧𝑊 ( 𝑧𝑥𝑧𝑦 ) → 𝑥 = 𝑦 )