Metamath Proof Explorer

Theorem in-ax8

Description: A proof of ax-8 that does not rely on ax-8 . It employs df-in to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 . Since the nature of this result is unclear, usage of this theorem is discouraged, and this method should not be applied to eliminate axiom dependencies. (Contributed by GG, 1-Aug-2025) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ax7 
 |-  ( x = y -> ( x = w -> y = w ) )
2 ax12v2 
 |-  ( x = w -> ( ( x e. t /\ x e. t ) -> A. x ( x = w -> ( x e. t /\ x e. t ) ) ) )
3 2 imp 
 |-  ( ( x = w /\ ( x e. t /\ x e. t ) ) -> A. x ( x = w -> ( x e. t /\ x e. t ) ) )
4 sb6 
 |-  ( [ w / x ] ( x e. t /\ x e. t ) <-> A. x ( x = w -> ( x e. t /\ x e. t ) ) )
5 df-in 
 |-  ( t i^i t ) = { x | ( x e. t /\ x e. t ) }
6 df-in 
 |-  ( t i^i t ) = { y | ( y e. t /\ y e. t ) }
7 5 6 eqtr3i 
 |-  { x | ( x e. t /\ x e. t ) } = { y | ( y e. t /\ y e. t ) }
8 dfcleq 
 |-  ( { x | ( x e. t /\ x e. t ) } = { y | ( y e. t /\ y e. t ) } <-> A. w ( w e. { x | ( x e. t /\ x e. t ) } <-> w e. { y | ( y e. t /\ y e. t ) } ) )
9 7 8 mpbi 
 |-  A. w ( w e. { x | ( x e. t /\ x e. t ) } <-> w e. { y | ( y e. t /\ y e. t ) } )
10 9 spi 
 |-  ( w e. { x | ( x e. t /\ x e. t ) } <-> w e. { y | ( y e. t /\ y e. t ) } )
11 df-clab 
 |-  ( w e. { x | ( x e. t /\ x e. t ) } <-> [ w / x ] ( x e. t /\ x e. t ) )
12 df-clab 
 |-  ( w e. { y | ( y e. t /\ y e. t ) } <-> [ w / y ] ( y e. t /\ y e. t ) )
13 10 11 12 3bitr3i 
 |-  ( [ w / x ] ( x e. t /\ x e. t ) <-> [ w / y ] ( y e. t /\ y e. t ) )
14 4 13 bitr3i 
 |-  ( A. x ( x = w -> ( x e. t /\ x e. t ) ) <-> [ w / y ] ( y e. t /\ y e. t ) )
15 sb6 
 |-  ( [ w / y ] ( y e. t /\ y e. t ) <-> A. y ( y = w -> ( y e. t /\ y e. t ) ) )
16 14 15 sylbb 
 |-  ( A. x ( x = w -> ( x e. t /\ x e. t ) ) -> A. y ( y = w -> ( y e. t /\ y e. t ) ) )
17 sp 
 |-  ( A. y ( y = w -> ( y e. t /\ y e. t ) ) -> ( y = w -> ( y e. t /\ y e. t ) ) )
18 3 16 17 3syl 
 |-  ( ( x = w /\ ( x e. t /\ x e. t ) ) -> ( y = w -> ( y e. t /\ y e. t ) ) )
19 18 ex 
 |-  ( x = w -> ( ( x e. t /\ x e. t ) -> ( y = w -> ( y e. t /\ y e. t ) ) ) )
20 19 com23 
 |-  ( x = w -> ( y = w -> ( ( x e. t /\ x e. t ) -> ( y e. t /\ y e. t ) ) ) )
21 1 20 sylcom 
 |-  ( x = y -> ( x = w -> ( ( x e. t /\ x e. t ) -> ( y e. t /\ y e. t ) ) ) )
22 21 com12 
 |-  ( x = w -> ( x = y -> ( ( x e. t /\ x e. t ) -> ( y e. t /\ y e. t ) ) ) )
23 22 equcoms 
 |-  ( w = x -> ( x = y -> ( ( x e. t /\ x e. t ) -> ( y e. t /\ y e. t ) ) ) )
24 ax6ev 
 |-  E. w w = x
25 23 24 exlimiiv 
 |-  ( x = y -> ( ( x e. t /\ x e. t ) -> ( y e. t /\ y e. t ) ) )
26 pm4.24 
 |-  ( x e. t <-> ( x e. t /\ x e. t ) )
27 pm4.24 
 |-  ( y e. t <-> ( y e. t /\ y e. t ) )
28 25 26 27 3imtr4g 
 |-  ( x = y -> ( x e. t -> y e. t ) )
29 ax9 
 |-  ( z = t -> ( x e. z -> x e. t ) )
30 29 equcoms 
 |-  ( t = z -> ( x e. z -> x e. t ) )
31 ax9 
 |-  ( t = z -> ( y e. t -> y e. z ) )
32 30 31 imim12d 
 |-  ( t = z -> ( ( x e. t -> y e. t ) -> ( x e. z -> y e. z ) ) )
33 28 32 syl5 
 |-  ( t = z -> ( x = y -> ( x e. z -> y e. z ) ) )
34 ax6ev 
 |-  E. t t = z
35 33 34 exlimiiv 
 |-  ( x = y -> ( x e. z -> y e. z ) )