Theorem dmsnop 6177

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3444  {csn 4585  ⟨cop 4591  dom cdm 5631

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-dm 5641

This theorem is referenced by:  dmtpop  6179  dmsnsnsn  6181  op1sta  6186  snres0  6259  funtp  6557  funopdmsn  7104  frrlem14  8255  tfrlem10  8332  ac6sfi  9207  dcomex  10376  axdc3lem4  10382  cnfldfunALT  21255  cnfldfunALTOLD  21268  noextend  27554  nosupbday  27593  nosupbnd1  27602  nosupbnd2  27604  noinfbday  27608  noinfbnd1  27617  noinfbnd2  27619  bnj1416  35002  bnj1421  35005  fineqvac  35060  subfacp1lem2a  35140  subfacp1lem5  35144