Theorem oprabid 5796

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 1486 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 2684	. . . 4 |- x e. _V
2		vex 2684	. . . 4 |- y e. _V
3	1, 2	opex 4146	. . 3 |- <. x , y >. e. _V
4		vex 2684	. . 3 |- z e. _V
5		opexg 4145	. . 3 |- ( ( <. x , y >. e. _V /\ z e. _V ) -> <. <. x , y >. , z >. e. _V )
6	3, 4, 5	mp2an 422	. 2 |- <. <. x , y >. , z >. e. _V
7	3, 4	eqvinop 4160	. . . . 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 2144	. . . . . . . 8 |- ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. <-> <. a , t >. = <. <. x , y >. , z >. ) )
10		vex 2684	. . . . . . . . 9 |- a e. _V
11		vex 2684	. . . . . . . . 9 |- t e. _V
12	10, 11	opth1 4153	. . . . . . . 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 4160	. . . . . . . . 9 |- ( a = <. x , y >. <-> E. r E. s ( a = <. r , s >. /\ <. r , s >. = <. x , y >. ) )
15		opeq1 3700	. . . . . . . . . . . . 13 |- ( a = <. r , s >. -> <. a , t >. = <. <. r , s >. , t >. )
16	15	eqeq2d 2149	. . . . . . . . . . . 12 |- ( a = <. r , s >. -> ( w = <. a , t >. <-> w = <. <. r , s >. , t >. ) )
17	1, 2, 4	otth2 4158	. . . . . . . . . . . . . . . . . . 19 |- ( <. <. x , y >. , z >. = <. <. r , s >. , t >. <-> ( x = r /\ y = s /\ z = t ) )
18		df-3an 964	. . . . . . . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . . . . 17 |- ( ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) <-> ( ( ( x = r /\ y = s ) /\ z = t ) /\ ph ) )
21		anass 398	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x = r /\ y = s ) /\ z = t ) /\ ph ) <-> ( ( x = r /\ y = s ) /\ ( z = t /\ ph ) ) )
22		anass 398	. . . . . . . . . . . . . . . . 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 1586	. . . . . . . . . . . . . . 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 5795	. . . . . . . . . . . . . . . . . 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 1579	. . . . . . . . . . . . . . . . 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 1642	. . . . . . . . . . . . . . . . 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 1642	. . . . . . . . . . . . . . . . 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 5795	. . . . . . . . . . . . . . . 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 5795	. . . . . . . . . . . . . . . . . 18 |- ( E. y E. z ( y = s /\ ( z = t /\ ph ) ) -> E. y ( y = s /\ E. z ( z = t /\ ph ) ) )
32	31	anim2i 339	. . . . . . . . . . . . . . . . 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 1579	. . . . . . . . . . . . . . . 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 2092	. . . . . . . . . . . . . . . . . . 19 |- E! x x = r
37		eupick 2076	. . . . . . . . . . . . . . . . . . 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 420	. . . . . . . . . . . . . . . . . 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 2092	. . . . . . . . . . . . . . . . . . . 20 |- E! y y = s
40		eupick 2076	. . . . . . . . . . . . . . . . . . . 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 420	. . . . . . . . . . . . . . . . . . 19 |- ( E. y ( y = s /\ E. z ( z = t /\ ph ) ) -> ( y = s -> E. z ( z = t /\ ph ) ) )
42		euequ1 2092	. . . . . . . . . . . . . . . . . . . 20 |- E! z z = t
43		eupick 2076	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E! z z = t /\ E. z ( z = t /\ ph ) ) -> ( z = t -> ph ) )
44	42, 43	mpan 420	. . . . . . . . . . . . . . . . . . 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 1199	. . . . . . . . . . . . . . . 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 2144	. . . . . . . . . . . . . . 15 |- ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. <-> <. <. r , s >. , t >. = <. <. x , y >. , z >. ) )
52		eqcom 2139	. . . . . . . . . . . . . . 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 460	. . . . . . . . . . . . . . . 16 |- ( w = <. <. r , s >. , t >. -> ( ( w = <. <. x , y >. , z >. /\ ph ) <-> ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) ) )
55	54	3exbidv 1841	. . . . . . . . . . . . . . 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 1868	. . . . . . . . 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 1868	. . . 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 1569	. . . . 5 |- ( ( w = <. <. x , y >. , z >. /\ ph ) -> E. z ( w = <. <. x , y >. , z >. /\ ph ) )
69		19.8a 1569	. . . . 5 |- ( E. z ( w = <. <. x , y >. , z >. /\ ph ) -> E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
70		19.8a 1569	. . . . 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 5771	. 2 |- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
75	6, 73, 74	elab2 2827	1 |- ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   /\ w3a 962   = wceq 1331   E.wex 1468   e. wcel 1480   E!weu 1997   _Vcvv 2681   <.cop 3525   {coprab 5768

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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-pow 4093  ax-pr 4126  ax-setind 4447

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ne 2307  df-ral 2419  df-v 2683  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-oprab 5771

This theorem is referenced by:  ssoprab2b  5821  ovid  5880  ovidig  5881  tposoprab  6170  xpcomco  6713