Metamath Proof Explorer

Theorem wl-sbcom2d-lem1

Description: Lemma used to prove wl-sbcom2d . (Contributed by Wolf Lammen, 10-Aug-2019) (New usage is discouraged.)

Ref Expression
Assertion wl-sbcom2d-lem1 
|- ( ( u = y /\ v = w ) -> ( -. A. x x = w -> ( [ u / x ] [ v / z ] ph <-> [ y / x ] [ w / z ] ph ) ) )

Proof

Step Hyp Ref Expression
1 nfna1 
 |-  F/ x -. A. x x = w
2 nfeqf2 
 |-  ( -. A. x x = w -> F/ x v = w )
3 1 2 nfan1 
 |-  F/ x ( -. A. x x = w /\ v = w )
4 sbequ 
 |-  ( v = w -> ( [ v / z ] ph <-> [ w / z ] ph ) )
5 4 adantl 
 |-  ( ( -. A. x x = w /\ v = w ) -> ( [ v / z ] ph <-> [ w / z ] ph ) )
6 3 5 sbbid 
 |-  ( ( -. A. x x = w /\ v = w ) -> ( [ u / x ] [ v / z ] ph <-> [ u / x ] [ w / z ] ph ) )
7 6 ancoms 
 |-  ( ( v = w /\ -. A. x x = w ) -> ( [ u / x ] [ v / z ] ph <-> [ u / x ] [ w / z ] ph ) )
8 sbequ 
 |-  ( u = y -> ( [ u / x ] [ w / z ] ph <-> [ y / x ] [ w / z ] ph ) )
9 7 8 sylan9bbr 
 |-  ( ( u = y /\ ( v = w /\ -. A. x x = w ) ) -> ( [ u / x ] [ v / z ] ph <-> [ y / x ] [ w / z ] ph ) )
10 9 expr 
 |-  ( ( u = y /\ v = w ) -> ( -. A. x x = w -> ( [ u / x ] [ v / z ] ph <-> [ y / x ] [ w / z ] ph ) ) )