Theorem dmsnop 6050

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

Syntax hints:   = wceq 1538   ∈ wcel 2111  Vcvv 3409  {csn 4525  ⟨cop 4531  dom cdm 5528

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pr 5302

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-dif 3863  df-un 3865  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-br 5037  df-dm 5538

This theorem is referenced by:  dmtpop  6052  dmsnsnsn  6054  op1sta  6059  funtp  6397  funopdmsn  6909  wfrlem13  7983  wfrlem16  7986  tfrlem10  8039  ac6sfi  8808  dcomex  9920  axdc3lem4  9926  cnfldfun  20191  bnj1416  32551  bnj1421  32554  subfacp1lem2a  32670  subfacp1lem5  32674  snres0  33205  frrlem14  33410  noextend  33466  nosupbday  33505  nosupbnd1  33514  nosupbnd2  33516  noinfbday  33520  noinfbnd1  33529  noinfbnd2  33531