This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )