Metamath Proof Explorer

Theorem oprabidw

Description: The law of concretion. Special case of Theorem 9.5 of Quine p. 61. Version of oprabid with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 20-Mar-2013) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

Ref Expression
Assertion oprabidw 
|- ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )

Proof

Step Hyp Ref Expression
1 opex 
 |-  <. <. x , y >. , z >. e. _V
2 opex 
 |-  <. x , y >. e. _V
3 vex 
 |-  z e. _V
4 2 3 eqvinop 
 |-  ( w = <. <. x , y >. , z >. <-> E. a E. t ( w = <. a , t >. /\ <. a , t >. = <. <. x , y >. , z >. ) )
5 4 biimpi 
 |-  ( w = <. <. x , y >. , z >. -> E. a E. t ( w = <. a , t >. /\ <. a , t >. = <. <. x , y >. , z >. ) )
6 eqeq1 
 |-  ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. <-> <. a , t >. = <. <. x , y >. , z >. ) )
7 vex 
 |-  a e. _V
8 vex 
 |-  t e. _V
9 7 8 opth1 
 |-  ( <. a , t >. = <. <. x , y >. , z >. -> a = <. x , y >. )
10 6 9 biimtrdi 
 |-  ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> a = <. x , y >. ) )
11 vex 
 |-  x e. _V
12 vex 
 |-  y e. _V
13 11 12 eqvinop 
 |-  ( a = <. x , y >. <-> E. r E. s ( a = <. r , s >. /\ <. r , s >. = <. x , y >. ) )
14 opeq1 
 |-  ( a = <. r , s >. -> <. a , t >. = <. <. r , s >. , t >. )
15 14 eqeq2d 
 |-  ( a = <. r , s >. -> ( w = <. a , t >. <-> w = <. <. r , s >. , t >. ) )
16 11 12 3 otth2 
 |-  ( <. <. x , y >. , z >. = <. <. r , s >. , t >. <-> ( x = r /\ y = s /\ z = t ) )
17 euequ 
 |-  E! x x = r
18 eupick 
 |-  ( ( 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 
 |-  ( 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 euequ 
 |-  E! y y = s
21 eupick 
 |-  ( ( E! y y = s /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( y = s -> E. z ( z = t /\ ph ) ) )
22 20 21 mpan 
 |-  ( E. y ( y = s /\ E. z ( z = t /\ ph ) ) -> ( y = s -> E. z ( z = t /\ ph ) ) )
23 euequ 
 |-  E! z z = t
24 eupick 
 |-  ( ( E! z z = t /\ E. z ( z = t /\ ph ) ) -> ( z = t -> ph ) )
25 23 24 mpan 
 |-  ( E. z ( z = t /\ ph ) -> ( z = t -> ph ) )
26 22 25 syl6 
 |-  ( E. y ( y = s /\ E. z ( z = t /\ ph ) ) -> ( y = s -> ( z = t -> ph ) ) )
27 19 26 syl6 
 |-  ( E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( x = r -> ( y = s -> ( z = t -> ph ) ) ) )
28 27 3impd 
 |-  ( E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( ( x = r /\ y = s /\ z = t ) -> ph ) )
29 16 28 biimtrid 
 |-  ( E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( <. <. x , y >. , z >. = <. <. r , s >. , t >. -> ph ) )
30 df-3an 
 |-  ( ( x = r /\ y = s /\ z = t ) <-> ( ( x = r /\ y = s ) /\ z = t ) )
31 16 30 bitri 
 |-  ( <. <. x , y >. , z >. = <. <. r , s >. , t >. <-> ( ( x = r /\ y = s ) /\ z = t ) )
32 31 anbi1i 
 |-  ( ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) <-> ( ( ( x = r /\ y = s ) /\ z = t ) /\ ph ) )
33 anass 
 |-  ( ( ( ( x = r /\ y = s ) /\ z = t ) /\ ph ) <-> ( ( x = r /\ y = s ) /\ ( z = t /\ ph ) ) )
34 anass 
 |-  ( ( ( x = r /\ y = s ) /\ ( z = t /\ ph ) ) <-> ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) )
35 32 33 34 3bitri 
 |-  ( ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) <-> ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) )
36 35 3exbii 
 |-  ( 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 nfe1 
 |-  F/ x E. x ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) )
38 19.8a 
 |-  ( ( y = s /\ ( z = t /\ ph ) ) -> E. z ( y = s /\ ( z = t /\ ph ) ) )
39 38 anim2i 
 |-  ( ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) -> ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) )
40 39 eximi 
 |-  ( E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) -> E. z ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) )
41 biidd 
 |-  ( A. x x = z -> ( ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) <-> ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) ) )
42 41 drex1v 
 |-  ( A. x x = z -> ( E. x ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) <-> E. z ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) ) )
43 40 42 imbitrrid 
 |-  ( A. x x = z -> ( E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) ) )
44 19.40 
 |-  ( E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) -> ( E. z x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) )
45 nfvd 
 |-  ( -. A. x x = z -> F/ z x = r )
46 45 19.9d 
 |-  ( -. A. x x = z -> ( E. z x = r -> x = r ) )
47 46 anim1d 
 |-  ( -. A. x x = z -> ( ( E. z x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) -> ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) ) )
48 19.8a 
 |-  ( ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) )
49 44 47 48 syl56 
 |-  ( -. A. x x = z -> ( E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) ) )
50 43 49 pm2.61i 
 |-  ( E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) )
51 37 50 exlimi 
 |-  ( E. x E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) )
52 51 eximi 
 |-  ( 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 ) ) ) )
53 excom 
 |-  ( 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 ) ) ) )
54 excom 
 |-  ( 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 ) ) ) )
55 52 53 54 3imtr4i 
 |-  ( 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 ) ) ) )
56 nfe1 
 |-  F/ x E. x ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) )
57 19.8a 
 |-  ( E. z ( y = s /\ ( z = t /\ ph ) ) -> E. y E. z ( y = s /\ ( z = t /\ ph ) ) )
58 57 anim2i 
 |-  ( ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) -> ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) )
59 58 eximi 
 |-  ( E. y ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) -> E. y ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) )
60 biidd 
 |-  ( A. x x = y -> ( ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) <-> ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) ) )
61 60 drex1v 
 |-  ( A. x x = y -> ( E. x ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) <-> E. y ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) ) )
62 59 61 imbitrrid 
 |-  ( A. x x = y -> ( E. y ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) ) )
63 19.40 
 |-  ( E. y ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) -> ( E. y x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) )
64 nfvd 
 |-  ( -. A. x x = y -> F/ y x = r )
65 64 19.9d 
 |-  ( -. A. x x = y -> ( E. y x = r -> x = r ) )
66 65 anim1d 
 |-  ( -. A. x x = y -> ( ( E. y x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) -> ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) ) )
67 19.8a 
 |-  ( ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) )
68 63 66 67 syl56 
 |-  ( -. A. x x = y -> ( E. y ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) ) )
69 62 68 pm2.61i 
 |-  ( E. y ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) )
70 56 69 exlimi 
 |-  ( 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 ) ) ) )
71 nfe1 
 |-  F/ y E. y ( y = s /\ E. z ( z = t /\ ph ) )
72 19.8a 
 |-  ( ( z = t /\ ph ) -> E. z ( z = t /\ ph ) )
73 72 anim2i 
 |-  ( ( y = s /\ ( z = t /\ ph ) ) -> ( y = s /\ E. z ( z = t /\ ph ) ) )
74 73 eximi 
 |-  ( E. z ( y = s /\ ( z = t /\ ph ) ) -> E. z ( y = s /\ E. z ( z = t /\ ph ) ) )
75 biidd 
 |-  ( A. y y = z -> ( ( y = s /\ E. z ( z = t /\ ph ) ) <-> ( y = s /\ E. z ( z = t /\ ph ) ) ) )
76 75 drex1v 
 |-  ( A. y y = z -> ( E. y ( y = s /\ E. z ( z = t /\ ph ) ) <-> E. z ( y = s /\ E. z ( z = t /\ ph ) ) ) )
77 74 76 imbitrrid 
 |-  ( A. y y = z -> ( E. z ( y = s /\ ( z = t /\ ph ) ) -> E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) )
78 19.40 
 |-  ( E. z ( y = s /\ ( z = t /\ ph ) ) -> ( E. z y = s /\ E. z ( z = t /\ ph ) ) )
79 nfvd 
 |-  ( -. A. y y = z -> F/ z y = s )
80 79 19.9d 
 |-  ( -. A. y y = z -> ( E. z y = s -> y = s ) )
81 80 anim1d 
 |-  ( -. A. y y = z -> ( ( E. z y = s /\ E. z ( z = t /\ ph ) ) -> ( y = s /\ E. z ( z = t /\ ph ) ) ) )
82 19.8a 
 |-  ( ( y = s /\ E. z ( z = t /\ ph ) ) -> E. y ( y = s /\ E. z ( z = t /\ ph ) ) )
83 78 81 82 syl56 
 |-  ( -. A. y y = z -> ( E. z ( y = s /\ ( z = t /\ ph ) ) -> E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) )
84 77 83 pm2.61i 
 |-  ( E. z ( y = s /\ ( z = t /\ ph ) ) -> E. y ( y = s /\ E. z ( z = t /\ ph ) ) )
85 71 84 exlimi 
 |-  ( E. y E. z ( y = s /\ ( z = t /\ ph ) ) -> E. y ( y = s /\ E. z ( z = t /\ ph ) ) )
86 85 anim2i 
 |-  ( ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) -> ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) )
87 86 eximi 
 |-  ( 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 ) ) ) )
88 55 70 87 3syl 
 |-  ( 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 ) ) ) )
89 36 88 sylbi 
 |-  ( 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 ) ) ) )
90 29 89 syl11 
 |-  ( <. <. x , y >. , z >. = <. <. r , s >. , t >. -> ( E. x E. y E. z ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) -> ph ) )
91 eqeq1 
 |-  ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. <-> <. <. r , s >. , t >. = <. <. x , y >. , z >. ) )
92 eqcom 
 |-  ( <. <. r , s >. , t >. = <. <. x , y >. , z >. <-> <. <. x , y >. , z >. = <. <. r , s >. , t >. )
93 91 92 bitrdi 
 |-  ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. <-> <. <. x , y >. , z >. = <. <. r , s >. , t >. ) )
94 93 anbi1d 
 |-  ( w = <. <. r , s >. , t >. -> ( ( w = <. <. x , y >. , z >. /\ ph ) <-> ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) ) )
95 94 3exbidv 
 |-  ( 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 ) ) )
96 95 imbi1d 
 |-  ( 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 ) ) )
97 93 96 imbi12d 
 |-  ( 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 ) ) ) )
98 90 97 mpbiri 
 |-  ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) )
99 15 98 biimtrdi 
 |-  ( a = <. r , s >. -> ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
100 99 adantr 
 |-  ( ( 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 ) ) ) )
101 100 exlimivv 
 |-  ( 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 ) ) ) )
102 13 101 sylbi 
 |-  ( a = <. x , y >. -> ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
103 102 com3l 
 |-  ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( a = <. x , y >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
104 10 103 mpdd 
 |-  ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) )
105 104 adantr 
 |-  ( ( w = <. a , t >. /\ <. a , t >. = <. <. x , y >. , z >. ) -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) )
106 105 exlimivv 
 |-  ( 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 ) ) )
107 5 106 mpcom 
 |-  ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) )
108 19.8a 
 |-  ( ( w = <. <. x , y >. , z >. /\ ph ) -> E. z ( w = <. <. x , y >. , z >. /\ ph ) )
109 19.8a 
 |-  ( E. z ( w = <. <. x , y >. , z >. /\ ph ) -> E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
110 19.8a 
 |-  ( E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
111 108 109 110 3syl 
 |-  ( ( w = <. <. x , y >. , z >. /\ ph ) -> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
112 111 ex 
 |-  ( w = <. <. x , y >. , z >. -> ( ph -> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) ) )
113 107 112 impbid 
 |-  ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) <-> ph ) )
114 df-oprab 
 |-  { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
115 1 113 114 elab2 
 |-  ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )