Metamath Proof Explorer

Theorem sbal2OLD

Description: Obsolete version of sbal2 as of 23-Sep-2023. (Contributed by NM, 2-Jan-2002) Remove a distinct variable constraint. (Revised by Wolf Lammen, 24-Dec-2022) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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