Metamath Proof Explorer

Theorem wl-sbalnae

Description: A theorem used in elimination of disjoint variable restrictions by replacing them with distinctors. (Contributed by Wolf Lammen, 25-Jul-2019)

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