Theorem oprabid 5907

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 1509 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 2741	. . . 4 |- x e. _V
2		vex 2741	. . . 4 |- y e. _V
3	1, 2	opex 4230	. . 3 |- <. x , y >. e. _V
4		vex 2741	. . 3 |- z e. _V
5		opexg 4229	. . 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 4244	. . . . 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 2184	. . . . . . . 8 |- ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. <-> <. a , t >. = <. <. x , y >. , z >. ) )
10		vex 2741	. . . . . . . . 9 |- a e. _V
11		vex 2741	. . . . . . . . 9 |- t e. _V
12	10, 11	opth1 4237	. . . . . . . 8 |- ( <. a , t >. = <. <. x , y >. , z >. -> a = <. x , y >. )
13	9, 12	syl6bi 163	. . . . . . 7 |- ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> a = <. x , y >. ) )
14	1, 2	eqvinop 4244	. . . . . . . . 9 |- ( a = <. x , y >. <-> E. r E. s ( a = <. r , s >. /\ <. r , s >. = <. x , y >. ) )
15		opeq1 3779	. . . . . . . . . . . . 13 |- ( a = <. r , s >. -> <. a , t >. = <. <. r , s >. , t >. )
16	15	eqeq2d 2189	. . . . . . . . . . . 12 |- ( a = <. r , s >. -> ( w = <. a , t >. <-> w = <. <. r , s >. , t >. ) )
17	1, 2, 4	otth2 4242	. . . . . . . . . . . . . . . . . . 19 |- ( <. <. x , y >. , z >. = <. <. r , s >. , t >. <-> ( x = r /\ y = s /\ z = t ) )
18		df-3an 980	. . . . . . . . . . . . . . . . . . 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 1607	. . . . . . . . . . . . . . 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 5906	. . . . . . . . . . . . . . . . . 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 1600	. . . . . . . . . . . . . . . . 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 1664	. . . . . . . . . . . . . . . . 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 1664	. . . . . . . . . . . . . . . . 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 5906	. . . . . . . . . . . . . . . 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 5906	. . . . . . . . . . . . . . . . . 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 1600	. . . . . . . . . . . . . . . 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 2121	. . . . . . . . . . . . . . . . . . 19 |- E! x x = r
37		eupick 2105	. . . . . . . . . . . . . . . . . . 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 2121	. . . . . . . . . . . . . . . . . . . 20 |- E! y y = s
40		eupick 2105	. . . . . . . . . . . . . . . . . . . 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 2121	. . . . . . . . . . . . . . . . . . . 20 |- E! z z = t
43		eupick 2105	. . . . . . . . . . . . . . . . . . . 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 1221	. . . . . . . . . . . . . . . 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 2184	. . . . . . . . . . . . . . 15 |- ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. <-> <. <. r , s >. , t >. = <. <. x , y >. , z >. ) )
52		eqcom 2179	. . . . . . . . . . . . . . 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 1869	. . . . . . . . . . . . . . 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	syl6bi 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 1896	. . . . . . . . 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 1896	. . . 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 1590	. . . . 5 |- ( ( w = <. <. x , y >. , z >. /\ ph ) -> E. z ( w = <. <. x , y >. , z >. /\ ph ) )
69		19.8a 1590	. . . . 5 |- ( E. z ( w = <. <. x , y >. , z >. /\ ph ) -> E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
70		19.8a 1590	. . . . 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 5879	. 2 |- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
75	6, 73, 74	elab2 2886	1 |- ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 978   = wceq 1353   E.wex 1492   E!weu 2026   e. wcel 2148   _Vcvv 2738   <.cop 3596   {coprab 5876

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-setind 4537

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-v 2740  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-oprab 5879

This theorem is referenced by:  ssoprab2b  5932  ovid  5991  ovidig  5992  tposoprab  6281  xpcomco  6826