Theorem oprabid 5954

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 condition between x, y, and z, we use ax-bndl 1523 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 2766	. . . 4 |- x e. _V
2		vex 2766	. . . 4 |- y e. _V
3	1, 2	opex 4262	. . 3 |- <. x , y >. e. _V
4		vex 2766	. . 3 |- z e. _V
5		opexg 4261	. . 3 |- ( ( <. x , y >. e. _V /\ z e. _V ) -> <. <. x , y >. , z >. e. _V )
6	3, 4, 5	mp2an 426	. 2 |- <. <. x , y >. , z >. e. _V
7	3, 4	eqvinop 4276	. . . . 5 |- ( w = <. <. x , y >. , z >. <-> E. a E. t ( w = <. a , t >. /\ <. a , t >. = <. <. x , y >. , z >. ) )
8	7	biimpi 120	. . . 4 |- ( w = <. <. x , y >. , z >. -> E. a E. t ( w = <. a , t >. /\ <. a , t >. = <. <. x , y >. , z >. ) )
9		eqeq1 2203	. . . . . . . 8 |- ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. <-> <. a , t >. = <. <. x , y >. , z >. ) )
10		vex 2766	. . . . . . . . 9 |- a e. _V
11		vex 2766	. . . . . . . . 9 |- t e. _V
12	10, 11	opth1 4269	. . . . . . . 8 |- ( <. a , t >. = <. <. x , y >. , z >. -> a = <. x , y >. )
13	9, 12	biimtrdi 163	. . . . . . 7 |- ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> a = <. x , y >. ) )
14	1, 2	eqvinop 4276	. . . . . . . . 9 |- ( a = <. x , y >. <-> E. r E. s ( a = <. r , s >. /\ <. r , s >. = <. x , y >. ) )
15		opeq1 3808	. . . . . . . . . . . . 13 |- ( a = <. r , s >. -> <. a , t >. = <. <. r , s >. , t >. )
16	15	eqeq2d 2208	. . . . . . . . . . . 12 |- ( a = <. r , s >. -> ( w = <. a , t >. <-> w = <. <. r , s >. , t >. ) )
17	1, 2, 4	otth2 4274	. . . . . . . . . . . . . . . . . . 19 |- ( <. <. x , y >. , z >. = <. <. r , s >. , t >. <-> ( x = r /\ y = s /\ z = t ) )
18		df-3an 982	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = r /\ y = s /\ z = t ) <-> ( ( x = r /\ y = s ) /\ z = t ) )
19	17, 18	bitri 184	. . . . . . . . . . . . . . . . . 18 |- ( <. <. x , y >. , z >. = <. <. r , s >. , t >. <-> ( ( x = r /\ y = s ) /\ z = t ) )
20	19	anbi1i 458	. . . . . . . . . . . . . . . . 17 |- ( ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) <-> ( ( ( x = r /\ y = s ) /\ z = t ) /\ ph ) )
21		anass 401	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x = r /\ y = s ) /\ z = t ) /\ ph ) <-> ( ( x = r /\ y = s ) /\ ( z = t /\ ph ) ) )
22		anass 401	. . . . . . . . . . . . . . . . 17 |- ( ( ( x = r /\ y = s ) /\ ( z = t /\ ph ) ) <-> ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) )
23	20, 21, 22	3bitri 206	. . . . . . . . . . . . . . . 16 |- ( ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) <-> ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) )
24	23	3exbii 1621	. . . . . . . . . . . . . . 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 5953	. . . . . . . . . . . . . . . . . 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 1614	. . . . . . . . . . . . . . . . 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 1678	. . . . . . . . . . . . . . . . 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 1678	. . . . . . . . . . . . . . . . 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 201	. . . . . . . . . . . . . . . 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 5953	. . . . . . . . . . . . . . . 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 5953	. . . . . . . . . . . . . . . . . 18 |- ( E. y E. z ( y = s /\ ( z = t /\ ph ) ) -> E. y ( y = s /\ E. z ( z = t /\ ph ) ) )
32	31	anim2i 342	. . . . . . . . . . . . . . . . 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 1614	. . . . . . . . . . . . . . . 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 121	. . . . . . . . . . . . . 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 2140	. . . . . . . . . . . . . . . . . . 19 |- E! x x = r
37		eupick 2124	. . . . . . . . . . . . . . . . . . 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 424	. . . . . . . . . . . . . . . . . 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 2140	. . . . . . . . . . . . . . . . . . . 20 |- E! y y = s
40		eupick 2124	. . . . . . . . . . . . . . . . . . . 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 424	. . . . . . . . . . . . . . . . . . 19 |- ( E. y ( y = s /\ E. z ( z = t /\ ph ) ) -> ( y = s -> E. z ( z = t /\ ph ) ) )
42		euequ1 2140	. . . . . . . . . . . . . . . . . . . 20 |- E! z z = t
43		eupick 2124	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E! z z = t /\ E. z ( z = t /\ ph ) ) -> ( z = t -> ph ) )
44	42, 43	mpan 424	. . . . . . . . . . . . . . . . . . 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 1223	. . . . . . . . . . . . . . . 16 |- ( E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( ( x = r /\ y = s /\ z = t ) -> ph ) )
48	17, 47	biimtrid 152	. . . . . . . . . . . . . . 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 2203	. . . . . . . . . . . . . . 15 |- ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. <-> <. <. r , s >. , t >. = <. <. x , y >. , z >. ) )
52		eqcom 2198	. . . . . . . . . . . . . . 15 |- ( <. <. r , s >. , t >. = <. <. x , y >. , z >. <-> <. <. x , y >. , z >. = <. <. r , s >. , t >. )
53	51, 52	bitrdi 196	. . . . . . . . . . . . . 14 |- ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. <-> <. <. x , y >. , z >. = <. <. r , s >. , t >. ) )
54	53	anbi1d 465	. . . . . . . . . . . . . . . 16 |- ( w = <. <. r , s >. , t >. -> ( ( w = <. <. x , y >. , z >. /\ ph ) <-> ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) ) )
55	54	3exbidv 1883	. . . . . . . . . . . . . . 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 231	. . . . . . . . . . . . . 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 234	. . . . . . . . . . . . 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 168	. . . . . . . . . . . 12 |- ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) )
59	16, 58	biimtrdi 163	. . . . . . . . . . 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 276	. . . . . . . . . 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 1911	. . . . . . . . 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 121	. . . . . . . 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 276	. . . . 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 1911	. . . 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 1604	. . . . 5 |- ( ( w = <. <. x , y >. , z >. /\ ph ) -> E. z ( w = <. <. x , y >. , z >. /\ ph ) )
69		19.8a 1604	. . . . 5 |- ( E. z ( w = <. <. x , y >. , z >. /\ ph ) -> E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
70		19.8a 1604	. . . . 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 115	. . 3 |- ( w = <. <. x , y >. , z >. -> ( ph -> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) ) )
73	67, 72	impbid 129	. 2 |- ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) <-> ph ) )
74		df-oprab 5926	. 2 |- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
75	6, 73, 74	elab2 2912	1 |- ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 980   = wceq 1364   E.wex 1506   E!weu 2045   e. wcel 2167   _Vcvv 2763   <.cop 3625   {coprab 5923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242  ax-setind 4573

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-ral 2480  df-v 2765  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-oprab 5926

This theorem is referenced by:  ssoprab2b  5979  ovid  6039  ovidig  6040  tposoprab  6338  xpcomco  6885