Theorem oprabid 6677

Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (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		opex 4932	. 2 |- <. <. x , y >. , z >. e. _V
2		opex 4932	. . . . . 6 |- <. x , y >. e. _V
3		vex 3203	. . . . . 6 |- z e. _V
4	2, 3	eqvinop 4955	. . . . 5 |- ( w = <. <. x , y >. , z >. <-> E. a E. t ( w = <. a , t >. /\ <. a , t >. = <. <. x , y >. , z >. ) )
5	4	biimpi 206	. . . 4 |- ( w = <. <. x , y >. , z >. -> E. a E. t ( w = <. a , t >. /\ <. a , t >. = <. <. x , y >. , z >. ) )
6		eqeq1 2626	. . . . . . . 8 |- ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. <-> <. a , t >. = <. <. x , y >. , z >. ) )
7		vex 3203	. . . . . . . . 9 |- a e. _V
8		vex 3203	. . . . . . . . 9 |- t e. _V
9	7, 8	opth1 4944	. . . . . . . 8 |- ( <. a , t >. = <. <. x , y >. , z >. -> a = <. x , y >. )
10	6, 9	syl6bi 243	. . . . . . 7 |- ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> a = <. x , y >. ) )
11		vex 3203	. . . . . . . . . 10 |- x e. _V
12		vex 3203	. . . . . . . . . 10 |- y e. _V
13	11, 12	eqvinop 4955	. . . . . . . . 9 |- ( a = <. x , y >. <-> E. r E. s ( a = <. r , s >. /\ <. r , s >. = <. x , y >. ) )
14		opeq1 4402	. . . . . . . . . . . . 13 |- ( a = <. r , s >. -> <. a , t >. = <. <. r , s >. , t >. )
15	14	eqeq2d 2632	. . . . . . . . . . . 12 |- ( a = <. r , s >. -> ( w = <. a , t >. <-> w = <. <. r , s >. , t >. ) )
16	11, 12, 3	otth2 4952	. . . . . . . . . . . . . . 15 |- ( <. <. x , y >. , z >. = <. <. r , s >. , t >. <-> ( x = r /\ y = s /\ z = t ) )
17		euequ1 2476	. . . . . . . . . . . . . . . . . 18 |- E! x x = r
18		eupick 2536	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) ) )
19	17, 18	mpan 706	. . . . . . . . . . . . . . . . 17 |- ( E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( x = r -> E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) )
20		euequ1 2476	. . . . . . . . . . . . . . . . . . 19 |- E! y y = s
21		eupick 2536	. . . . . . . . . . . . . . . . . . 19 |- ( ( E! y y = s /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( y = s -> E. z ( z = t /\ ph ) ) )
22	20, 21	mpan 706	. . . . . . . . . . . . . . . . . 18 |- ( E. y ( y = s /\ E. z ( z = t /\ ph ) ) -> ( y = s -> E. z ( z = t /\ ph ) ) )
23		euequ1 2476	. . . . . . . . . . . . . . . . . . 19 |- E! z z = t
24		eupick 2536	. . . . . . . . . . . . . . . . . . 19 |- ( ( E! z z = t /\ E. z ( z = t /\ ph ) ) -> ( z = t -> ph ) )
25	23, 24	mpan 706	. . . . . . . . . . . . . . . . . 18 |- ( E. z ( z = t /\ ph ) -> ( z = t -> ph ) )
26	22, 25	syl6 35	. . . . . . . . . . . . . . . . 17 |- ( E. y ( y = s /\ E. z ( z = t /\ ph ) ) -> ( y = s -> ( z = t -> ph ) ) )
27	19, 26	syl6 35	. . . . . . . . . . . . . . . 16 |- ( E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( x = r -> ( y = s -> ( z = t -> ph ) ) ) )
28	27	3impd 1281	. . . . . . . . . . . . . . 15 |- ( E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( ( x = r /\ y = s /\ z = t ) -> ph ) )
29	16, 28	syl5bi 232	. . . . . . . . . . . . . 14 |- ( E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( <. <. x , y >. , z >. = <. <. r , s >. , t >. -> ph ) )
30		df-3an 1039	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = r /\ y = s /\ z = t ) <-> ( ( x = r /\ y = s ) /\ z = t ) )
31	16, 30	bitri 264	. . . . . . . . . . . . . . . . . 18 |- ( <. <. x , y >. , z >. = <. <. r , s >. , t >. <-> ( ( x = r /\ y = s ) /\ z = t ) )
32	31	anbi1i 731	. . . . . . . . . . . . . . . . 17 |- ( ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) <-> ( ( ( x = r /\ y = s ) /\ z = t ) /\ ph ) )
33		anass 681	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x = r /\ y = s ) /\ z = t ) /\ ph ) <-> ( ( x = r /\ y = s ) /\ ( z = t /\ ph ) ) )
34		anass 681	. . . . . . . . . . . . . . . . 17 |- ( ( ( x = r /\ y = s ) /\ ( z = t /\ ph ) ) <-> ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) )
35	32, 33, 34	3bitri 286	. . . . . . . . . . . . . . . 16 |- ( ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) <-> ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) )
36	35	3exbii 1776	. . . . . . . . . . . . . . 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 ) ) ) )
37		nfcvf2 2789	. . . . . . . . . . . . . . . . . . . 20 |- ( -. A. x x = z -> F/_ z x )
38		nfcvd 2765	. . . . . . . . . . . . . . . . . . . 20 |- ( -. A. x x = z -> F/_ z r )
39	37, 38	nfeqd 2772	. . . . . . . . . . . . . . . . . . 19 |- ( -. A. x x = z -> F/ z x = r )
40	39	exdistrf 2333	. . . . . . . . . . . . . . . . . 18 |- ( E. x E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) )
41	40	eximi 1762	. . . . . . . . . . . . . . . . 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 ) ) ) )
42		excom 2042	. . . . . . . . . . . . . . . . 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 ) ) ) )
43		excom 2042	. . . . . . . . . . . . . . . . 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 ) ) ) )
44	41, 42, 43	3imtr4i 281	. . . . . . . . . . . . . . . 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 ) ) ) )
45		nfcvf2 2789	. . . . . . . . . . . . . . . . . 18 |- ( -. A. x x = y -> F/_ y x )
46		nfcvd 2765	. . . . . . . . . . . . . . . . . 18 |- ( -. A. x x = y -> F/_ y r )
47	45, 46	nfeqd 2772	. . . . . . . . . . . . . . . . 17 |- ( -. A. x x = y -> F/ y x = r )
48	47	exdistrf 2333	. . . . . . . . . . . . . . . 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 ) ) ) )
49		nfcvf2 2789	. . . . . . . . . . . . . . . . . . . 20 |- ( -. A. y y = z -> F/_ z y )
50		nfcvd 2765	. . . . . . . . . . . . . . . . . . . 20 |- ( -. A. y y = z -> F/_ z s )
51	49, 50	nfeqd 2772	. . . . . . . . . . . . . . . . . . 19 |- ( -. A. y y = z -> F/ z y = s )
52	51	exdistrf 2333	. . . . . . . . . . . . . . . . . 18 |- ( E. y E. z ( y = s /\ ( z = t /\ ph ) ) -> E. y ( y = s /\ E. z ( z = t /\ ph ) ) )
53	52	anim2i 593	. . . . . . . . . . . . . . . . 17 |- ( ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) -> ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) )
54	53	eximi 1762	. . . . . . . . . . . . . . . 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 ) ) ) )
55	44, 48, 54	3syl 18	. . . . . . . . . . . . . . 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 ) ) ) )
56	36, 55	sylbi 207	. . . . . . . . . . . . . 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 ) ) ) )
57	29, 56	syl11 33	. . . . . . . . . . . . 13 |- ( <. <. x , y >. , z >. = <. <. r , s >. , t >. -> ( E. x E. y E. z ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) -> ph ) )
58		eqeq1 2626	. . . . . . . . . . . . . . 15 |- ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. <-> <. <. r , s >. , t >. = <. <. x , y >. , z >. ) )
59		eqcom 2629	. . . . . . . . . . . . . . 15 |- ( <. <. r , s >. , t >. = <. <. x , y >. , z >. <-> <. <. x , y >. , z >. = <. <. r , s >. , t >. )
60	58, 59	syl6bb 276	. . . . . . . . . . . . . 14 |- ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. <-> <. <. x , y >. , z >. = <. <. r , s >. , t >. ) )
61	60	anbi1d 741	. . . . . . . . . . . . . . . 16 |- ( w = <. <. r , s >. , t >. -> ( ( w = <. <. x , y >. , z >. /\ ph ) <-> ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) ) )
62	61	3exbidv 1853	. . . . . . . . . . . . . . 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 ) ) )
63	62	imbi1d 331	. . . . . . . . . . . . . 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 ) ) )
64	60, 63	imbi12d 334	. . . . . . . . . . . . 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 ) ) ) )
65	57, 64	mpbiri 248	. . . . . . . . . . . 12 |- ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) )
66	15, 65	syl6bi 243	. . . . . . . . . . 11 |- ( a = <. r , s >. -> ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
67	66	adantr 481	. . . . . . . . . 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 ) ) ) )
68	67	exlimivv 1860	. . . . . . . . 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 ) ) ) )
69	13, 68	sylbi 207	. . . . . . . 8 |- ( a = <. x , y >. -> ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
70	69	com3l 89	. . . . . . 7 |- ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( a = <. x , y >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
71	10, 70	mpdd 43	. . . . . 6 |- ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) )
72	71	adantr 481	. . . . 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 ) ) )
73	72	exlimivv 1860	. . . 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 ) ) )
74	5, 73	mpcom 38	. . 3 |- ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) )
75		19.8a 2052	. . . . 5 |- ( ( w = <. <. x , y >. , z >. /\ ph ) -> E. z ( w = <. <. x , y >. , z >. /\ ph ) )
76		19.8a 2052	. . . . 5 |- ( E. z ( w = <. <. x , y >. , z >. /\ ph ) -> E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
77		19.8a 2052	. . . . 5 |- ( E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
78	75, 76, 77	3syl 18	. . . 4 |- ( ( w = <. <. x , y >. , z >. /\ ph ) -> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
79	78	ex 450	. . 3 |- ( w = <. <. x , y >. , z >. -> ( ph -> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) ) )
80	74, 79	impbid 202	. 2 |- ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) <-> ph ) )
81		df-oprab 6654	. 2 |- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
82	1, 80, 81	elab2 3354	1 |- ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   E!weu 2470   <.cop 4183   {coprab 6651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-oprab 6654

This theorem is referenced by:  ssoprab2b  6712  ovid  6777  ovidig  6778  tposoprab  7388  xpcomco  8050