Theorem zfcndext

Description: Axiom of Extensionality ax-ext , reproved from conditionless ZFC version and predicate calculus. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 15-Aug-2003) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	zfcndext	|- ( A. z ( z e. x <-> z e. y ) -> x = y )

Proof

Step	Hyp	Ref	Expression
1		axextnd	|- E. z ( ( z e. x <-> z e. y ) -> x = y )
2	1	19.36iv	|- ( A. z ( z e. x <-> z e. y ) -> x = y )