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) (Revised by Gino Giotto, 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 syl6bi
 |-  ( 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 syl5bi
 |-  ( 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 syl5ibr
 |-  ( 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 syl5ibr
 |-  ( 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 syl5ibr
 |-  ( 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 syl6bi
 |-  ( 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 )