MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oprabid Structured version   Visualization version   GIF version

Theorem oprabid 6901
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 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)

Proof of Theorem oprabid
Dummy variables 𝑎 𝑟 𝑠 𝑡 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opex 5122 . 2 ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ V
2 opex 5122 . . . . . 6 𝑥, 𝑦⟩ ∈ V
3 vex 3394 . . . . . 6 𝑧 ∈ V
42, 3eqvinop 5144 . . . . 5 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ∃𝑎𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
54biimpi 207 . . . 4 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ∃𝑎𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
6 eqeq1 2810 . . . . . . . 8 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
7 vex 3394 . . . . . . . . 9 𝑎 ∈ V
8 vex 3394 . . . . . . . . 9 𝑡 ∈ V
97, 8opth1 5133 . . . . . . . 8 (⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑎 = ⟨𝑥, 𝑦⟩)
106, 9syl6bi 244 . . . . . . 7 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑎 = ⟨𝑥, 𝑦⟩))
11 vex 3394 . . . . . . . . . 10 𝑥 ∈ V
12 vex 3394 . . . . . . . . . 10 𝑦 ∈ V
1311, 12eqvinop 5144 . . . . . . . . 9 (𝑎 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑟𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩))
14 opeq1 4595 . . . . . . . . . . . . 13 (𝑎 = ⟨𝑟, 𝑠⟩ → ⟨𝑎, 𝑡⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
1514eqeq2d 2816 . . . . . . . . . . . 12 (𝑎 = ⟨𝑟, 𝑠⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ ↔ 𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
1611, 12, 3otth2 5141 . . . . . . . . . . . . . . 15 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ (𝑥 = 𝑟𝑦 = 𝑠𝑧 = 𝑡))
17 euequi 2638 . . . . . . . . . . . . . . . . . 18 ∃!𝑥 𝑥 = 𝑟
18 eupick 2700 . . . . . . . . . . . . . . . . . 18 ((∃!𝑥 𝑥 = 𝑟 ∧ ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
1917, 18mpan 673 . . . . . . . . . . . . . . . . 17 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
20 euequi 2638 . . . . . . . . . . . . . . . . . . 19 ∃!𝑦 𝑦 = 𝑠
21 eupick 2700 . . . . . . . . . . . . . . . . . . 19 ((∃!𝑦 𝑦 = 𝑠 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡𝜑)))
2220, 21mpan 673 . . . . . . . . . . . . . . . . . 18 (∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡𝜑)))
23 euequi 2638 . . . . . . . . . . . . . . . . . . 19 ∃!𝑧 𝑧 = 𝑡
24 eupick 2700 . . . . . . . . . . . . . . . . . . 19 ((∃!𝑧 𝑧 = 𝑡 ∧ ∃𝑧(𝑧 = 𝑡𝜑)) → (𝑧 = 𝑡𝜑))
2523, 24mpan 673 . . . . . . . . . . . . . . . . . 18 (∃𝑧(𝑧 = 𝑡𝜑) → (𝑧 = 𝑡𝜑))
2622, 25syl6 35 . . . . . . . . . . . . . . . . 17 (∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)) → (𝑦 = 𝑠 → (𝑧 = 𝑡𝜑)))
2719, 26syl6 35 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (𝑥 = 𝑟 → (𝑦 = 𝑠 → (𝑧 = 𝑡𝜑))))
28273impd 1450 . . . . . . . . . . . . . . 15 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → ((𝑥 = 𝑟𝑦 = 𝑠𝑧 = 𝑡) → 𝜑))
2916, 28syl5bi 233 . . . . . . . . . . . . . 14 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → 𝜑))
30 df-3an 1102 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝑟𝑦 = 𝑠𝑧 = 𝑡) ↔ ((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡))
3116, 30bitri 266 . . . . . . . . . . . . . . . . . 18 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ ((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡))
3231anbi1i 612 . . . . . . . . . . . . . . . . 17 ((⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ (((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑))
33 anass 456 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑) ↔ ((𝑥 = 𝑟𝑦 = 𝑠) ∧ (𝑧 = 𝑡𝜑)))
34 anass 456 . . . . . . . . . . . . . . . . 17 (((𝑥 = 𝑟𝑦 = 𝑠) ∧ (𝑧 = 𝑡𝜑)) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
3532, 33, 343bitri 288 . . . . . . . . . . . . . . . 16 ((⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
36353exbii 1935 . . . . . . . . . . . . . . 15 (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ ∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
37 nfcvf2 2973 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑥 𝑥 = 𝑧𝑧𝑥)
38 nfcvd 2949 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑥 𝑥 = 𝑧𝑧𝑟)
3937, 38nfeqd 2956 . . . . . . . . . . . . . . . . . . 19 (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧 𝑥 = 𝑟)
4039exdistrf 2495 . . . . . . . . . . . . . . . . . 18 (∃𝑥𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
4140eximi 1919 . . . . . . . . . . . . . . . . 17 (∃𝑦𝑥𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑦𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
42 excom 2209 . . . . . . . . . . . . . . . . 17 (∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) ↔ ∃𝑦𝑥𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
43 excom 2209 . . . . . . . . . . . . . . . . 17 (∃𝑥𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) ↔ ∃𝑦𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
4441, 42, 433imtr4i 283 . . . . . . . . . . . . . . . 16 (∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
45 nfcvf2 2973 . . . . . . . . . . . . . . . . . 18 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
46 nfcvd 2949 . . . . . . . . . . . . . . . . . 18 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑟)
4745, 46nfeqd 2956 . . . . . . . . . . . . . . . . 17 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑟)
4847exdistrf 2495 . . . . . . . . . . . . . . . 16 (∃𝑥𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
49 nfcvf2 2973 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑦 𝑦 = 𝑧𝑧𝑦)
50 nfcvd 2949 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑦 𝑦 = 𝑧𝑧𝑠)
5149, 50nfeqd 2956 . . . . . . . . . . . . . . . . . . 19 (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑦 = 𝑠)
5251exdistrf 2495 . . . . . . . . . . . . . . . . . 18 (∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)))
5352anim2i 605 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑟 ∧ ∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5453eximi 1919 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5544, 48, 543syl 18 . . . . . . . . . . . . . . 15 (∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5636, 55sylbi 208 . . . . . . . . . . . . . 14 (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5729, 56syl11 33 . . . . . . . . . . . . 13 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑))
58 eqeq1 2810 . . . . . . . . . . . . . . 15 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
59 eqcom 2813 . . . . . . . . . . . . . . 15 (⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
6058, 59syl6bb 278 . . . . . . . . . . . . . 14 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
6160anbi1d 617 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑)))
62613exbidv 2016 . . . . . . . . . . . . . . 15 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ ∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑)))
6362imbi1d 332 . . . . . . . . . . . . . 14 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑) ↔ (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑)))
6460, 63imbi12d 335 . . . . . . . . . . . . 13 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)) ↔ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑))))
6557, 64mpbiri 249 . . . . . . . . . . . 12 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
6615, 65syl6bi 244 . . . . . . . . . . 11 (𝑎 = ⟨𝑟, 𝑠⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
6766adantr 468 . . . . . . . . . 10 ((𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩) → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
6867exlimivv 2023 . . . . . . . . 9 (∃𝑟𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩) → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
6913, 68sylbi 208 . . . . . . . 8 (𝑎 = ⟨𝑥, 𝑦⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
7069com3l 89 . . . . . . 7 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝑎 = ⟨𝑥, 𝑦⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
7110, 70mpdd 43 . . . . . 6 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
7271adantr 468 . . . . 5 ((𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
7372exlimivv 2023 . . . 4 (∃𝑎𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
745, 73mpcom 38 . . 3 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))
75 19.8a 2217 . . . . 5 ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
76 19.8a 2217 . . . . 5 (∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
77 19.8a 2217 . . . . 5 (∃𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
7875, 76, 773syl 18 . . . 4 ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
7978ex 399 . . 3 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝜑 → ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)))
8074, 79impbid 203 . 2 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ 𝜑))
81 df-oprab 6874 . 2 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
821, 80, 81elab2 3549 1 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100  wal 1635   = wceq 1637  wex 1859  wcel 2156  ∃!weu 2630  cop 4376  {coprab 6871
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-oprab 6874
This theorem is referenced by:  ssoprab2b  6938  ovid  7003  ovidig  7004  tposoprab  7619  xpcomco  8285
  Copyright terms: Public domain W3C validator