Theorem dmsnop 6205

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 6202	. 2 ⊢ (𝐵 ∈ V → dom {⟨𝐴, 𝐵⟩} = {𝐴})
3	1, 2	ax-mp 5	1 ⊢ dom {⟨𝐴, 𝐵⟩} = {𝐴}

Syntax hints:   = wceq 1540   ∈ wcel 2108  Vcvv 3459  {csn 4601  ⟨cop 4607  dom cdm 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-dm 5664

This theorem is referenced by:  dmtpop  6207  dmsnsnsn  6209  op1sta  6214  snres0  6287  funtp  6593  funopdmsn  7140  frrlem14  8298  wfrlem13OLD  8335  wfrlem16OLD  8338  tfrlem10  8401  ac6sfi  9292  dcomex  10461  axdc3lem4  10467  cnfldfunALT  21330  cnfldfunALTOLD  21343  noextend  27630  nosupbday  27669  nosupbnd1  27678  nosupbnd2  27680  noinfbday  27684  noinfbnd1  27693  noinfbnd2  27695  bnj1416  35070  bnj1421  35073  fineqvac  35128  subfacp1lem2a  35202  subfacp1lem5  35206