Theorem dmsnop 6108

Description: The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by NM, 30-Jan-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)

Hypothesis

Ref	Expression
dmsnop.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
dmsnop	⊢ dom {⟨𝐴, 𝐵⟩} = {𝐴}

Proof of Theorem dmsnop

Step	Hyp	Ref	Expression
1		dmsnop.1	. 2 ⊢ 𝐵 ∈ V
2		dmsnopg 6105	. 2 ⊢ (𝐵 ∈ V → dom {⟨𝐴, 𝐵⟩} = {𝐴})
3	1, 2	ax-mp 5	1 ⊢ dom {⟨𝐴, 𝐵⟩} = {𝐴}

Syntax hints:   = wceq 1539   ∈ wcel 2108  Vcvv 3422  {csn 4558  ⟨cop 4564  dom cdm 5580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-dm 5590

This theorem is referenced by:  dmtpop  6110  dmsnsnsn  6112  op1sta  6117  funtp  6475  funopdmsn  7004  frrlem14  8086  wfrlem13OLD  8123  wfrlem16OLD  8126  tfrlem10  8189  ac6sfi  8988  dcomex  10134  axdc3lem4  10140  cnfldfun  20522  bnj1416  32919  bnj1421  32922  fineqvac  32966  subfacp1lem2a  33042  subfacp1lem5  33046  snres0  33577  noextend  33796  nosupbday  33835  nosupbnd1  33844  nosupbnd2  33846  noinfbday  33850  noinfbnd1  33859  noinfbnd2  33861