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

Theorem oprabid 6717
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 4962 . 2 ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ V
2 opex 4962 . . . . . 6 𝑥, 𝑦⟩ ∈ V
3 vex 3234 . . . . . 6 𝑧 ∈ V
42, 3eqvinop 4984 . . . . 5 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ∃𝑎𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
54biimpi 206 . . . 4 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ∃𝑎𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
6 eqeq1 2655 . . . . . . . 8 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
7 vex 3234 . . . . . . . . 9 𝑎 ∈ V
8 vex 3234 . . . . . . . . 9 𝑡 ∈ V
97, 8opth1 4973 . . . . . . . 8 (⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑎 = ⟨𝑥, 𝑦⟩)
106, 9syl6bi 243 . . . . . . 7 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑎 = ⟨𝑥, 𝑦⟩))
11 vex 3234 . . . . . . . . . 10 𝑥 ∈ V
12 vex 3234 . . . . . . . . . 10 𝑦 ∈ V
1311, 12eqvinop 4984 . . . . . . . . 9 (𝑎 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑟𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩))
14 opeq1 4433 . . . . . . . . . . . . 13 (𝑎 = ⟨𝑟, 𝑠⟩ → ⟨𝑎, 𝑡⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
1514eqeq2d 2661 . . . . . . . . . . . 12 (𝑎 = ⟨𝑟, 𝑠⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ ↔ 𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
1611, 12, 3otth2 4981 . . . . . . . . . . . . . . 15 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ (𝑥 = 𝑟𝑦 = 𝑠𝑧 = 𝑡))
17 euequ1 2504 . . . . . . . . . . . . . . . . . 18 ∃!𝑥 𝑥 = 𝑟
18 eupick 2565 . . . . . . . . . . . . . . . . . 18 ((∃!𝑥 𝑥 = 𝑟 ∧ ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
1917, 18mpan 706 . . . . . . . . . . . . . . . . 17 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
20 euequ1 2504 . . . . . . . . . . . . . . . . . . 19 ∃!𝑦 𝑦 = 𝑠
21 eupick 2565 . . . . . . . . . . . . . . . . . . 19 ((∃!𝑦 𝑦 = 𝑠 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡𝜑)))
2220, 21mpan 706 . . . . . . . . . . . . . . . . . 18 (∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡𝜑)))
23 euequ1 2504 . . . . . . . . . . . . . . . . . . 19 ∃!𝑧 𝑧 = 𝑡
24 eupick 2565 . . . . . . . . . . . . . . . . . . 19 ((∃!𝑧 𝑧 = 𝑡 ∧ ∃𝑧(𝑧 = 𝑡𝜑)) → (𝑧 = 𝑡𝜑))
2523, 24mpan 706 . . . . . . . . . . . . . . . . . 18 (∃𝑧(𝑧 = 𝑡𝜑) → (𝑧 = 𝑡𝜑))
2622, 25syl6 35 . . . . . . . . . . . . . . . . 17 (∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)) → (𝑦 = 𝑠 → (𝑧 = 𝑡𝜑)))
2719, 26syl6 35 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (𝑥 = 𝑟 → (𝑦 = 𝑠 → (𝑧 = 𝑡𝜑))))
28273impd 1303 . . . . . . . . . . . . . . 15 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → ((𝑥 = 𝑟𝑦 = 𝑠𝑧 = 𝑡) → 𝜑))
2916, 28syl5bi 232 . . . . . . . . . . . . . 14 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → 𝜑))
30 df-3an 1056 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝑟𝑦 = 𝑠𝑧 = 𝑡) ↔ ((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡))
3116, 30bitri 264 . . . . . . . . . . . . . . . . . 18 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ ((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡))
3231anbi1i 731 . . . . . . . . . . . . . . . . 17 ((⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ (((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑))
33 anass 682 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑) ↔ ((𝑥 = 𝑟𝑦 = 𝑠) ∧ (𝑧 = 𝑡𝜑)))
34 anass 682 . . . . . . . . . . . . . . . . 17 (((𝑥 = 𝑟𝑦 = 𝑠) ∧ (𝑧 = 𝑡𝜑)) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
3532, 33, 343bitri 286 . . . . . . . . . . . . . . . 16 ((⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
36353exbii 1816 . . . . . . . . . . . . . . 15 (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ ∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
37 nfcvf2 2818 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑥 𝑥 = 𝑧𝑧𝑥)
38 nfcvd 2794 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑥 𝑥 = 𝑧𝑧𝑟)
3937, 38nfeqd 2801 . . . . . . . . . . . . . . . . . . 19 (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧 𝑥 = 𝑟)
4039exdistrf 2364 . . . . . . . . . . . . . . . . . 18 (∃𝑥𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
4140eximi 1802 . . . . . . . . . . . . . . . . 17 (∃𝑦𝑥𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑦𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
42 excom 2082 . . . . . . . . . . . . . . . . 17 (∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) ↔ ∃𝑦𝑥𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
43 excom 2082 . . . . . . . . . . . . . . . . 17 (∃𝑥𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) ↔ ∃𝑦𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
4441, 42, 433imtr4i 281 . . . . . . . . . . . . . . . 16 (∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
45 nfcvf2 2818 . . . . . . . . . . . . . . . . . 18 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
46 nfcvd 2794 . . . . . . . . . . . . . . . . . 18 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑟)
4745, 46nfeqd 2801 . . . . . . . . . . . . . . . . 17 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑟)
4847exdistrf 2364 . . . . . . . . . . . . . . . 16 (∃𝑥𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
49 nfcvf2 2818 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑦 𝑦 = 𝑧𝑧𝑦)
50 nfcvd 2794 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑦 𝑦 = 𝑧𝑧𝑠)
5149, 50nfeqd 2801 . . . . . . . . . . . . . . . . . . 19 (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑦 = 𝑠)
5251exdistrf 2364 . . . . . . . . . . . . . . . . . 18 (∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)))
5352anim2i 592 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑟 ∧ ∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5453eximi 1802 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5544, 48, 543syl 18 . . . . . . . . . . . . . . 15 (∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5636, 55sylbi 207 . . . . . . . . . . . . . 14 (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5729, 56syl11 33 . . . . . . . . . . . . 13 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑))
58 eqeq1 2655 . . . . . . . . . . . . . . 15 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
59 eqcom 2658 . . . . . . . . . . . . . . 15 (⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
6058, 59syl6bb 276 . . . . . . . . . . . . . 14 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
6160anbi1d 741 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑)))
62613exbidv 1893 . . . . . . . . . . . . . . 15 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ ∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑)))
6362imbi1d 330 . . . . . . . . . . . . . 14 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑) ↔ (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑)))
6460, 63imbi12d 333 . . . . . . . . . . . . 13 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)) ↔ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑))))
6557, 64mpbiri 248 . . . . . . . . . . . 12 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
6615, 65syl6bi 243 . . . . . . . . . . 11 (𝑎 = ⟨𝑟, 𝑠⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
6766adantr 480 . . . . . . . . . 10 ((𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩) → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
6867exlimivv 1900 . . . . . . . . 9 (∃𝑟𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩) → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
6913, 68sylbi 207 . . . . . . . 8 (𝑎 = ⟨𝑥, 𝑦⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
7069com3l 89 . . . . . . 7 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝑎 = ⟨𝑥, 𝑦⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
7110, 70mpdd 43 . . . . . 6 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
7271adantr 480 . . . . 5 ((𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
7372exlimivv 1900 . . . 4 (∃𝑎𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
745, 73mpcom 38 . . 3 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))
75 19.8a 2090 . . . . 5 ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
76 19.8a 2090 . . . . 5 (∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
77 19.8a 2090 . . . . 5 (∃𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
7875, 76, 773syl 18 . . . 4 ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
7978ex 449 . . 3 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝜑 → ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)))
8074, 79impbid 202 . 2 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ 𝜑))
81 df-oprab 6694 . 2 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
821, 80, 81elab2 3386 1 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054  wal 1521   = wceq 1523  wex 1744  wcel 2030  ∃!weu 2498  cop 4216  {coprab 6691
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-oprab 6694
This theorem is referenced by:  ssoprab2b  6754  ovid  6819  ovidig  6820  tposoprab  7433  xpcomco  8091
  Copyright terms: Public domain W3C validator