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

Theorem oprabid 7203
Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker oprabidw 7202 when possible. (Contributed by Mario Carneiro, 20-Mar-2013.) (New usage is discouraged.)
Assertion
Ref Expression
oprabid (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)

Proof of Theorem oprabid
Dummy variables 𝑎 𝑟 𝑠 𝑡 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opex 5323 . 2 ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ V
2 opex 5323 . . . . . 6 𝑥, 𝑦⟩ ∈ V
3 vex 3402 . . . . . 6 𝑧 ∈ V
42, 3eqvinop 5345 . . . . 5 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ∃𝑎𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
54biimpi 219 . . . 4 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ∃𝑎𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
6 eqeq1 2742 . . . . . . . 8 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
7 vex 3402 . . . . . . . . 9 𝑎 ∈ V
8 vex 3402 . . . . . . . . 9 𝑡 ∈ V
97, 8opth1 5334 . . . . . . . 8 (⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑎 = ⟨𝑥, 𝑦⟩)
106, 9syl6bi 256 . . . . . . 7 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑎 = ⟨𝑥, 𝑦⟩))
11 vex 3402 . . . . . . . . . 10 𝑥 ∈ V
12 vex 3402 . . . . . . . . . 10 𝑦 ∈ V
1311, 12eqvinop 5345 . . . . . . . . 9 (𝑎 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑟𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩))
14 opeq1 4760 . . . . . . . . . . . . 13 (𝑎 = ⟨𝑟, 𝑠⟩ → ⟨𝑎, 𝑡⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
1514eqeq2d 2749 . . . . . . . . . . . 12 (𝑎 = ⟨𝑟, 𝑠⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ ↔ 𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
1611, 12, 3otth2 5342 . . . . . . . . . . . . . . 15 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ (𝑥 = 𝑟𝑦 = 𝑠𝑧 = 𝑡))
17 euequ 2598 . . . . . . . . . . . . . . . . . 18 ∃!𝑥 𝑥 = 𝑟
18 eupick 2636 . . . . . . . . . . . . . . . . . 18 ((∃!𝑥 𝑥 = 𝑟 ∧ ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
1917, 18mpan 690 . . . . . . . . . . . . . . . . 17 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
20 euequ 2598 . . . . . . . . . . . . . . . . . . 19 ∃!𝑦 𝑦 = 𝑠
21 eupick 2636 . . . . . . . . . . . . . . . . . . 19 ((∃!𝑦 𝑦 = 𝑠 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡𝜑)))
2220, 21mpan 690 . . . . . . . . . . . . . . . . . 18 (∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡𝜑)))
23 euequ 2598 . . . . . . . . . . . . . . . . . . 19 ∃!𝑧 𝑧 = 𝑡
24 eupick 2636 . . . . . . . . . . . . . . . . . . 19 ((∃!𝑧 𝑧 = 𝑡 ∧ ∃𝑧(𝑧 = 𝑡𝜑)) → (𝑧 = 𝑡𝜑))
2523, 24mpan 690 . . . . . . . . . . . . . . . . . 18 (∃𝑧(𝑧 = 𝑡𝜑) → (𝑧 = 𝑡𝜑))
2622, 25syl6 35 . . . . . . . . . . . . . . . . 17 (∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)) → (𝑦 = 𝑠 → (𝑧 = 𝑡𝜑)))
2719, 26syl6 35 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (𝑥 = 𝑟 → (𝑦 = 𝑠 → (𝑧 = 𝑡𝜑))))
28273impd 1349 . . . . . . . . . . . . . . 15 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → ((𝑥 = 𝑟𝑦 = 𝑠𝑧 = 𝑡) → 𝜑))
2916, 28syl5bi 245 . . . . . . . . . . . . . 14 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → 𝜑))
30 df-3an 1090 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝑟𝑦 = 𝑠𝑧 = 𝑡) ↔ ((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡))
3116, 30bitri 278 . . . . . . . . . . . . . . . . . 18 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ ((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡))
3231anbi1i 627 . . . . . . . . . . . . . . . . 17 ((⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ (((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑))
33 anass 472 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑) ↔ ((𝑥 = 𝑟𝑦 = 𝑠) ∧ (𝑧 = 𝑡𝜑)))
34 anass 472 . . . . . . . . . . . . . . . . 17 (((𝑥 = 𝑟𝑦 = 𝑠) ∧ (𝑧 = 𝑡𝜑)) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
3532, 33, 343bitri 300 . . . . . . . . . . . . . . . 16 ((⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
36353exbii 1856 . . . . . . . . . . . . . . 15 (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ ∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
37 nfcvf2 2929 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑥 𝑥 = 𝑧𝑧𝑥)
38 nfcvd 2900 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑥 𝑥 = 𝑧𝑧𝑟)
3937, 38nfeqd 2909 . . . . . . . . . . . . . . . . . . 19 (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧 𝑥 = 𝑟)
4039exdistrf 2446 . . . . . . . . . . . . . . . . . 18 (∃𝑥𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
4140eximi 1841 . . . . . . . . . . . . . . . . 17 (∃𝑦𝑥𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑦𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
42 excom 2169 . . . . . . . . . . . . . . . . 17 (∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) ↔ ∃𝑦𝑥𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
43 excom 2169 . . . . . . . . . . . . . . . . 17 (∃𝑥𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) ↔ ∃𝑦𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
4441, 42, 433imtr4i 295 . . . . . . . . . . . . . . . 16 (∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
45 nfcvf2 2929 . . . . . . . . . . . . . . . . . 18 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
46 nfcvd 2900 . . . . . . . . . . . . . . . . . 18 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑟)
4745, 46nfeqd 2909 . . . . . . . . . . . . . . . . 17 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑟)
4847exdistrf 2446 . . . . . . . . . . . . . . . 16 (∃𝑥𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
49 nfcvf2 2929 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑦 𝑦 = 𝑧𝑧𝑦)
50 nfcvd 2900 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑦 𝑦 = 𝑧𝑧𝑠)
5149, 50nfeqd 2909 . . . . . . . . . . . . . . . . . . 19 (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑦 = 𝑠)
5251exdistrf 2446 . . . . . . . . . . . . . . . . . 18 (∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)))
5352anim2i 620 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑟 ∧ ∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5453eximi 1841 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5544, 48, 543syl 18 . . . . . . . . . . . . . . 15 (∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5636, 55sylbi 220 . . . . . . . . . . . . . 14 (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5729, 56syl11 33 . . . . . . . . . . . . 13 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑))
58 eqeq1 2742 . . . . . . . . . . . . . . 15 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
59 eqcom 2745 . . . . . . . . . . . . . . 15 (⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
6058, 59bitrdi 290 . . . . . . . . . . . . . 14 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
6160anbi1d 633 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑)))
62613exbidv 1931 . . . . . . . . . . . . . . 15 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ ∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑)))
6362imbi1d 345 . . . . . . . . . . . . . 14 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑) ↔ (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑)))
6460, 63imbi12d 348 . . . . . . . . . . . . 13 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)) ↔ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑))))
6557, 64mpbiri 261 . . . . . . . . . . . 12 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
6615, 65syl6bi 256 . . . . . . . . . . 11 (𝑎 = ⟨𝑟, 𝑠⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
6766adantr 484 . . . . . . . . . 10 ((𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩) → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
6867exlimivv 1938 . . . . . . . . 9 (∃𝑟𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩) → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
6913, 68sylbi 220 . . . . . . . 8 (𝑎 = ⟨𝑥, 𝑦⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
7069com3l 89 . . . . . . 7 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝑎 = ⟨𝑥, 𝑦⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
7110, 70mpdd 43 . . . . . 6 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
7271adantr 484 . . . . 5 ((𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
7372exlimivv 1938 . . . 4 (∃𝑎𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
745, 73mpcom 38 . . 3 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))
75 19.8a 2181 . . . . 5 ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
76 19.8a 2181 . . . . 5 (∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
77 19.8a 2181 . . . . 5 (∃𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
7875, 76, 773syl 18 . . . 4 ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
7978ex 416 . . 3 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝜑 → ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)))
8074, 79impbid 215 . 2 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ 𝜑))
81 df-oprab 7175 . 2 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
821, 80, 81elab2 3577 1 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1088  wal 1540   = wceq 1542  wex 1786  wcel 2113  ∃!weu 2569  cop 4523  {coprab 7172
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-13 2371  ax-ext 2710  ax-sep 5168  ax-nul 5175  ax-pr 5297
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-v 3400  df-dif 3847  df-un 3849  df-nul 4213  df-if 4416  df-sn 4518  df-pr 4520  df-op 4524  df-oprab 7175
This theorem is referenced by:  ssoprab2b  7238
  Copyright terms: Public domain W3C validator