Theorem 2sb5ndVD 37370

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 37007) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2sb5nd 36997 is 2sb5ndVD 37370 without virtual deductions and was automatically derived from 2sb5ndVD 37370. (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 36996	. 2 |- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )
2		anabs5 826	. . . 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 36989	. . . . . . . . 9 |- ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( ( x = u /\ y = v ) /\ ph ) )
4	3	exbii 1726	. . . . . . . 8 |- ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. y ( ( x = u /\ y = v ) /\ ph ) )
5		hbs1 2285	. . . . . . . . . . . . 13 |- ( [ u / x ] [ v / y ] ph -> A. x [ u / x ] [ v / y ] ph )
6		idn1 37012	. . . . . . . . . . . . . 14 |- (. A. x x = y ->. A. x x = y ).
7		axc11 2163	. . . . . . . . . . . . . 14 |- ( A. x x = y -> ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
8	6, 7	e1a 37074	. . . . . . . . . . . . 13 |- (. A. x x = y ->. ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
9		imim1 78	. . . . . . . . . . . . 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 37138	. . . . . . . . . . . 12 |- (. A. x x = y ->. ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
11	10	in1 37009	. . . . . . . . . . 11 |- ( A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
12		hbs1 2285	. . . . . . . . . . . . . . 15 |- ( [ v / y ] ph -> A. y [ v / y ] ph )
13	12	sbt 2268	. . . . . . . . . . . . . 14 |- [ u / x ] ( [ v / y ] ph -> A. y [ v / y ] ph )
14		sbi1 2241	. . . . . . . . . . . . . 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 37222	. . . . . . . . . . . . 13 |- ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph )
16		idn1 37012	. . . . . . . . . . . . . . 15 |- (. -. A. x x = y ->. -. A. x x = y ).
17		axc11n 2157	. . . . . . . . . . . . . . . 16 |- ( A. y y = x -> A. x x = y )
18	17	con3i 142	. . . . . . . . . . . . . . 15 |- ( -. A. x x = y -> -. A. y y = x )
19	16, 18	e1a 37074	. . . . . . . . . . . . . 14 |- (. -. A. x x = y ->. -. A. y y = x ).
20		sbal2 2310	. . . . . . . . . . . . . 14 |- ( -. A. y y = x -> ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) )
21	19, 20	e1a 37074	. . . . . . . . . . . . 13 |- (. -. A. x x = y ->. ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) ).
22		imbi2 331	. . . . . . . . . . . . . 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 232	. . . . . . . . . . . . 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 37138	. . . . . . . . . . . 12 |- (. -. A. x x = y ->. ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
25	24	in1 37009	. . . . . . . . . . 11 |- ( -. A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
26	11, 25	pm2.61i 169	. . . . . . . . . 10 |- ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph )
27	26	nfi 1682	. . . . . . . . 9 |- F/ y [ u / x ] [ v / y ] ph
28	27	19.41 2070	. . . . . . . 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 259	. . . . . . 7 |- ( E. y ( ( x = u /\ y = v ) /\ ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
30	29	exbii 1726	. . . . . 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 1682	. . . . . . 7 |- F/ x [ u / x ] [ v / y ] ph
32	31	19.41 2070	. . . . . 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 258	. . . . 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 708	. . . 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 259	. . 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 648	. . 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 214	. 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 200	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 189   \/ wo 375   /\ wa 376   A.wal 1450   = wceq 1452   E.wex 1671   [wsb 1805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-ne 2643  df-v 3033  df-vd1 37008

This theorem is referenced by: (None)