Theorem 2sb5ndVD 31949

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 31585) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2sb5nd 31572 is 2sb5ndVD 31949 without virtual deductions and was automatically derived from 2sb5ndVD 31949. (Contributed by Alan Sare, 30-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	|- ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( ( x = u /\ y = v ) /\ ph ) )
2:1:	|- ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. y ( ( x = u /\ y = v ) /\ ph ) )
3::	|- ( [ v / y ] ph -> A. y [ v / y ] ph )
4:3:	|- [ u / x ] ( [ v / y ] ph -> A. y [ v / y ] ph )
5:4:	|- ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph )
6::	|- (. -. A. x x = y ->. -. A. x x = y ).
7::	|- ( A. y y = x -> A. x x = y )
8:7:	|- ( -. A. x x = y -> -. A. y y = x )
9:6,8:	|- (. -. A. x x = y ->. -. A. y y = x ).
10:9:	|- ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph )
11:5,10:	|- ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph )
12:11:	|- ( -. A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
13::	|- ( [ u / x ] [ v / y ] ph -> A. x [ u / x ] [ v / y ] ph )
14::	|- (. A. x x = y ->. A. x x = y ).
15:14:	|- (. A. x x = y ->. ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
16:13,15:	|- (. A. x x = y ->. ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
17:16:	|- ( A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
19:12,17:	|- ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph )
20:19:	|- ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
21:2,20:	|- ( E. y ( ( x = u /\ y = v ) /\ ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
22:21:	|- ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) <-> E. x ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
23:13:	|- ( E. x ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
24:22,23:	|- ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
240:24:	|- ( ( E. x E. y ( x = u /\ y = v ) /\ ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ) <-> ( E. x E. y ( x = u /\ y = v ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
241::	|- ( ( E. x E. y ( x = u /\ y = v ) /\ ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ) <-> ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
242:241,240:	|- ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. x E. y ( x = u /\ y = v ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
243::	|- ( ( E. x E. y ( x = u /\ y = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) ) <-> ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. x E. y ( x = u /\ y = v ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) ) )
25:242,243:	|- ( E. x E. y ( x = u /\ y = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
26::	|- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )
qed:25,26:	|- ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )

Assertion

Ref	Expression
2sb5ndVD	|- ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )

Distinct variable groups:   x, u   y, u   x, v   y, v

Allowed substitution hints:   ph( x, y, v, u)

Proof of Theorem 2sb5ndVD

Step	Hyp	Ref	Expression
1		ax6e2ndeq 31571	. 2 |- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )
2		anabs5 807	. . . 4 |- ( ( E. x E. y ( x = u /\ y = v ) /\ ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ) <-> ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
3		2pm13.193 31564	. . . . . . . . 9 |- ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( ( x = u /\ y = v ) /\ ph ) )
4	3	exbii 1635	. . . . . . . 8 |- ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. y ( ( x = u /\ y = v ) /\ ph ) )
5		hbs1 2148	. . . . . . . . . . . . 13 |- ( [ u / x ] [ v / y ] ph -> A. x [ u / x ] [ v / y ] ph )
6		idn1 31590	. . . . . . . . . . . . . 14 |- (. A. x x = y ->. A. x x = y ).
7		axc11 2011	. . . . . . . . . . . . . 14 |- ( A. x x = y -> ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
8	6, 7	e1a 31652	. . . . . . . . . . . . 13 |- (. A. x x = y ->. ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
9		imim1 76	. . . . . . . . . . . . 13 |- ( ( [ u / x ] [ v / y ] ph -> A. x [ u / x ] [ v / y ] ph ) -> ( ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ) )
10	5, 8, 9	e01 31716	. . . . . . . . . . . 12 |- (. A. x x = y ->. ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
11	10	in1 31587	. . . . . . . . . . 11 |- ( A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
12		hbs1 2148	. . . . . . . . . . . . . . 15 |- ( [ v / y ] ph -> A. y [ v / y ] ph )
13	12	sbt 2124	. . . . . . . . . . . . . 14 |- [ u / x ] ( [ v / y ] ph -> A. y [ v / y ] ph )
14		sbi1 2091	. . . . . . . . . . . . . 14 |- ( [ u / x ] ( [ v / y ] ph -> A. y [ v / y ] ph ) -> ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph ) )
15	13, 14	e0a 31808	. . . . . . . . . . . . 13 |- ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph )
16		idn1 31590	. . . . . . . . . . . . . . 15 |- (. -. A. x x = y ->. -. A. x x = y ).
17		axc11n 2006	. . . . . . . . . . . . . . . 16 |- ( A. y y = x -> A. x x = y )
18	17	con3i 135	. . . . . . . . . . . . . . 15 |- ( -. A. x x = y -> -. A. y y = x )
19	16, 18	e1a 31652	. . . . . . . . . . . . . 14 |- (. -. A. x x = y ->. -. A. y y = x ).
20		sbal2 2180	. . . . . . . . . . . . . 14 |- ( -. A. y y = x -> ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) )
21	19, 20	e1a 31652	. . . . . . . . . . . . 13 |- (. -. A. x x = y ->. ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) ).
22		imbi2 324	. . . . . . . . . . . . . 14 |- ( ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) -> ( ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph ) <-> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ) )
23	22	biimpcd 224	. . . . . . . . . . . . 13 |- ( ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph ) -> ( ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ) )
24	15, 21, 23	e01 31716	. . . . . . . . . . . 12 |- (. -. A. x x = y ->. ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
25	24	in1 31587	. . . . . . . . . . 11 |- ( -. A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
26	11, 25	pm2.61i 164	. . . . . . . . . 10 |- ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph )
27	26	nfi 1597	. . . . . . . . 9 |- F/ y [ u / x ] [ v / y ] ph
28	27	19.41 1908	. . . . . . . 8 |- ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
29	4, 28	bitr3i 251	. . . . . . 7 |- ( E. y ( ( x = u /\ y = v ) /\ ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
30	29	exbii 1635	. . . . . 6 |- ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) <-> E. x ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
31	5	nfi 1597	. . . . . . 7 |- F/ x [ u / x ] [ v / y ] ph
32	31	19.41 1908	. . . . . 6 |- ( E. x ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
33	30, 32	bitr2i 250	. . . . 5 |- ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
34	33	anbi2i 694	. . . 4 |- ( ( E. x E. y ( x = u /\ y = v ) /\ ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ) <-> ( E. x E. y ( x = u /\ y = v ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
35	2, 34	bitr3i 251	. . 3 |- ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. x E. y ( x = u /\ y = v ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
36		pm5.32 636	. . 3 |- ( ( E. x E. y ( x = u /\ y = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) ) <-> ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. x E. y ( x = u /\ y = v ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) ) )
37	35, 36	mpbir 209	. 2 |- ( E. x E. y ( x = u /\ y = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
38	1, 37	sylbi 195	1 |- ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   A.wal 1368   = wceq 1370   E.wex 1587   [wsb 1702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-ne 2646  df-v 3073  df-vd1 31586

This theorem is referenced by: (None)