Theorem oprabid 5480

Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Although this theorem would be useful with a distinct variable constraint between x, y, and z, we use ax-bndl 1396 to eliminate that constraint. (Contributed by Mario Carneiro, 20-Mar-2013.)

Assertion

Ref	Expression
oprabid	|- ( <. <.x , y >. , z >. e. { <. <.x , y >. , z >. | ph } <-> ph)

Proof of Theorem oprabid

Dummy variables a r s t 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	opex 3957	. . 3 |- <.x , y >. e. _V
4		vex 2554	. . 3 |- z e. _V
5		opexg 3955	. . 3 |- (( <.x , y >. e. _V /\ z e. _V) -> <. <.x , y >. , z >. e. _V)
6	3, 4, 5	mp2an 402	. 2 |- <. <.x , y >. , z >. e. _V
7	3, 4	eqvinop 3971	. . . . 5 |- (w = <. <.x , y >. , z >. <-> E. aE. t(w = <. a , t >. /\ <. a , t >. = <. <.x , y >. , z >.))
8	7	biimpi 113	. . . 4 |- (w = <. <.x , y >. , z >. -> E. aE. t(w = <. a , t >. /\ <. a , t >. = <. <.x , y >. , z >.))
9		eqeq1 2043	. . . . . . . 8 |- (w = <. a , t >. -> (w = <. <.x , y >. , z >. <-> <. a , t >. = <. <.x , y >. , z >.))
10		vex 2554	. . . . . . . . 9 |- a e. _V
11		vex 2554	. . . . . . . . 9 |- t e. _V
12	10, 11	opth1 3964	. . . . . . . 8 |- ( <. a , t >. = <. <.x , y >. , z >. -> a = <.x , y >.)
13	9, 12	syl6bi 152	. . . . . . 7 |- (w = <. a , t >. -> (w = <. <.x , y >. , z >. -> a = <.x , y >.))
14	1, 2	eqvinop 3971	. . . . . . . . 9 |- ( a = <.x , y >. <-> E. rE. s( a = <. r , s >. /\ <. r , s >. = <.x , y >.))
15		opeq1 3540	. . . . . . . . . . . . 13 |- ( a = <. r , s >. -> <. a , t >. = <. <. r , s >. , t >.)
16	15	eqeq2d 2048	. . . . . . . . . . . 12 |- ( a = <. r , s >. -> (w = <. a , t >. <-> w = <. <. r , s >. , t >.))
17	1, 2, 4	otth2 3969	. . . . . . . . . . . . . . . . . . 19 |- ( <. <.x , y >. , z >. = <. <. r , s >. , t >. <-> (x = r /\ y = s /\ z = t))
18		df-3an 886	. . . . . . . . . . . . . . . . . . 19 |- ((x = r /\ y = s /\ z = t) <-> ((x = r /\ y = s) /\ z = t))
19	17, 18	bitri 173	. . . . . . . . . . . . . . . . . 18 |- ( <. <.x , y >. , z >. = <. <. r , s >. , t >. <-> ((x = r /\ y = s) /\ z = t))
20	19	anbi1i 431	. . . . . . . . . . . . . . . . 17 |- (( <. <.x , y >. , z >. = <. <. r , s >. , t >. /\ ph) <-> (((x = r /\ y = s) /\ z = t) /\ ph))
21		anass 381	. . . . . . . . . . . . . . . . 17 |- ((((x = r /\ y = s) /\ z = t) /\ ph) <-> ((x = r /\ y = s) /\ (z = t /\ ph)))
22		anass 381	. . . . . . . . . . . . . . . . 17 |- (((x = r /\ y = s) /\ (z = t /\ ph)) <-> (x = r /\ (y = s /\ (z = t /\ ph))))
23	20, 21, 22	3bitri 195	. . . . . . . . . . . . . . . 16 |- (( <. <.x , y >. , z >. = <. <. r , s >. , t >. /\ ph) <-> (x = r /\ (y = s /\ (z = t /\ ph))))
24	23	3exbii 1495	. . . . . . . . . . . . . . 15 |- (E.xE.yE.z( <. <.x , y >. , z >. = <. <. r , s >. , t >. /\ ph) <-> E.xE.yE.z(x = r /\ (y = s /\ (z = t /\ ph))))
25		oprabidlem 5479	. . . . . . . . . . . . . . . . . 18 |- (E.xE.z(x = r /\ (y = s /\ (z = t /\ ph))) -> E.x(x = r /\ E.z(y = s /\ (z = t /\ ph))))
26	25	eximi 1488	. . . . . . . . . . . . . . . . 17 |- (E.yE.xE.z(x = r /\ (y = s /\ (z = t /\ ph))) -> E.yE.x(x = r /\ E.z(y = s /\ (z = t /\ ph))))
27		excom 1551	. . . . . . . . . . . . . . . . 17 |- (E.xE.yE.z(x = r /\ (y = s /\ (z = t /\ ph))) <-> E.yE.xE.z(x = r /\ (y = s /\ (z = t /\ ph))))
28		excom 1551	. . . . . . . . . . . . . . . . 17 |- (E.xE.y(x = r /\ E.z(y = s /\ (z = t /\ ph))) <-> E.yE.x(x = r /\ E.z(y = s /\ (z = t /\ ph))))
29	26, 27, 28	3imtr4i 190	. . . . . . . . . . . . . . . 16 |- (E.xE.yE.z(x = r /\ (y = s /\ (z = t /\ ph))) -> E.xE.y(x = r /\ E.z(y = s /\ (z = t /\ ph))))
30		oprabidlem 5479	. . . . . . . . . . . . . . . 16 |- (E.xE.y(x = r /\ E.z(y = s /\ (z = t /\ ph))) -> E.x(x = r /\ E.yE.z(y = s /\ (z = t /\ ph))))
31		oprabidlem 5479	. . . . . . . . . . . . . . . . . 18 |- (E.yE.z(y = s /\ (z = t /\ ph)) -> E.y(y = s /\ E.z(z = t /\ ph)))
32	31	anim2i 324	. . . . . . . . . . . . . . . . 17 |- ((x = r /\ E.yE.z(y = s /\ (z = t /\ ph))) -> (x = r /\ E.y(y = s /\ E.z(z = t /\ ph))))
33	32	eximi 1488	. . . . . . . . . . . . . . . 16 |- (E.x(x = r /\ E.yE.z(y = s /\ (z = t /\ ph))) -> E.x(x = r /\ E.y(y = s /\ E.z(z = t /\ ph))))
34	29, 30, 33	3syl 17	. . . . . . . . . . . . . . 15 |- (E.xE.yE.z(x = r /\ (y = s /\ (z = t /\ ph))) -> E.x(x = r /\ E.y(y = s /\ E.z(z = t /\ ph))))
35	24, 34	sylbi 114	. . . . . . . . . . . . . 14 |- (E.xE.yE.z( <. <.x , y >. , z >. = <. <. r , s >. , t >. /\ ph) -> E.x(x = r /\ E.y(y = s /\ E.z(z = t /\ ph))))
36		euequ1 1992	. . . . . . . . . . . . . . . . . . 19 |- E!x x = r
37		eupick 1976	. . . . . . . . . . . . . . . . . . 19 |- ((E!x x = r /\ E.x(x = r /\ E.y(y = s /\ E.z(z = t /\ ph)))) -> (x = r -> E.y(y = s /\ E.z(z = t /\ ph))))
38	36, 37	mpan 400	. . . . . . . . . . . . . . . . . 18 |- (E.x(x = r /\ E.y(y = s /\ E.z(z = t /\ ph))) -> (x = r -> E.y(y = s /\ E.z(z = t /\ ph))))
39		euequ1 1992	. . . . . . . . . . . . . . . . . . . 20 |- E!y y = s
40		eupick 1976	. . . . . . . . . . . . . . . . . . . 20 |- ((E!y y = s /\ E.y(y = s /\ E.z(z = t /\ ph))) -> (y = s -> E.z(z = t /\ ph)))
41	39, 40	mpan 400	. . . . . . . . . . . . . . . . . . 19 |- (E.y(y = s /\ E.z(z = t /\ ph)) -> (y = s -> E.z(z = t /\ ph)))
42		euequ1 1992	. . . . . . . . . . . . . . . . . . . 20 |- E!z z = t
43		eupick 1976	. . . . . . . . . . . . . . . . . . . 20 |- ((E!z z = t /\ E.z(z = t /\ ph)) -> (z = t -> ph))
44	42, 43	mpan 400	. . . . . . . . . . . . . . . . . . 19 |- (E.z(z = t /\ ph) -> (z = t -> ph))
45	41, 44	syl6 29	. . . . . . . . . . . . . . . . . 18 |- (E.y(y = s /\ E.z(z = t /\ ph)) -> (y = s -> (z = t -> ph)))
46	38, 45	syl6 29	. . . . . . . . . . . . . . . . 17 |- (E.x(x = r /\ E.y(y = s /\ E.z(z = t /\ ph))) -> (x = r -> (y = s -> (z = t -> ph))))
47	46	3impd 1117	. . . . . . . . . . . . . . . 16 |- (E.x(x = r /\ E.y(y = s /\ E.z(z = t /\ ph))) -> ((x = r /\ y = s /\ z = t) -> ph))
48	17, 47	syl5bi 141	. . . . . . . . . . . . . . 15 |- (E.x(x = r /\ E.y(y = s /\ E.z(z = t /\ ph))) -> ( <. <.x , y >. , z >. = <. <. r , s >. , t >. -> ph))
49	48	com12 27	. . . . . . . . . . . . . 14 |- ( <. <.x , y >. , z >. = <. <. r , s >. , t >. -> (E.x(x = r /\ E.y(y = s /\ E.z(z = t /\ ph))) -> ph))
50	35, 49	syl5 28	. . . . . . . . . . . . 13 |- ( <. <.x , y >. , z >. = <. <. r , s >. , t >. -> (E.xE.yE.z( <. <.x , y >. , z >. = <. <. r , s >. , t >. /\ ph) -> ph))
51		eqeq1 2043	. . . . . . . . . . . . . . 15 |- (w = <. <. r , s >. , t >. -> (w = <. <.x , y >. , z >. <-> <. <. r , s >. , t >. = <. <.x , y >. , z >.))
52		eqcom 2039	. . . . . . . . . . . . . . 15 |- ( <. <. r , s >. , t >. = <. <.x , y >. , z >. <-> <. <.x , y >. , z >. = <. <. r , s >. , t >.)
53	51, 52	syl6bb 185	. . . . . . . . . . . . . 14 |- (w = <. <. r , s >. , t >. -> (w = <. <.x , y >. , z >. <-> <. <.x , y >. , z >. = <. <. r , s >. , t >.))
54	53	anbi1d 438	. . . . . . . . . . . . . . . 16 |- (w = <. <. r , s >. , t >. -> ((w = <. <.x , y >. , z >. /\ ph) <-> ( <. <.x , y >. , z >. = <. <. r , s >. , t >. /\ ph)))
55	54	3exbidv 1746	. . . . . . . . . . . . . . 15 |- (w = <. <. r , s >. , t >. -> (E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph) <-> E.xE.yE.z( <. <.x , y >. , z >. = <. <. r , s >. , t >. /\ ph)))
56	55	imbi1d 220	. . . . . . . . . . . . . 14 |- (w = <. <. r , s >. , t >. -> ((E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph) -> ph) <-> (E.xE.yE.z( <. <.x , y >. , z >. = <. <. r , s >. , t >. /\ ph) -> ph)))
57	53, 56	imbi12d 223	. . . . . . . . . . . . 13 |- (w = <. <. r , s >. , t >. -> ((w = <. <.x , y >. , z >. -> (E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph) -> ph)) <-> ( <. <.x , y >. , z >. = <. <. r , s >. , t >. -> (E.xE.yE.z( <. <.x , y >. , z >. = <. <. r , s >. , t >. /\ ph) -> ph))))
58	50, 57	mpbiri 157	. . . . . . . . . . . 12 |- (w = <. <. r , s >. , t >. -> (w = <. <.x , y >. , z >. -> (E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph) -> ph)))
59	16, 58	syl6bi 152	. . . . . . . . . . 11 |- ( a = <. r , s >. -> (w = <. a , t >. -> (w = <. <.x , y >. , z >. -> (E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph) -> ph))))
60	59	adantr 261	. . . . . . . . . 10 |- (( a = <. r , s >. /\ <. r , s >. = <.x , y >.) -> (w = <. a , t >. -> (w = <. <.x , y >. , z >. -> (E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph) -> ph))))
61	60	exlimivv 1773	. . . . . . . . 9 |- (E. rE. s( a = <. r , s >. /\ <. r , s >. = <.x , y >.) -> (w = <. a , t >. -> (w = <. <.x , y >. , z >. -> (E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph) -> ph))))
62	14, 61	sylbi 114	. . . . . . . 8 |- ( a = <.x , y >. -> (w = <. a , t >. -> (w = <. <.x , y >. , z >. -> (E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph) -> ph))))
63	62	com3l 75	. . . . . . 7 |- (w = <. a , t >. -> (w = <. <.x , y >. , z >. -> ( a = <.x , y >. -> (E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph) -> ph))))
64	13, 63	mpdd 36	. . . . . 6 |- (w = <. a , t >. -> (w = <. <.x , y >. , z >. -> (E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph) -> ph)))
65	64	adantr 261	. . . . 5 |- ((w = <. a , t >. /\ <. a , t >. = <. <.x , y >. , z >.) -> (w = <. <.x , y >. , z >. -> (E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph) -> ph)))
66	65	exlimivv 1773	. . . 4 |- (E. aE. t(w = <. a , t >. /\ <. a , t >. = <. <.x , y >. , z >.) -> (w = <. <.x , y >. , z >. -> (E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph) -> ph)))
67	8, 66	mpcom 32	. . 3 |- (w = <. <.x , y >. , z >. -> (E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph) -> ph))
68		19.8a 1479	. . . . 5 |- ((w = <. <.x , y >. , z >. /\ ph) -> E.z(w = <. <.x , y >. , z >. /\ ph))
69		19.8a 1479	. . . . 5 |- (E.z(w = <. <.x , y >. , z >. /\ ph) -> E.yE.z(w = <. <.x , y >. , z >. /\ ph))
70		19.8a 1479	. . . . 5 |- (E.yE.z(w = <. <.x , y >. , z >. /\ ph) -> E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph))
71	68, 69, 70	3syl 17	. . . 4 |- ((w = <. <.x , y >. , z >. /\ ph) -> E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph))
72	71	ex 108	. . 3 |- (w = <. <.x , y >. , z >. -> (ph -> E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph)))
73	67, 72	impbid 120	. 2 |- (w = <. <.x , y >. , z >. -> (E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph) <-> ph))
74		df-oprab 5459	. 2 |- { <. <.x , y >. , z >. | ph } = {w | E.xE.yE.z(w = <. <.x , y >. , z >. /\ ph) }
75	6, 73, 74	elab2 2684	1 |- ( <. <.x , y >. , z >. e. { <. <.x , y >. , z >. | ph } <-> ph)

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   /\ w3a 884   = wceq 1242  E.wex 1378   e. wcel 1390  E!weu 1897   _Vcvv 2551   <.cop 3370   {coprab 5456

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-in1 544  ax-in2 545  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  ax-setind 4220

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  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-ne 2203  df-ral 2305  df-v 2553  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-oprab 5459

This theorem is referenced by:  ssoprab2b  5504  ovid  5559  ovidig  5560  tposoprab  5836  xpcomco  6236