Theorem wl-2sb6d 33341

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

Hypotheses

Ref	Expression
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

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

Proof of Theorem wl-2sb6d

Step	Hyp	Ref	Expression
1		wl-2sb6d.4	. 2 |- ( ph -> -. A. x x = z )
2		wl-2sb6d.2	. 2 |- ( ph -> -. A. y y = w )
3		wl-2sb6d.1	. . 3 |- ( ph -> -. A. y y = x )
4		wl-2sb6d.3	. . 3 |- ( ph -> -. A. y y = z )
5	3, 4	jca 554	. 2 |- ( ph -> ( -. A. y y = x /\ -. A. y y = z ) )
6		wl-sb6nae 33339	. . 3 |- ( -. A. x x = z -> ( [ z / x ] [ w / y ] ps <-> A. x ( x = z -> [ w / y ] ps ) ) )
7		nfnae 2318	. . . . 5 |- F/ x -. A. y y = w
8		wl-nfnae1 33316	. . . . . 6 |- F/ x -. A. y y = x
9		nfnae 2318	. . . . . 6 |- F/ x -. A. y y = z
10	8, 9	nfan 1828	. . . . 5 |- F/ x ( -. A. y y = x /\ -. A. y y = z )
11	7, 10	nfan 1828	. . . 4 |- F/ x ( -. A. y y = w /\ ( -. A. y y = x /\ -. A. y y = z ) )
12		wl-sb6nae 33339	. . . . . 6 |- ( -. A. y y = w -> ( [ w / y ] ps <-> A. y ( y = w -> ps ) ) )
13	12	imbi2d 330	. . . . 5 |- ( -. A. y y = w -> ( ( x = z -> [ w / y ] ps ) <-> ( x = z -> A. y ( y = w -> ps ) ) ) )
14		impexp 462	. . . . . . 7 |- ( ( ( x = z /\ y = w ) -> ps ) <-> ( x = z -> ( y = w -> ps ) ) )
15	14	albii 1747	. . . . . 6 |- ( A. y ( ( x = z /\ y = w ) -> ps ) <-> A. y ( x = z -> ( y = w -> ps ) ) )
16		nfeqf 2301	. . . . . . 7 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x = z )
17		19.21t 2073	. . . . . . 7 |- ( F/ y x = z -> ( A. y ( x = z -> ( y = w -> ps ) ) <-> ( x = z -> A. y ( y = w -> ps ) ) ) )
18	16, 17	syl 17	. . . . . 6 |- ( ( -. 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	syl5rbb 273	. . . . 5 |- ( ( -. 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 736	. . . 4 |- ( ( -. 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 2090	. . 3 |- ( ( -. 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 736	. 2 |- ( ( -. 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	1, 2, 5, 22	syl12anc 1324	1 |- ( ph -> ( [ z / x ] [ w / y ] ps <-> A. x A. y ( ( x = z /\ y = w ) -> ps ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   F/wnf 1708   [wsb 1880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881

This theorem is referenced by:  wl-sbcom2d-lem2  33343