Theorem oprabid 5811

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 1487 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 2692	. . . 4 |- x e. _V
2		vex 2692	. . . 4 |- y e. _V
3	1, 2	opex 4159	. . 3 |- <. x , y >. e. _V
4		vex 2692	. . 3 |- z e. _V
5		opexg 4158	. . 3 |- ( ( <. x , y >. e. _V /\ z e. _V ) -> <. <. x , y >. , z >. e. _V )
6	3, 4, 5	mp2an 423	. 2 |- <. <. x , y >. , z >. e. _V
7	3, 4	eqvinop 4173	. . . . 5 |- ( w = <. <. x , y >. , z >. <-> E. a E. t ( w = <. a , t >. /\ <. a , t >. = <. <. x , y >. , z >. ) )
8	7	biimpi 119	. . . 4 |- ( w = <. <. x , y >. , z >. -> E. a E. t ( w = <. a , t >. /\ <. a , t >. = <. <. x , y >. , z >. ) )
9		eqeq1 2147	. . . . . . . 8 |- ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. <-> <. a , t >. = <. <. x , y >. , z >. ) )
10		vex 2692	. . . . . . . . 9 |- a e. _V
11		vex 2692	. . . . . . . . 9 |- t e. _V
12	10, 11	opth1 4166	. . . . . . . 8 |- ( <. a , t >. = <. <. x , y >. , z >. -> a = <. x , y >. )
13	9, 12	syl6bi 162	. . . . . . 7 |- ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> a = <. x , y >. ) )
14	1, 2	eqvinop 4173	. . . . . . . . 9 |- ( a = <. x , y >. <-> E. r E. s ( a = <. r , s >. /\ <. r , s >. = <. x , y >. ) )
15		opeq1 3713	. . . . . . . . . . . . 13 |- ( a = <. r , s >. -> <. a , t >. = <. <. r , s >. , t >. )
16	15	eqeq2d 2152	. . . . . . . . . . . 12 |- ( a = <. r , s >. -> ( w = <. a , t >. <-> w = <. <. r , s >. , t >. ) )
17	1, 2, 4	otth2 4171	. . . . . . . . . . . . . . . . . . 19 |- ( <. <. x , y >. , z >. = <. <. r , s >. , t >. <-> ( x = r /\ y = s /\ z = t ) )
18		df-3an 965	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = r /\ y = s /\ z = t ) <-> ( ( x = r /\ y = s ) /\ z = t ) )
19	17, 18	bitri 183	. . . . . . . . . . . . . . . . . 18 |- ( <. <. x , y >. , z >. = <. <. r , s >. , t >. <-> ( ( x = r /\ y = s ) /\ z = t ) )
20	19	anbi1i 454	. . . . . . . . . . . . . . . . 17 |- ( ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) <-> ( ( ( x = r /\ y = s ) /\ z = t ) /\ ph ) )
21		anass 399	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x = r /\ y = s ) /\ z = t ) /\ ph ) <-> ( ( x = r /\ y = s ) /\ ( z = t /\ ph ) ) )
22		anass 399	. . . . . . . . . . . . . . . . 17 |- ( ( ( x = r /\ y = s ) /\ ( z = t /\ ph ) ) <-> ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) )
23	20, 21, 22	3bitri 205	. . . . . . . . . . . . . . . 16 |- ( ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) <-> ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) )
24	23	3exbii 1587	. . . . . . . . . . . . . . 15 |- ( E. x E. y E. z ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) <-> E. x E. y E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) )
25		oprabidlem 5810	. . . . . . . . . . . . . . . . . 18 |- ( E. x E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) )
26	25	eximi 1580	. . . . . . . . . . . . . . . . 17 |- ( E. y E. x E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) -> E. y E. x ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) )
27		excom 1643	. . . . . . . . . . . . . . . . 17 |- ( E. x E. y E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) <-> E. y E. x E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) )
28		excom 1643	. . . . . . . . . . . . . . . . 17 |- ( E. x E. y ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) <-> E. y E. x ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) )
29	26, 27, 28	3imtr4i 200	. . . . . . . . . . . . . . . 16 |- ( E. x E. y E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) -> E. x E. y ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) )
30		oprabidlem 5810	. . . . . . . . . . . . . . . 16 |- ( E. x E. y ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) )
31		oprabidlem 5810	. . . . . . . . . . . . . . . . . 18 |- ( E. y E. z ( y = s /\ ( z = t /\ ph ) ) -> E. y ( y = s /\ E. z ( z = t /\ ph ) ) )
32	31	anim2i 340	. . . . . . . . . . . . . . . . 17 |- ( ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) -> ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) )
33	32	eximi 1580	. . . . . . . . . . . . . . . 16 |- ( E. x ( x = r /\ E. y E. 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. x E. y E. 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 120	. . . . . . . . . . . . . 14 |- ( E. x E. y E. z ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) -> E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) )
36		euequ1 2095	. . . . . . . . . . . . . . . . . . 19 |- E! x x = r
37		eupick 2079	. . . . . . . . . . . . . . . . . . 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 421	. . . . . . . . . . . . . . . . . 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 2095	. . . . . . . . . . . . . . . . . . . 20 |- E! y y = s
40		eupick 2079	. . . . . . . . . . . . . . . . . . . 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 421	. . . . . . . . . . . . . . . . . . 19 |- ( E. y ( y = s /\ E. z ( z = t /\ ph ) ) -> ( y = s -> E. z ( z = t /\ ph ) ) )
42		euequ1 2095	. . . . . . . . . . . . . . . . . . . 20 |- E! z z = t
43		eupick 2079	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E! z z = t /\ E. z ( z = t /\ ph ) ) -> ( z = t -> ph ) )
44	42, 43	mpan 421	. . . . . . . . . . . . . . . . . . 19 |- ( E. z ( z = t /\ ph ) -> ( z = t -> ph ) )
45	41, 44	syl6 33	. . . . . . . . . . . . . . . . . 18 |- ( E. y ( y = s /\ E. z ( z = t /\ ph ) ) -> ( y = s -> ( z = t -> ph ) ) )
46	38, 45	syl6 33	. . . . . . . . . . . . . . . . 17 |- ( E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( x = r -> ( y = s -> ( z = t -> ph ) ) ) )
47	46	3impd 1200	. . . . . . . . . . . . . . . 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 151	. . . . . . . . . . . . . . 15 |- ( E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( <. <. x , y >. , z >. = <. <. r , s >. , t >. -> ph ) )
49	48	com12 30	. . . . . . . . . . . . . 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 32	. . . . . . . . . . . . 13 |- ( <. <. x , y >. , z >. = <. <. r , s >. , t >. -> ( E. x E. y E. z ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) -> ph ) )
51		eqeq1 2147	. . . . . . . . . . . . . . 15 |- ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. <-> <. <. r , s >. , t >. = <. <. x , y >. , z >. ) )
52		eqcom 2142	. . . . . . . . . . . . . . 15 |- ( <. <. r , s >. , t >. = <. <. x , y >. , z >. <-> <. <. x , y >. , z >. = <. <. r , s >. , t >. )
53	51, 52	syl6bb 195	. . . . . . . . . . . . . 14 |- ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. <-> <. <. x , y >. , z >. = <. <. r , s >. , t >. ) )
54	53	anbi1d 461	. . . . . . . . . . . . . . . 16 |- ( w = <. <. r , s >. , t >. -> ( ( w = <. <. x , y >. , z >. /\ ph ) <-> ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) ) )
55	54	3exbidv 1842	. . . . . . . . . . . . . . 15 |- ( w = <. <. r , s >. , t >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) <-> E. x E. y E. z ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) ) )
56	55	imbi1d 230	. . . . . . . . . . . . . 14 |- ( w = <. <. r , s >. , t >. -> ( ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) <-> ( E. x E. y E. z ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) -> ph ) ) )
57	53, 56	imbi12d 233	. . . . . . . . . . . . 13 |- ( w = <. <. r , s >. , t >. -> ( ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) <-> ( <. <. x , y >. , z >. = <. <. r , s >. , t >. -> ( E. x E. y E. z ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) -> ph ) ) ) )
58	50, 57	mpbiri 167	. . . . . . . . . . . 12 |- ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) )
59	16, 58	syl6bi 162	. . . . . . . . . . 11 |- ( a = <. r , s >. -> ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
60	59	adantr 274	. . . . . . . . . 10 |- ( ( a = <. r , s >. /\ <. r , s >. = <. x , y >. ) -> ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
61	60	exlimivv 1869	. . . . . . . . 9 |- ( E. r E. s ( a = <. r , s >. /\ <. r , s >. = <. x , y >. ) -> ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
62	14, 61	sylbi 120	. . . . . . . 8 |- ( a = <. x , y >. -> ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
63	62	com3l 81	. . . . . . 7 |- ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( a = <. x , y >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
64	13, 63	mpdd 41	. . . . . 6 |- ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) )
65	64	adantr 274	. . . . 5 |- ( ( w = <. a , t >. /\ <. a , t >. = <. <. x , y >. , z >. ) -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) )
66	65	exlimivv 1869	. . . 4 |- ( E. a E. t ( w = <. a , t >. /\ <. a , t >. = <. <. x , y >. , z >. ) -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) )
67	8, 66	mpcom 36	. . 3 |- ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) )
68		19.8a 1570	. . . . 5 |- ( ( w = <. <. x , y >. , z >. /\ ph ) -> E. z ( w = <. <. x , y >. , z >. /\ ph ) )
69		19.8a 1570	. . . . 5 |- ( E. z ( w = <. <. x , y >. , z >. /\ ph ) -> E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
70		19.8a 1570	. . . . 5 |- ( E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
71	68, 69, 70	3syl 17	. . . 4 |- ( ( w = <. <. x , y >. , z >. /\ ph ) -> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
72	71	ex 114	. . 3 |- ( w = <. <. x , y >. , z >. -> ( ph -> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) ) )
73	67, 72	impbid 128	. 2 |- ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) <-> ph ) )
74		df-oprab 5786	. 2 |- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
75	6, 73, 74	elab2 2836	1 |- ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   /\ w3a 963   = wceq 1332   E.wex 1469   e. wcel 1481   E!weu 2000   _Vcvv 2689   <.cop 3535   {coprab 5783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-pow 4106  ax-pr 4139  ax-setind 4460

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-v 2691  df-dif 3078  df-un 3080  df-in 3082  df-ss 3089  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-oprab 5786

This theorem is referenced by:  ssoprab2b  5836  ovid  5895  ovidig  5896  tposoprab  6185  xpcomco  6728