Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  elvvv GIF version

Theorem elvvv 4648
 Description: Membership in universal class of ordered triples. (Contributed by NM, 17-Dec-2008.)
Assertion
Ref Expression
elvvv (𝐴 ∈ ((V × V) × V) ↔ ∃𝑥𝑦𝑧 𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
Distinct variable group:   𝑥,𝑦,𝑧,𝐴

Proof of Theorem elvvv
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 elxp 4602 . 2 (𝐴 ∈ ((V × V) × V) ↔ ∃𝑤𝑧(𝐴 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 ∈ (V × V) ∧ 𝑧 ∈ V)))
2 anass 399 . . . . 5 (((𝐴 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 ∈ (V × V)) ∧ 𝑧 ∈ V) ↔ (𝐴 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 ∈ (V × V) ∧ 𝑧 ∈ V)))
3 19.42vv 1891 . . . . . 6 (∃𝑥𝑦(𝐴 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ↔ (𝐴 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥𝑦 𝑤 = ⟨𝑥, 𝑦⟩))
4 ancom 264 . . . . . . 7 ((𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝐴 = ⟨𝑤, 𝑧⟩) ↔ (𝐴 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩))
542exbii 1586 . . . . . 6 (∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝐴 = ⟨𝑤, 𝑧⟩) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩))
6 vex 2715 . . . . . . . 8 𝑧 ∈ V
76biantru 300 . . . . . . 7 ((𝐴 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 ∈ (V × V)) ↔ ((𝐴 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 ∈ (V × V)) ∧ 𝑧 ∈ V))
8 elvv 4647 . . . . . . . 8 (𝑤 ∈ (V × V) ↔ ∃𝑥𝑦 𝑤 = ⟨𝑥, 𝑦⟩)
98anbi2i 453 . . . . . . 7 ((𝐴 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 ∈ (V × V)) ↔ (𝐴 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥𝑦 𝑤 = ⟨𝑥, 𝑦⟩))
107, 9bitr3i 185 . . . . . 6 (((𝐴 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 ∈ (V × V)) ∧ 𝑧 ∈ V) ↔ (𝐴 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥𝑦 𝑤 = ⟨𝑥, 𝑦⟩))
113, 5, 103bitr4ri 212 . . . . 5 (((𝐴 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 ∈ (V × V)) ∧ 𝑧 ∈ V) ↔ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝐴 = ⟨𝑤, 𝑧⟩))
122, 11bitr3i 185 . . . 4 ((𝐴 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 ∈ (V × V) ∧ 𝑧 ∈ V)) ↔ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝐴 = ⟨𝑤, 𝑧⟩))
13122exbii 1586 . . 3 (∃𝑤𝑧(𝐴 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 ∈ (V × V) ∧ 𝑧 ∈ V)) ↔ ∃𝑤𝑧𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝐴 = ⟨𝑤, 𝑧⟩))
14 exrot4 1671 . . . 4 (∃𝑥𝑦𝑤𝑧(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝐴 = ⟨𝑤, 𝑧⟩) ↔ ∃𝑤𝑧𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝐴 = ⟨𝑤, 𝑧⟩))
15 excom 1644 . . . . . 6 (∃𝑤𝑧(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝐴 = ⟨𝑤, 𝑧⟩) ↔ ∃𝑧𝑤(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝐴 = ⟨𝑤, 𝑧⟩))
16 vex 2715 . . . . . . . . 9 𝑥 ∈ V
17 vex 2715 . . . . . . . . 9 𝑦 ∈ V
1816, 17opex 4189 . . . . . . . 8 𝑥, 𝑦⟩ ∈ V
19 opeq1 3741 . . . . . . . . 9 (𝑤 = ⟨𝑥, 𝑦⟩ → ⟨𝑤, 𝑧⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
2019eqeq2d 2169 . . . . . . . 8 (𝑤 = ⟨𝑥, 𝑦⟩ → (𝐴 = ⟨𝑤, 𝑧⟩ ↔ 𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
2118, 20ceqsexv 2751 . . . . . . 7 (∃𝑤(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝐴 = ⟨𝑤, 𝑧⟩) ↔ 𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
2221exbii 1585 . . . . . 6 (∃𝑧𝑤(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝐴 = ⟨𝑤, 𝑧⟩) ↔ ∃𝑧 𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
2315, 22bitri 183 . . . . 5 (∃𝑤𝑧(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝐴 = ⟨𝑤, 𝑧⟩) ↔ ∃𝑧 𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
24232exbii 1586 . . . 4 (∃𝑥𝑦𝑤𝑧(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝐴 = ⟨𝑤, 𝑧⟩) ↔ ∃𝑥𝑦𝑧 𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
2514, 24bitr3i 185 . . 3 (∃𝑤𝑧𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝐴 = ⟨𝑤, 𝑧⟩) ↔ ∃𝑥𝑦𝑧 𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
2613, 25bitri 183 . 2 (∃𝑤𝑧(𝐴 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 ∈ (V × V) ∧ 𝑧 ∈ V)) ↔ ∃𝑥𝑦𝑧 𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
271, 26bitri 183 1 (𝐴 ∈ ((V × V) × V) ↔ ∃𝑥𝑦𝑧 𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1335  ∃wex 1472   ∈ wcel 2128  Vcvv 2712  ⟨cop 3563   × cxp 4583 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-opab 4026  df-xp 4591 This theorem is referenced by:  ssrelrel  4685  dftpos3  6206
 Copyright terms: Public domain W3C validator