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

Theorem dmsnopg 6235
Description: The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
dmsnopg (𝐵𝑉 → dom {⟨𝐴, 𝐵⟩} = {𝐴})

Proof of Theorem dmsnopg
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3482 . . . . . 6 𝑥 ∈ V
2 vex 3482 . . . . . 6 𝑦 ∈ V
31, 2opth1 5486 . . . . 5 (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑥 = 𝐴)
43exlimiv 1928 . . . 4 (∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑥 = 𝐴)
5 opeq1 4878 . . . . 5 (𝑥 = 𝐴 → ⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩)
6 opeq2 4879 . . . . . . 7 (𝑦 = 𝐵 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝐵⟩)
76eqeq1d 2737 . . . . . 6 (𝑦 = 𝐵 → (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ ↔ ⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
87spcegv 3597 . . . . 5 (𝐵𝑉 → (⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩ → ∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩))
95, 8syl5 34 . . . 4 (𝐵𝑉 → (𝑥 = 𝐴 → ∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩))
104, 9impbid2 226 . . 3 (𝐵𝑉 → (∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ ↔ 𝑥 = 𝐴))
111eldm2 5915 . . . 4 (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ ∃𝑦𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩})
12 opex 5475 . . . . . 6 𝑥, 𝑦⟩ ∈ V
1312elsn 4646 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩} ↔ ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
1413exbii 1845 . . . 4 (∃𝑦𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩} ↔ ∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
1511, 14bitri 275 . . 3 (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ ∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
16 velsn 4647 . . 3 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
1710, 15, 163bitr4g 314 . 2 (𝐵𝑉 → (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ 𝑥 ∈ {𝐴}))
1817eqrdv 2733 1 (𝐵𝑉 → dom {⟨𝐴, 𝐵⟩} = {𝐴})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  wex 1776  wcel 2106  {csn 4631  cop 4637  dom cdm 5689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-dm 5699
This theorem is referenced by:  dmsnopss  6236  dmpropg  6237  dmsnop  6238  rnsnopg  6243  fnsng  6620  funprg  6622  funtpg  6623  fntpg  6628  funsnfsupp  9430  s1dmALT  14644  setsval  17201  setsdm  17204  estrreslem2  18194  snstriedgval  29070  1loopgrvd0  29537  1hevtxdg0  29538  1hevtxdg1  29539  1egrvtxdg1  29542  p1evtxdeqlem  29545  wlkp1  29714  eupthp1  30245  trlsegvdeglem5  30253  cosnopne  32709  bnj96  34858  bnj535  34883  ovnovollem1  46612
  Copyright terms: Public domain W3C validator