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

Metamath Proof Explorer

Theorem sbal2

Description: Move quantifier in and out of substitution. (Contributed by NM, 2-Jan-2002) Remove a distinct variable constraint. (Revised by Wolf Lammen, 24-Dec-2022) (Proof shortened by Wolf Lammen, 23-Sep-2023) Usage of this theorem is discouraged because it depends on ax-13 . Use sbal instead. (New usage is discouraged.)

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

Proof

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