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

Theorem dmsnopg 6041
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 3447 . . . . . 6 𝑥 ∈ V
2 vex 3447 . . . . . 6 𝑦 ∈ V
31, 2opth1 5335 . . . . 5 (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑥 = 𝐴)
43exlimiv 1931 . . . 4 (∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑥 = 𝐴)
5 opeq1 4766 . . . . 5 (𝑥 = 𝐴 → ⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩)
6 opeq2 4768 . . . . . . 7 (𝑦 = 𝐵 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝐵⟩)
76eqeq1d 2803 . . . . . 6 (𝑦 = 𝐵 → (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ ↔ ⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
87spcegv 3548 . . . . 5 (𝐵𝑉 → (⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩ → ∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩))
95, 8syl5 34 . . . 4 (𝐵𝑉 → (𝑥 = 𝐴 → ∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩))
104, 9impbid2 229 . . 3 (𝐵𝑉 → (∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ ↔ 𝑥 = 𝐴))
111eldm2 5738 . . . 4 (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ ∃𝑦𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩})
12 opex 5324 . . . . . 6 𝑥, 𝑦⟩ ∈ V
1312elsn 4543 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩} ↔ ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
1413exbii 1849 . . . 4 (∃𝑦𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩} ↔ ∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
1511, 14bitri 278 . . 3 (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ ∃𝑦𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
16 velsn 4544 . . 3 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
1710, 15, 163bitr4g 317 . 2 (𝐵𝑉 → (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ 𝑥 ∈ {𝐴}))
1817eqrdv 2799 1 (𝐵𝑉 → dom {⟨𝐴, 𝐵⟩} = {𝐴})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wex 1781  wcel 2112  {csn 4528  cop 4534  dom cdm 5523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-dm 5533
This theorem is referenced by:  dmsnopss  6042  dmpropg  6043  dmsnop  6044  rnsnopg  6049  fnsng  6380  funprg  6382  funtpg  6383  fntpg  6388  funsnfsupp  8845  s1dmALT  13958  setsval  16509  setsdm  16513  estrreslem2  17384  snstriedgval  26835  1loopgrvd0  27298  1hevtxdg0  27299  1hevtxdg1  27300  1egrvtxdg1  27303  p1evtxdeqlem  27306  wlkp1  27475  eupthp1  28005  trlsegvdeglem5  28013  cosnopne  30458  bnj96  32251  bnj535  32276  ovnovollem1  43288
  Copyright terms: Public domain W3C validator