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

Theorem dmsnopg 5524
 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 3176 . . . . . 6 𝑥 ∈ V
2 vex 3176 . . . . . 6 𝑦 ∈ V
31, 2opth1 4870 . . . . 5 (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑥 = 𝐴)
43exlimiv 1845 . . . 4 (∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑥 = 𝐴)
5 opeq1 4340 . . . . 5 (𝑥 = 𝐴 → ⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩)
6 opeq2 4341 . . . . . . 7 (𝑦 = 𝐵 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝐵⟩)
76eqeq1d 2612 . . . . . 6 (𝑦 = 𝐵 → (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ ↔ ⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
87spcegv 3267 . . . . 5 (𝐵𝑉 → (⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩ → ∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩))
95, 8syl5 33 . . . 4 (𝐵𝑉 → (𝑥 = 𝐴 → ∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩))
104, 9impbid2 215 . . 3 (𝐵𝑉 → (∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ ↔ 𝑥 = 𝐴))
111eldm2 5244 . . . 4 (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ ∃𝑦𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩})
12 opex 4859 . . . . . 6 𝑥, 𝑦⟩ ∈ V
1312elsn 4140 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩} ↔ ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
1413exbii 1764 . . . 4 (∃𝑦𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩} ↔ ∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
1511, 14bitri 263 . . 3 (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ ∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
16 velsn 4141 . . 3 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
1710, 15, 163bitr4g 302 . 2 (𝐵𝑉 → (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ 𝑥 ∈ {𝐴}))
1817eqrdv 2608 1 (𝐵𝑉 → dom {⟨𝐴, 𝐵⟩} = {𝐴})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {csn 4125  ⟨cop 4131  dom cdm 5038 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 4709  ax-nul 4717  ax-pr 4833 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-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-br 4584  df-dm 5048 This theorem is referenced by:  dmsnopss  5525  dmpropg  5526  dmsnop  5527  rnsnopg  5532  fnsng  5852  funprg  5854  funprgOLD  5855  funtpg  5856  funtpgOLD  5857  fntpg  5862  suppsnop  7196  funsnfsupp  8182  s1dmALT  13242  setsval  15720  setsdm  15724  estrreslem2  16601  snstriedgval  25713  eupap1  26503  bnj96  30189  bnj535  30214  ovnovollem1  39546  1loopgrvd0  40719  1hevtxdg0  40720  1hevtxdg1  40721  1egrvtxdg1  40725  p1evtxdeqlem  40728  1wlkp1  40890  eupthp1  41384  trlsegvdeglem5  41392
 Copyright terms: Public domain W3C validator