Theorem 2sb5ndVD 37301

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 36933) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2sb5nd 36921 is 2sb5ndVD 37301 without virtual deductions and was automatically derived from 2sb5ndVD 37301. (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 36920	. 2 |- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )
2		anabs5 817	. . . 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 36913	. . . . . . . . 9 |- ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( ( x = u /\ y = v ) /\ ph ) )
4	3	exbii 1717	. . . . . . . 8 |- ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. y ( ( x = u /\ y = v ) /\ ph ) )
5		hbs1 2264	. . . . . . . . . . . . 13 |- ( [ u / x ] [ v / y ] ph -> A. x [ u / x ] [ v / y ] ph )
6		idn1 36938	. . . . . . . . . . . . . 14 |- (. A. x x = y ->. A. x x = y ).
7		axc11 2147	. . . . . . . . . . . . . 14 |- ( A. x x = y -> ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
8	6, 7	e1a 37000	. . . . . . . . . . . . 13 |- (. A. x x = y ->. ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
9		imim1 79	. . . . . . . . . . . . 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 37064	. . . . . . . . . . . 12 |- (. A. x x = y ->. ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
11	10	in1 36935	. . . . . . . . . . 11 |- ( A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
12		hbs1 2264	. . . . . . . . . . . . . . 15 |- ( [ v / y ] ph -> A. y [ v / y ] ph )
13	12	sbt 2247	. . . . . . . . . . . . . 14 |- [ u / x ] ( [ v / y ] ph -> A. y [ v / y ] ph )
14		sbi1 2220	. . . . . . . . . . . . . 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 37153	. . . . . . . . . . . . 13 |- ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph )
16		idn1 36938	. . . . . . . . . . . . . . 15 |- (. -. A. x x = y ->. -. A. x x = y ).
17		axc11n 2142	. . . . . . . . . . . . . . . 16 |- ( A. y y = x -> A. x x = y )
18	17	con3i 141	. . . . . . . . . . . . . . 15 |- ( -. A. x x = y -> -. A. y y = x )
19	16, 18	e1a 37000	. . . . . . . . . . . . . 14 |- (. -. A. x x = y ->. -. A. y y = x ).
20		sbal2 2289	. . . . . . . . . . . . . 14 |- ( -. A. y y = x -> ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) )
21	19, 20	e1a 37000	. . . . . . . . . . . . 13 |- (. -. A. x x = y ->. ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) ).
22		imbi2 326	. . . . . . . . . . . . . 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 228	. . . . . . . . . . . . 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 37064	. . . . . . . . . . . 12 |- (. -. A. x x = y ->. ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
25	24	in1 36935	. . . . . . . . . . 11 |- ( -. A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
26	11, 25	pm2.61i 168	. . . . . . . . . 10 |- ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph )
27	26	nfi 1673	. . . . . . . . 9 |- F/ y [ u / x ] [ v / y ] ph
28	27	19.41 2050	. . . . . . . 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 255	. . . . . . 7 |- ( E. y ( ( x = u /\ y = v ) /\ ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
30	29	exbii 1717	. . . . . 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 1673	. . . . . . 7 |- F/ x [ u / x ] [ v / y ] ph
32	31	19.41 2050	. . . . . 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 254	. . . . 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 699	. . . 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 255	. . 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 641	. . 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 213	. 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 199	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 188   \/ wo 370   /\ wa 371   A.wal 1441   = wceq 1443   E.wex 1662   [wsb 1796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-ne 2623  df-v 3046  df-vd1 36934

This theorem is referenced by: (None)