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	\|- A. x e. U. ( R1 " On ) A. y e. U. ( R1 " On ) ( A. z e. U. ( R1 " On ) ( z e. x <-> z e. y ) -> x = y )

Proof

Step	Hyp	Ref	Expression
1		trwf	\|- Tr U. ( R1 " On )
2		traxext	\|- ( Tr U. ( R1 " On ) -> A. x e. U. ( R1 " On ) A. y e. U. ( R1 " On ) ( A. z e. U. ( R1 " On ) ( z e. x <-> z e. y ) -> x = y ) )
3	1 2	ax-mp	\|- A. x e. U. ( R1 " On ) A. y e. U. ( R1 " On ) ( A. z e. U. ( R1 " On ) ( z e. x <-> z e. y ) -> x = y )

Step

Hyp

Ref

Expression

trwf

 |-  Tr U. ( R1 " On )

traxext

 |-  ( Tr U. ( R1 " On ) -> A. x e. U. ( R1 " On ) A. y e. U. ( R1 " On ) ( A. z e. U. ( R1 " On ) ( z e. x <-> z e. y ) -> x = y ) )

1 2

ax-mp

 |-  A. x e. U. ( R1 " On ) A. y e. U. ( R1 " On ) ( A. z e. U. ( R1 " On ) ( z e. x <-> z e. y ) -> x = y )