Theorem dmsnop 6214

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

Syntax hints:   = wceq 1534   ∈ wcel 2099  Vcvv 3469  {csn 4624  ⟨cop 4630  dom cdm 5672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143  df-dm 5682

This theorem is referenced by:  dmtpop  6216  dmsnsnsn  6218  op1sta  6223  snres0  6296  funtp  6604  funopdmsn  7153  frrlem14  8298  wfrlem13OLD  8335  wfrlem16OLD  8338  tfrlem10  8401  ac6sfi  9303  dcomex  10462  axdc3lem4  10468  cnfldfunALT  21281  cnfldfunALTOLD  21294  cnfldfunALTOLDOLD  21295  noextend  27586  nosupbday  27625  nosupbnd1  27634  nosupbnd2  27636  noinfbday  27640  noinfbnd1  27649  noinfbnd2  27651  bnj1416  34606  bnj1421  34609  fineqvac  34653  subfacp1lem2a  34726  subfacp1lem5  34730