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

Metamath Proof Explorer

Theorem ss-ax8

Description: A proof of ax-8 that does not rely on ax-8 . It employs df-ss to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 . Contrary to in-ax8 , this proof does not rely on df-cleq , therefore using fewer axioms . This method should not be applied to eliminate axiom dependencies. (Contributed by GG, 30-Aug-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ss-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 -> A. x ( x = w -> x e. t ) ) )
3 2 imp 
 |-  ( ( x = w /\ x e. t ) -> A. x ( x = w -> x e. t ) )
4 equsb3 
 |-  ( [ x / v ] v = w <-> x = w )
5 4 bicomi 
 |-  ( x = w <-> [ x / v ] v = w )
6 5 imbi1i 
 |-  ( ( x = w -> x e. t ) <-> ( [ x / v ] v = w -> x e. t ) )
7 6 albii 
 |-  ( A. x ( x = w -> x e. t ) <-> A. x ( [ x / v ] v = w -> x e. t ) )
8 df-clab 
 |-  ( x e. { v | v = w } <-> [ x / v ] v = w )
9 8 bicomi 
 |-  ( [ x / v ] v = w <-> x e. { v | v = w } )
10 9 imbi1i 
 |-  ( ( [ x / v ] v = w -> x e. t ) <-> ( x e. { v | v = w } -> x e. t ) )
11 10 albii 
 |-  ( A. x ( [ x / v ] v = w -> x e. t ) <-> A. x ( x e. { v | v = w } -> x e. t ) )
12 df-ss 
 |-  ( { v | v = w } C_ t <-> A. x ( x e. { v | v = w } -> x e. t ) )
13 df-ss 
 |-  ( { v | v = w } C_ t <-> A. y ( y e. { v | v = w } -> y e. t ) )
14 12 13 bitr3i 
 |-  ( A. x ( x e. { v | v = w } -> x e. t ) <-> A. y ( y e. { v | v = w } -> y e. t ) )
15 df-clab 
 |-  ( y e. { v | v = w } <-> [ y / v ] v = w )
16 15 imbi1i 
 |-  ( ( y e. { v | v = w } -> y e. t ) <-> ( [ y / v ] v = w -> y e. t ) )
17 16 albii 
 |-  ( A. y ( y e. { v | v = w } -> y e. t ) <-> A. y ( [ y / v ] v = w -> y e. t ) )
18 11 14 17 3bitri 
 |-  ( A. x ( [ x / v ] v = w -> x e. t ) <-> A. y ( [ y / v ] v = w -> y e. t ) )
19 equsb3 
 |-  ( [ y / v ] v = w <-> y = w )
20 19 imbi1i 
 |-  ( ( [ y / v ] v = w -> y e. t ) <-> ( y = w -> y e. t ) )
21 20 albii 
 |-  ( A. y ( [ y / v ] v = w -> y e. t ) <-> A. y ( y = w -> y e. t ) )
22 7 18 21 3bitri 
 |-  ( A. x ( x = w -> x e. t ) <-> A. y ( y = w -> y e. t ) )
23 22 biimpi 
 |-  ( A. x ( x = w -> x e. t ) -> A. y ( y = w -> y e. t ) )
24 sp 
 |-  ( A. y ( y = w -> y e. t ) -> ( y = w -> y e. t ) )
25 3 23 24 3syl 
 |-  ( ( x = w /\ x e. t ) -> ( y = w -> y e. t ) )
26 25 ex 
 |-  ( x = w -> ( x e. t -> ( y = w -> y e. t ) ) )
27 26 com23 
 |-  ( x = w -> ( y = w -> ( x e. t -> y e. t ) ) )
28 1 27 sylcom 
 |-  ( x = y -> ( x = w -> ( x e. t -> y e. t ) ) )
29 28 com12 
 |-  ( x = w -> ( x = y -> ( x e. t -> y e. t ) ) )
30 29 equcoms 
 |-  ( w = x -> ( x = y -> ( x e. t -> y e. t ) ) )
31 ax6ev 
 |-  E. w w = x
32 30 31 exlimiiv 
 |-  ( x = y -> ( x e. t -> y e. t ) )
33 ax9 
 |-  ( z = t -> ( x e. z -> x e. t ) )
34 33 equcoms 
 |-  ( t = z -> ( x e. z -> x e. t ) )
35 ax9 
 |-  ( t = z -> ( y e. t -> y e. z ) )
36 34 35 imim12d 
 |-  ( t = z -> ( ( x e. t -> y e. t ) -> ( x e. z -> y e. z ) ) )
37 32 36 syl5 
 |-  ( t = z -> ( x = y -> ( x e. z -> y e. z ) ) )
38 ax6ev 
 |-  E. t t = z
39 37 38 exlimiiv 
 |-  ( x = y -> ( x e. z -> y e. z ) )