Theorem dmsnop 6220

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  Vcvv 3450  {csn 4584  ⟨cop 4834  dom cdm 5651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-dm 5661

This theorem is used by:  dmtpop  6222  dmsnsnsn  6224  op1sta  6229  snres0  6304  funtp  6602  funopdmsn  7159  frrlem14  8324  tfrlem10  8402  ac6sfi  9282  dcomex  10532  axdc3lem4  10538  cnfldfunALT  21702  noextend  28032  nosupbday  28071  nosupbnd1  28080  nosupbnd2  28082  noinfbday  28086  noinfbnd1  28095  noinfbnd2  28097  bnj1416  35719  bnj1421  35722  fineqvac  35844  subfacp1lem2a  36035  subfacp1lem5  36039