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

Theorem oprabid 6554
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 4853 . 2 ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ V
2 opex 4853 . . . . . 6 𝑥, 𝑦⟩ ∈ V
3 vex 3176 . . . . . 6 𝑧 ∈ V
42, 3eqvinop 4875 . . . . 5 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ∃𝑎𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
54biimpi 205 . . . 4 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ∃𝑎𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
6 eqeq1 2614 . . . . . . . 8 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
7 vex 3176 . . . . . . . . 9 𝑎 ∈ V
8 vex 3176 . . . . . . . . 9 𝑡 ∈ V
97, 8opth1 4864 . . . . . . . 8 (⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑎 = ⟨𝑥, 𝑦⟩)
106, 9syl6bi 242 . . . . . . 7 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑎 = ⟨𝑥, 𝑦⟩))
11 vex 3176 . . . . . . . . . 10 𝑥 ∈ V
12 vex 3176 . . . . . . . . . 10 𝑦 ∈ V
1311, 12eqvinop 4875 . . . . . . . . 9 (𝑎 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑟𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩))
14 opeq1 4335 . . . . . . . . . . . . 13 (𝑎 = ⟨𝑟, 𝑠⟩ → ⟨𝑎, 𝑡⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
1514eqeq2d 2620 . . . . . . . . . . . 12 (𝑎 = ⟨𝑟, 𝑠⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ ↔ 𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
1611, 12, 3otth2 4872 . . . . . . . . . . . . . . . . . . 19 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ (𝑥 = 𝑟𝑦 = 𝑠𝑧 = 𝑡))
17 df-3an 1033 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝑟𝑦 = 𝑠𝑧 = 𝑡) ↔ ((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡))
1816, 17bitri 263 . . . . . . . . . . . . . . . . . 18 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ ((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡))
1918anbi1i 727 . . . . . . . . . . . . . . . . 17 ((⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ (((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑))
20 anass 679 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑟𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑) ↔ ((𝑥 = 𝑟𝑦 = 𝑠) ∧ (𝑧 = 𝑡𝜑)))
21 anass 679 . . . . . . . . . . . . . . . . 17 (((𝑥 = 𝑟𝑦 = 𝑠) ∧ (𝑧 = 𝑡𝜑)) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
2219, 20, 213bitri 285 . . . . . . . . . . . . . . . 16 ((⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
23223exbii 1766 . . . . . . . . . . . . . . 15 (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ ∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
24 nfcvf2 2775 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑥 𝑥 = 𝑧𝑧𝑥)
25 nfcvd 2752 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑥 𝑥 = 𝑧𝑧𝑟)
2624, 25nfeqd 2758 . . . . . . . . . . . . . . . . . . 19 (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧 𝑥 = 𝑟)
2726exdistrf 2321 . . . . . . . . . . . . . . . . . 18 (∃𝑥𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
2827eximi 1752 . . . . . . . . . . . . . . . . 17 (∃𝑦𝑥𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑦𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
29 excom 2029 . . . . . . . . . . . . . . . . 17 (∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) ↔ ∃𝑦𝑥𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
30 excom 2029 . . . . . . . . . . . . . . . . 17 (∃𝑥𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) ↔ ∃𝑦𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
3128, 29, 303imtr4i 280 . . . . . . . . . . . . . . . 16 (∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
32 nfcvf2 2775 . . . . . . . . . . . . . . . . . 18 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
33 nfcvd 2752 . . . . . . . . . . . . . . . . . 18 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑟)
3432, 33nfeqd 2758 . . . . . . . . . . . . . . . . 17 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑟)
3534exdistrf 2321 . . . . . . . . . . . . . . . 16 (∃𝑥𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))))
36 nfcvf2 2775 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑦 𝑦 = 𝑧𝑧𝑦)
37 nfcvd 2752 . . . . . . . . . . . . . . . . . . . 20 (¬ ∀𝑦 𝑦 = 𝑧𝑧𝑠)
3836, 37nfeqd 2758 . . . . . . . . . . . . . . . . . . 19 (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑦 = 𝑠)
3938exdistrf 2321 . . . . . . . . . . . . . . . . . 18 (∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)))
4039anim2i 591 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑟 ∧ ∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
4140eximi 1752 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
4231, 35, 413syl 18 . . . . . . . . . . . . . . 15 (∃𝑥𝑦𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
4323, 42sylbi 206 . . . . . . . . . . . . . 14 (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
44 euequ1 2464 . . . . . . . . . . . . . . . . . . 19 ∃!𝑥 𝑥 = 𝑟
45 eupick 2524 . . . . . . . . . . . . . . . . . . 19 ((∃!𝑥 𝑥 = 𝑟 ∧ ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
4644, 45mpan 702 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))))
47 euequ1 2464 . . . . . . . . . . . . . . . . . . . 20 ∃!𝑦 𝑦 = 𝑠
48 eupick 2524 . . . . . . . . . . . . . . . . . . . 20 ((∃!𝑦 𝑦 = 𝑠 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡𝜑)))
4947, 48mpan 702 . . . . . . . . . . . . . . . . . . 19 (∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡𝜑)))
50 euequ1 2464 . . . . . . . . . . . . . . . . . . . 20 ∃!𝑧 𝑧 = 𝑡
51 eupick 2524 . . . . . . . . . . . . . . . . . . . 20 ((∃!𝑧 𝑧 = 𝑡 ∧ ∃𝑧(𝑧 = 𝑡𝜑)) → (𝑧 = 𝑡𝜑))
5250, 51mpan 702 . . . . . . . . . . . . . . . . . . 19 (∃𝑧(𝑧 = 𝑡𝜑) → (𝑧 = 𝑡𝜑))
5349, 52syl6 34 . . . . . . . . . . . . . . . . . 18 (∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑)) → (𝑦 = 𝑠 → (𝑧 = 𝑡𝜑)))
5446, 53syl6 34 . . . . . . . . . . . . . . . . 17 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (𝑥 = 𝑟 → (𝑦 = 𝑠 → (𝑧 = 𝑡𝜑))))
55543impd 1273 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → ((𝑥 = 𝑟𝑦 = 𝑠𝑧 = 𝑡) → 𝜑))
5616, 55syl5bi 231 . . . . . . . . . . . . . . 15 (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → 𝜑))
5756com12 32 . . . . . . . . . . . . . 14 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡𝜑))) → 𝜑))
5843, 57syl5 33 . . . . . . . . . . . . 13 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑))
59 eqeq1 2614 . . . . . . . . . . . . . . 15 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
60 eqcom 2617 . . . . . . . . . . . . . . 15 (⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
6159, 60syl6bb 275 . . . . . . . . . . . . . 14 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
6261anbi1d 737 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑)))
63623exbidv 1840 . . . . . . . . . . . . . . 15 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ ∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑)))
6463imbi1d 330 . . . . . . . . . . . . . 14 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑) ↔ (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑)))
6561, 64imbi12d 333 . . . . . . . . . . . . 13 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)) ↔ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥𝑦𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑))))
6658, 65mpbiri 247 . . . . . . . . . . . 12 (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
6715, 66syl6bi 242 . . . . . . . . . . 11 (𝑎 = ⟨𝑟, 𝑠⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
6867adantr 480 . . . . . . . . . 10 ((𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩) → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
6968exlimivv 1847 . . . . . . . . 9 (∃𝑟𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩) → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
7013, 69sylbi 206 . . . . . . . 8 (𝑎 = ⟨𝑥, 𝑦⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
7170com3l 87 . . . . . . 7 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝑎 = ⟨𝑥, 𝑦⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
7210, 71mpdd 42 . . . . . 6 (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
7372adantr 480 . . . . 5 ((𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
7473exlimivv 1847 . . . 4 (∃𝑎𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
755, 74mpcom 37 . . 3 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))
76 19.8a 2039 . . . . 5 ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
77 19.8a 2039 . . . . 5 (∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
78 19.8a 2039 . . . . 5 (∃𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
7976, 77, 783syl 18 . . . 4 ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
8079ex 449 . . 3 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝜑 → ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)))
8175, 80impbid 201 . 2 (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ 𝜑))
82 df-oprab 6531 . 2 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
831, 81, 82elab2 3323 1 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383  w3a 1031  wal 1473   = wceq 1475  wex 1695  wcel 1977  ∃!weu 2458  cop 4131  {coprab 6528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-oprab 6531
This theorem is referenced by:  ssoprab2b  6588  ovid  6653  ovidig  6654  tposoprab  7253  xpcomco  7913
  Copyright terms: Public domain W3C validator