Theorem copsexg 3972

Description: Substitution of class A for ordered pair <.x , y >.. (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.)

Assertion

Ref	Expression
copsexg	|- (A = <.x , y >. -> (ph <-> E.xE.y(A = <.x , y >. /\ ph)))

Distinct variable groups:   x,A   y,A

Allowed substitution hints:   ph(x,y)

Proof of Theorem copsexg

Dummy variables z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2554	. . . 4 |- x e. _V
2		vex 2554	. . . 4 |- y e. _V
3	1, 2	eqvinop 3971	. . 3 |- (A = <.x , y >. <-> E.zE.w(A = <.z , w >. /\ <.z , w >. = <.x , y >.))
4		19.8a 1479	. . . . . . . . 9 |- (E.y( <.z , w >. = <.x , y >. /\ ph) -> E.xE.y( <.z , w >. = <.x , y >. /\ ph))
5	4	19.23bi 1480	. . . . . . . 8 |- (( <.z , w >. = <.x , y >. /\ ph) -> E.xE.y( <.z , w >. = <.x , y >. /\ ph))
6	5	ex 108	. . . . . . 7 |- ( <.z , w >. = <.x , y >. -> (ph -> E.xE.y( <.z , w >. = <.x , y >. /\ ph)))
7		vex 2554	. . . . . . . . 9 |- z e. _V
8		vex 2554	. . . . . . . . 9 |- w e. _V
9	7, 8	opth 3965	. . . . . . . 8 |- ( <.z , w >. = <.x , y >. <-> (z = x /\ w = y))
10	9	anbi1i 431	. . . . . . . . . 10 |- (( <.z , w >. = <.x , y >. /\ ph) <-> ((z = x /\ w = y) /\ ph))
11	10	2exbii 1494	. . . . . . . . 9 |- (E.xE.y( <.z , w >. = <.x , y >. /\ ph) <-> E.xE.y((z = x /\ w = y) /\ ph))
12		nfe1 1382	. . . . . . . . . . 11 |- F/xE.x(z = x /\ E.y(w = y /\ ph))
13		dveeq2or 1694	. . . . . . . . . . . 12 |- (A.y y = x \/ F/y z = x)
14		nfae 1604	. . . . . . . . . . . . . . 15 |- F/yA.y y = x
15		anass 381	. . . . . . . . . . . . . . . 16 |- (((z = x /\ w = y) /\ ph) <-> (z = x /\ (w = y /\ ph)))
16		19.8a 1479	. . . . . . . . . . . . . . . . . 18 |- ((w = y /\ ph) -> E.y(w = y /\ ph))
17	16	a1i 9	. . . . . . . . . . . . . . . . 17 |- (A.y y = x -> ((w = y /\ ph) -> E.y(w = y /\ ph)))
18	17	anim2d 320	. . . . . . . . . . . . . . . 16 |- (A.y y = x -> ((z = x /\ (w = y /\ ph)) -> (z = x /\ E.y(w = y /\ ph))))
19	15, 18	syl5bi 141	. . . . . . . . . . . . . . 15 |- (A.y y = x -> (((z = x /\ w = y) /\ ph) -> (z = x /\ E.y(w = y /\ ph))))
20	14, 19	eximd 1500	. . . . . . . . . . . . . 14 |- (A.y y = x -> (E.y((z = x /\ w = y) /\ ph) -> E.y(z = x /\ E.y(w = y /\ ph))))
21		biidd 161	. . . . . . . . . . . . . . 15 |- (A.y y = x -> ((z = x /\ E.y(w = y /\ ph)) <-> (z = x /\ E.y(w = y /\ ph))))
22	21	drex1 1676	. . . . . . . . . . . . . 14 |- (A.y y = x -> (E.y(z = x /\ E.y(w = y /\ ph)) <-> E.x(z = x /\ E.y(w = y /\ ph))))
23	20, 22	sylibd 138	. . . . . . . . . . . . 13 |- (A.y y = x -> (E.y((z = x /\ w = y) /\ ph) -> E.x(z = x /\ E.y(w = y /\ ph))))
24	15	exbii 1493	. . . . . . . . . . . . . . 15 |- (E.y((z = x /\ w = y) /\ ph) <-> E.y(z = x /\ (w = y /\ ph)))
25		19.40 1519	. . . . . . . . . . . . . . . 16 |- (E.y(z = x /\ (w = y /\ ph)) -> (E.y z = x /\ E.y(w = y /\ ph)))
26		19.9t 1530	. . . . . . . . . . . . . . . . . 18 |- ( F/y z = x -> (E.y z = x <-> z = x))
27	26	biimpd 132	. . . . . . . . . . . . . . . . 17 |- ( F/y z = x -> (E.y z = x -> z = x))
28	27	anim1d 319	. . . . . . . . . . . . . . . 16 |- ( F/y z = x -> ((E.y z = x /\ E.y(w = y /\ ph)) -> (z = x /\ E.y(w = y /\ ph))))
29	25, 28	syl5 28	. . . . . . . . . . . . . . 15 |- ( F/y z = x -> (E.y(z = x /\ (w = y /\ ph)) -> (z = x /\ E.y(w = y /\ ph))))
30	24, 29	syl5bi 141	. . . . . . . . . . . . . 14 |- ( F/y z = x -> (E.y((z = x /\ w = y) /\ ph) -> (z = x /\ E.y(w = y /\ ph))))
31		19.8a 1479	. . . . . . . . . . . . . 14 |- ((z = x /\ E.y(w = y /\ ph)) -> E.x(z = x /\ E.y(w = y /\ ph)))
32	30, 31	syl6 29	. . . . . . . . . . . . 13 |- ( F/y z = x -> (E.y((z = x /\ w = y) /\ ph) -> E.x(z = x /\ E.y(w = y /\ ph))))
33	23, 32	jaoi 635	. . . . . . . . . . . 12 |- ((A.y y = x \/ F/y z = x) -> (E.y((z = x /\ w = y) /\ ph) -> E.x(z = x /\ E.y(w = y /\ ph))))
34	13, 33	ax-mp 7	. . . . . . . . . . 11 |- (E.y((z = x /\ w = y) /\ ph) -> E.x(z = x /\ E.y(w = y /\ ph)))
35	12, 34	exlimi 1482	. . . . . . . . . 10 |- (E.xE.y((z = x /\ w = y) /\ ph) -> E.x(z = x /\ E.y(w = y /\ ph)))
36		euequ1 1992	. . . . . . . . . . . . . 14 |- E!x x = z
37		equcom 1590	. . . . . . . . . . . . . . 15 |- (x = z <-> z = x)
38	37	eubii 1906	. . . . . . . . . . . . . 14 |- (E!x x = z <-> E!x z = x)
39	36, 38	mpbi 133	. . . . . . . . . . . . 13 |- E!x z = x
40		eupick 1976	. . . . . . . . . . . . 13 |- ((E!x z = x /\ E.x(z = x /\ E.y(w = y /\ ph))) -> (z = x -> E.y(w = y /\ ph)))
41	39, 40	mpan 400	. . . . . . . . . . . 12 |- (E.x(z = x /\ E.y(w = y /\ ph)) -> (z = x -> E.y(w = y /\ ph)))
42	41	com12 27	. . . . . . . . . . 11 |- (z = x -> (E.x(z = x /\ E.y(w = y /\ ph)) -> E.y(w = y /\ ph)))
43		euequ1 1992	. . . . . . . . . . . . . 14 |- E!y y = w
44		equcom 1590	. . . . . . . . . . . . . . 15 |- (y = w <-> w = y)
45	44	eubii 1906	. . . . . . . . . . . . . 14 |- (E!y y = w <-> E!y w = y)
46	43, 45	mpbi 133	. . . . . . . . . . . . 13 |- E!y w = y
47		eupick 1976	. . . . . . . . . . . . 13 |- ((E!y w = y /\ E.y(w = y /\ ph)) -> (w = y -> ph))
48	46, 47	mpan 400	. . . . . . . . . . . 12 |- (E.y(w = y /\ ph) -> (w = y -> ph))
49	48	com12 27	. . . . . . . . . . 11 |- (w = y -> (E.y(w = y /\ ph) -> ph))
50	42, 49	sylan9 389	. . . . . . . . . 10 |- ((z = x /\ w = y) -> (E.x(z = x /\ E.y(w = y /\ ph)) -> ph))
51	35, 50	syl5 28	. . . . . . . . 9 |- ((z = x /\ w = y) -> (E.xE.y((z = x /\ w = y) /\ ph) -> ph))
52	11, 51	syl5bi 141	. . . . . . . 8 |- ((z = x /\ w = y) -> (E.xE.y( <.z , w >. = <.x , y >. /\ ph) -> ph))
53	9, 52	sylbi 114	. . . . . . 7 |- ( <.z , w >. = <.x , y >. -> (E.xE.y( <.z , w >. = <.x , y >. /\ ph) -> ph))
54	6, 53	impbid 120	. . . . . 6 |- ( <.z , w >. = <.x , y >. -> (ph <-> E.xE.y( <.z , w >. = <.x , y >. /\ ph)))
55		eqeq1 2043	. . . . . . 7 |- (A = <.z , w >. -> (A = <.x , y >. <-> <.z , w >. = <.x , y >.))
56	55	anbi1d 438	. . . . . . . . 9 |- (A = <.z , w >. -> ((A = <.x , y >. /\ ph) <-> ( <.z , w >. = <.x , y >. /\ ph)))
57	56	2exbidv 1745	. . . . . . . 8 |- (A = <.z , w >. -> (E.xE.y(A = <.x , y >. /\ ph) <-> E.xE.y( <.z , w >. = <.x , y >. /\ ph)))
58	57	bibi2d 221	. . . . . . 7 |- (A = <.z , w >. -> ((ph <-> E.xE.y(A = <.x , y >. /\ ph)) <-> (ph <-> E.xE.y( <.z , w >. = <.x , y >. /\ ph))))
59	55, 58	imbi12d 223	. . . . . 6 |- (A = <.z , w >. -> ((A = <.x , y >. -> (ph <-> E.xE.y(A = <.x , y >. /\ ph))) <-> ( <.z , w >. = <.x , y >. -> (ph <-> E.xE.y( <.z , w >. = <.x , y >. /\ ph)))))
60	54, 59	mpbiri 157	. . . . 5 |- (A = <.z , w >. -> (A = <.x , y >. -> (ph <-> E.xE.y(A = <.x , y >. /\ ph))))
61	60	adantr 261	. . . 4 |- ((A = <.z , w >. /\ <.z , w >. = <.x , y >.) -> (A = <.x , y >. -> (ph <-> E.xE.y(A = <.x , y >. /\ ph))))
62	61	exlimivv 1773	. . 3 |- (E.zE.w(A = <.z , w >. /\ <.z , w >. = <.x , y >.) -> (A = <.x , y >. -> (ph <-> E.xE.y(A = <.x , y >. /\ ph))))
63	3, 62	sylbi 114	. 2 |- (A = <.x , y >. -> (A = <.x , y >. -> (ph <-> E.xE.y(A = <.x , y >. /\ ph))))
64	63	pm2.43i 43	1 |- (A = <.x , y >. -> (ph <-> E.xE.y(A = <.x , y >. /\ ph)))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   \/ wo 628  A.wal 1240   = wceq 1242   F/wnf 1346  E.wex 1378  E!weu 1897   <.cop 3370

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376

This theorem is referenced by:  copsex2t  3973  copsex2g  3974  opabid  3985  mosubopt  4348