Theorem dmsnop 6172

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  Vcvv 3438  {csn 4578  ⟨cop 4584  dom cdm 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-dm 5632

This theorem is referenced by:  dmtpop  6174  dmsnsnsn  6176  op1sta  6181  snres0  6254  funtp  6547  funopdmsn  7093  frrlem14  8239  tfrlem10  8316  ac6sfi  9182  dcomex  10355  axdc3lem4  10361  cnfldfunALT  21322  cnfldfunALTOLD  21335  noextend  27632  nosupbday  27671  nosupbnd1  27680  nosupbnd2  27682  noinfbday  27686  noinfbnd1  27695  noinfbnd2  27697  bnj1416  35144  bnj1421  35147  fineqvac  35221  subfacp1lem2a  35323  subfacp1lem5  35327