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

Theorem oprabid 7307
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 2372. Use the weaker oprabidw 7306 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 5379 . 2 ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ V
2 opex 5379 . . . . . 6 𝑥, 𝑦⟩ ∈ V
3 vex 3436 . . . . . 6 𝑧 ∈ V
42, 3eqvinop 5401 . . . . 5 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ∃𝑎𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
54biimpi 215 . . . 4 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ∃𝑎𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
6 eqeq1 2742 . . . . . . . 8 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
7 vex 3436 . . . . . . . . 9 𝑎 ∈ V
8 vex 3436 . . . . . . . . 9 𝑡 ∈ V
97, 8opth1 5390 . . . . . . . 8 (⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑎 = ⟨𝑥, 𝑦⟩)
106, 9syl6bi 252 . . . . . . 7 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑎 = ⟨𝑥, 𝑦⟩))
11 vex 3436 . . . . . . . . . 10 𝑥 ∈ V
12 vex 3436 . . . . . . . . . 10 𝑦 ∈ V
1311, 12eqvinop 5401 . . . . . . . . 9 (𝑎 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑟𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩))
14 opeq1 4804 . . . . . . . . . . . . 13 (𝑎 = ⟨𝑟, 𝑠⟩ → ⟨𝑎, 𝑡⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
1514eqeq2d 2749 . . . . . . . . . . . 12 (𝑎 = ⟨𝑟, 𝑠⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ ↔ 𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
1611, 12, 3otth2 5398 . . . . . . . . . . . . . . 15 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ (𝑥 = 𝑟𝑦 = 𝑠𝑧 = 𝑡))
17 euequ 2597 . . . . . . . . . . . . . . . . . 18 ∃!𝑥 𝑥 = 𝑟
18 eupick 2635 . . . . . . . . . . . . . . . . . 18 ((∃!𝑥 𝑥 = 𝑟 ∧ ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
1917, 18mpan 687 . . . . . . . . . . . . . . . . 17 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
20 euequ 2597 . . . . . . . . . . . . . . . . . . 19 ∃!𝑦 𝑦 = 𝑠
21 eupick 2635 . . . . . . . . . . . . . . . . . . 19 ((∃!𝑦 𝑦 = 𝑠 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡𝜑)))
2220, 21mpan 687 . . . . . . . . . . . . . . . . . 18 (∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡𝜑)))
23 euequ 2597 . . . . . . . . . . . . . . . . . . 19 ∃!𝑧 𝑧 = 𝑡
24 eupick 2635 . . . . . . . . . . . . . . . . . . 19 ((∃!𝑧 𝑧 = 𝑡 ∧ ∃𝑧(𝑧 = 𝑡𝜑)) → (𝑧 = 𝑡𝜑))
2523, 24mpan 687 . . . . . . . . . . . . . . . . . 18 (∃𝑧(𝑧 = 𝑡𝜑) → (𝑧 = 𝑡𝜑))
2622, 25syl6 35 . . . . . . . . . . . . . . . . 17 (∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)) → (𝑦 = 𝑠 → (𝑧 = 𝑡𝜑)))
2719, 26syl6 35 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (𝑥 = 𝑟 → (𝑦 = 𝑠 → (𝑧 = 𝑡𝜑))))
28273impd 1347 . . . . . . . . . . . . . . 15 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → ((𝑥 = 𝑟𝑦 = 𝑠𝑧 = 𝑡) → 𝜑))
2916, 28syl5bi 241 . . . . . . . . . . . . . 14 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → 𝜑))
30 df-3an 1088 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝑟𝑦 = 𝑠𝑧 = 𝑡) ↔ ((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡))
3116, 30bitri 274 . . . . . . . . . . . . . . . . . 18 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ ((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡))
3231anbi1i 624 . . . . . . . . . . . . . . . . 17 ((⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ (((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑))
33 anass 469 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑) ↔ ((𝑥 = 𝑟𝑦 = 𝑠) ∧ (𝑧 = 𝑡𝜑)))
34 anass 469 . . . . . . . . . . . . . . . . 17 (((𝑥 = 𝑟𝑦 = 𝑠) ∧ (𝑧 = 𝑡𝜑)) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
3532, 33, 343bitri 297 . . . . . . . . . . . . . . . 16 ((⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
36353exbii 1852 . . . . . . . . . . . . . . 15 (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ ∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
37 nfcvf2 2937 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑥 𝑥 = 𝑧𝑧𝑥)
38 nfcvd 2908 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑥 𝑥 = 𝑧𝑧𝑟)
3937, 38nfeqd 2917 . . . . . . . . . . . . . . . . . . 19 (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧 𝑥 = 𝑟)
4039exdistrf 2447 . . . . . . . . . . . . . . . . . 18 (∃𝑥𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
4140eximi 1837 . . . . . . . . . . . . . . . . 17 (∃𝑦𝑥𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑦𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
42 excom 2162 . . . . . . . . . . . . . . . . 17 (∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) ↔ ∃𝑦𝑥𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
43 excom 2162 . . . . . . . . . . . . . . . . 17 (∃𝑥𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) ↔ ∃𝑦𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
4441, 42, 433imtr4i 292 . . . . . . . . . . . . . . . 16 (∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
45 nfcvf2 2937 . . . . . . . . . . . . . . . . . 18 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
46 nfcvd 2908 . . . . . . . . . . . . . . . . . 18 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑟)
4745, 46nfeqd 2917 . . . . . . . . . . . . . . . . 17 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑟)
4847exdistrf 2447 . . . . . . . . . . . . . . . 16 (∃𝑥𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
49 nfcvf2 2937 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑦 𝑦 = 𝑧𝑧𝑦)
50 nfcvd 2908 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑦 𝑦 = 𝑧𝑧𝑠)
5149, 50nfeqd 2917 . . . . . . . . . . . . . . . . . . 19 (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑦 = 𝑠)
5251exdistrf 2447 . . . . . . . . . . . . . . . . . 18 (∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)))
5352anim2i 617 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑟 ∧ ∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5453eximi 1837 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5544, 48, 543syl 18 . . . . . . . . . . . . . . 15 (∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5636, 55sylbi 216 . . . . . . . . . . . . . 14 (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
5729, 56syl11 33 . . . . . . . . . . . . 13 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑))
58 eqeq1 2742 . . . . . . . . . . . . . . 15 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
59 eqcom 2745 . . . . . . . . . . . . . . 15 (⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
6058, 59bitrdi 287 . . . . . . . . . . . . . 14 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
6160anbi1d 630 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑)))
62613exbidv 1928 . . . . . . . . . . . . . . 15 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ ∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑)))
6362imbi1d 342 . . . . . . . . . . . . . 14 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑) ↔ (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑)))
6460, 63imbi12d 345 . . . . . . . . . . . . 13 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)) ↔ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑))))
6557, 64mpbiri 257 . . . . . . . . . . . 12 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
6615, 65syl6bi 252 . . . . . . . . . . 11 (𝑎 = ⟨𝑟, 𝑠⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
6766adantr 481 . . . . . . . . . 10 ((𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩) → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
6867exlimivv 1935 . . . . . . . . 9 (∃𝑟𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩) → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
6913, 68sylbi 216 . . . . . . . 8 (𝑎 = ⟨𝑥, 𝑦⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
7069com3l 89 . . . . . . 7 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝑎 = ⟨𝑥, 𝑦⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
7110, 70mpdd 43 . . . . . 6 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
7271adantr 481 . . . . 5 ((𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
7372exlimivv 1935 . . . 4 (∃𝑎𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
745, 73mpcom 38 . . 3 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))
75 19.8a 2174 . . . . 5 ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
76 19.8a 2174 . . . . 5 (∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
77 19.8a 2174 . . . . 5 (∃𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
7875, 76, 773syl 18 . . . 4 ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
7978ex 413 . . 3 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝜑 → ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)))
8074, 79impbid 211 . 2 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ 𝜑))
81 df-oprab 7279 . 2 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
821, 80, 81elab2 3613 1 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086  wal 1537   = wceq 1539  wex 1782  wcel 2106  ∃!weu 2568  cop 4567  {coprab 7276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2372  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-oprab 7279
This theorem is referenced by:  ssoprab2b  7344
  Copyright terms: Public domain W3C validator