Metamath Proof Explorer

Theorem wl-2sb6d

Description: Version of 2sb6 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019)

Ref Expression
Hypotheses wl-2sb6d.1 
|- ( ph -> -. A. y y = x )
wl-2sb6d.2 
|- ( ph -> -. A. y y = w )
wl-2sb6d.3 
|- ( ph -> -. A. y y = z )
wl-2sb6d.4 
|- ( ph -> -. A. x x = z )
Assertion wl-2sb6d 
|- ( ph -> ( [ z / x ] [ w / y ] ps <-> A. x A. y ( ( x = z /\ y = w ) -> ps ) ) )

Proof

Step Hyp Ref Expression
1 wl-2sb6d.1 
 |-  ( ph -> -. A. y y = x )
2 wl-2sb6d.2 
 |-  ( ph -> -. A. y y = w )
3 wl-2sb6d.3 
 |-  ( ph -> -. A. y y = z )
4 wl-2sb6d.4 
 |-  ( ph -> -. A. x x = z )
5 1 3 jca 
 |-  ( ph -> ( -. A. y y = x /\ -. A. y y = z ) )
6 sb4b 
 |-  ( -. A. x x = z -> ( [ z / x ] [ w / y ] ps <-> A. x ( x = z -> [ w / y ] ps ) ) )
7 nfnae 
 |-  F/ x -. A. y y = w
8 wl-nfnae1 
 |-  F/ x -. A. y y = x
9 nfnae 
 |-  F/ x -. A. y y = z
10 8 9 nfan 
 |-  F/ x ( -. A. y y = x /\ -. A. y y = z )
11 7 10 nfan 
 |-  F/ x ( -. A. y y = w /\ ( -. A. y y = x /\ -. A. y y = z ) )
12 sb4b 
 |-  ( -. A. y y = w -> ( [ w / y ] ps <-> A. y ( y = w -> ps ) ) )
13 12 imbi2d 
 |-  ( -. A. y y = w -> ( ( x = z -> [ w / y ] ps ) <-> ( x = z -> A. y ( y = w -> ps ) ) ) )
14 impexp 
 |-  ( ( ( x = z /\ y = w ) -> ps ) <-> ( x = z -> ( y = w -> ps ) ) )
15 14 albii 
 |-  ( A. y ( ( x = z /\ y = w ) -> ps ) <-> A. y ( x = z -> ( y = w -> ps ) ) )
16 nfeqf 
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x = z )
17 19.21t 
 |-  ( F/ y x = z -> ( A. y ( x = z -> ( y = w -> ps ) ) <-> ( x = z -> A. y ( y = w -> ps ) ) ) )
18 16 17 syl 
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> ( A. y ( x = z -> ( y = w -> ps ) ) <-> ( x = z -> A. y ( y = w -> ps ) ) ) )
19 15 18 bitr2id 
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> ( ( x = z -> A. y ( y = w -> ps ) ) <-> A. y ( ( x = z /\ y = w ) -> ps ) ) )
20 13 19 sylan9bb 
 |-  ( ( -. A. y y = w /\ ( -. A. y y = x /\ -. A. y y = z ) ) -> ( ( x = z -> [ w / y ] ps ) <-> A. y ( ( x = z /\ y = w ) -> ps ) ) )
21 11 20 albid 
 |-  ( ( -. A. y y = w /\ ( -. A. y y = x /\ -. A. y y = z ) ) -> ( A. x ( x = z -> [ w / y ] ps ) <-> A. x A. y ( ( x = z /\ y = w ) -> ps ) ) )
22 6 21 sylan9bb 
 |-  ( ( -. A. x x = z /\ ( -. A. y y = w /\ ( -. A. y y = x /\ -. A. y y = z ) ) ) -> ( [ z / x ] [ w / y ] ps <-> A. x A. y ( ( x = z /\ y = w ) -> ps ) ) )
23 4 2 5 22 syl12anc 
 |-  ( ph -> ( [ z / x ] [ w / y ] ps <-> A. x A. y ( ( x = z /\ y = w ) -> ps ) ) )