Theorem dmsnop 6215

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

Syntax hints:   = wceq 1541   ∈ wcel 2106  Vcvv 3474  {csn 4628  ⟨cop 4634  dom cdm 5676

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-dm 5686

This theorem is referenced by:  dmtpop  6217  dmsnsnsn  6219  op1sta  6224  snres0  6297  funtp  6605  funopdmsn  7147  frrlem14  8283  wfrlem13OLD  8320  wfrlem16OLD  8323  tfrlem10  8386  ac6sfi  9286  dcomex  10441  axdc3lem4  10447  cnfldfunALT  20956  cnfldfunALTOLD  20957  noextend  27166  nosupbday  27205  nosupbnd1  27214  nosupbnd2  27216  noinfbday  27220  noinfbnd1  27229  noinfbnd2  27231  bnj1416  34045  bnj1421  34048  fineqvac  34092  subfacp1lem2a  34166  subfacp1lem5  34170