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

Metamath Proof Explorer

Theorem sbal1

Description: Check out sbal for a version not dependent on ax-13 . A theorem used in elimination of disjoint variable restriction on x and z by replacing it with a distinctor -. A. x x = z . (Contributed by NM, 15-May-1993) (Proof shortened by Wolf Lammen, 3-Oct-2018) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion sbal1 
|- ( -. A. x x = z -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )

Proof

Step Hyp Ref Expression
1 sb4b 
 |-  ( -. A. y y = z -> ( [ z / y ] A. x ph <-> A. y ( y = z -> A. x ph ) ) )
2 nfnae 
 |-  F/ y -. A. x x = z
3 nfeqf2 
 |-  ( -. A. x x = z -> F/ x y = z )
4 19.21t 
 |-  ( F/ x y = z -> ( A. x ( y = z -> ph ) <-> ( y = z -> A. x ph ) ) )
5 4 bicomd 
 |-  ( F/ x y = z -> ( ( y = z -> A. x ph ) <-> A. x ( y = z -> ph ) ) )
6 3 5 syl 
 |-  ( -. A. x x = z -> ( ( y = z -> A. x ph ) <-> A. x ( y = z -> ph ) ) )
7 2 6 albid 
 |-  ( -. A. x x = z -> ( A. y ( y = z -> A. x ph ) <-> A. y A. x ( y = z -> ph ) ) )
8 1 7 sylan9bbr 
 |-  ( ( -. A. x x = z /\ -. A. y y = z ) -> ( [ z / y ] A. x ph <-> A. y A. x ( y = z -> ph ) ) )
9 nfnae 
 |-  F/ x -. A. y y = z
10 sb4b 
 |-  ( -. A. y y = z -> ( [ z / y ] ph <-> A. y ( y = z -> ph ) ) )
11 9 10 albid 
 |-  ( -. A. y y = z -> ( A. x [ z / y ] ph <-> A. x A. y ( y = z -> ph ) ) )
12 alcom 
 |-  ( A. x A. y ( y = z -> ph ) <-> A. y A. x ( y = z -> ph ) )
13 11 12 bitrdi 
 |-  ( -. A. y y = z -> ( A. x [ z / y ] ph <-> A. y A. x ( y = z -> ph ) ) )
14 13 adantl 
 |-  ( ( -. A. x x = z /\ -. A. y y = z ) -> ( A. x [ z / y ] ph <-> A. y A. x ( y = z -> ph ) ) )
15 8 14 bitr4d 
 |-  ( ( -. A. x x = z /\ -. A. y y = z ) -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
16 15 ex 
 |-  ( -. A. x x = z -> ( -. A. y y = z -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) ) )
17 sbequ12 
 |-  ( y = z -> ( A. x ph <-> [ z / y ] A. x ph ) )
18 17 sps 
 |-  ( A. y y = z -> ( A. x ph <-> [ z / y ] A. x ph ) )
19 sbequ12 
 |-  ( y = z -> ( ph <-> [ z / y ] ph ) )
20 19 sps 
 |-  ( A. y y = z -> ( ph <-> [ z / y ] ph ) )
21 20 dral2 
 |-  ( A. y y = z -> ( A. x ph <-> A. x [ z / y ] ph ) )
22 18 21 bitr3d 
 |-  ( A. y y = z -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
23 16 22 pm2.61d2 
 |-  ( -. A. x x = z -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )