Theorem ax9ALT

Description: Proof of ax-9 from Tarski's FOL and dfcleq . For a version not using ax-8 either, see eleq2w2 . This shows that dfcleq is too powerful to be used as a definition instead of df-cleq . Note that ax-ext is also a direct consequence of dfcleq (as an instance of its forward implication). (Contributed by BJ, 24-Jun-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ax9ALT	|- ( x = y -> ( z e. x -> z e. y ) )

Proof

Step	Hyp	Ref	Expression
1		dfcleq	|- ( x = y <-> A. t ( t e. x <-> t e. y ) )
2	1	biimpi	|- ( x = y -> A. t ( t e. x <-> t e. y ) )
3		biimp	|- ( ( t e. x <-> t e. y ) -> ( t e. x -> t e. y ) )
4	2 3	sylg	|- ( x = y -> A. t ( t e. x -> t e. y ) )
5		ax8	|- ( z = t -> ( z e. x -> t e. x ) )
6	5	equcoms	|- ( t = z -> ( z e. x -> t e. x ) )
7		ax8	|- ( t = z -> ( t e. y -> z e. y ) )
8	6 7	imim12d	|- ( t = z -> ( ( t e. x -> t e. y ) -> ( z e. x -> z e. y ) ) )
9	8	spimvw	|- ( A. t ( t e. x -> t e. y ) -> ( z e. x -> z e. y ) )
10	4 9	syl	|- ( x = y -> ( z e. x -> z e. y ) )