Theorem bj-ax9-2 32891

Description: Proof of ax-9 1999 from Tarski's FOL=, ax-8 1992 (specifically, ax8v1 1994 and ax8v2 1995) , df-cleq 2615 and ax-ext 2602. For a version not using ax-8 1992, see bj-ax9 32890. This shows that df-cleq 2615 is "too powerful". A possible definition is given by bj-df-cleq 32893. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-ax9-2	|- ( x = y -> ( z e. x -> z e. y ) )

Proof of Theorem bj-ax9-2

Dummy variables v u w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-ext 2602	. . . . 5 |- ( A. u ( u e. v <-> u e. w ) -> v = w )
2	1	df-cleq 2615	. . . 4 |- ( x = y <-> A. u ( u e. x <-> u e. y ) )
3	2	biimpi 206	. . 3 |- ( x = y -> A. u ( u e. x <-> u e. y ) )
4		biimp 205	. . 3 |- ( ( u e. x <-> u e. y ) -> ( u e. x -> u e. y ) )
5	3, 4	sylg 1750	. 2 |- ( x = y -> A. u ( u e. x -> u e. y ) )
6		ax8v2 1995	. . . . 5 |- ( z = u -> ( z e. x -> u e. x ) )
7	6	equcoms 1947	. . . 4 |- ( u = z -> ( z e. x -> u e. x ) )
8		ax8v1 1994	. . . 4 |- ( u = z -> ( u e. y -> z e. y ) )
9	7, 8	imim12d 81	. . 3 |- ( u = z -> ( ( u e. x -> u e. y ) -> ( z e. x -> z e. y ) ) )
10	9	spimvw 1927	. 2 |- ( A. u ( u e. x -> u e. y ) -> ( z e. x -> z e. y ) )
11	5, 10	syl 17	1 |- ( x = y -> ( z e. x -> z e. y ) )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by: (None)