Theorem dmsnop 6236

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  Vcvv 3480  {csn 4626  ⟨cop 4632  dom cdm 5685

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-dm 5695

This theorem is referenced by:  dmtpop  6238  dmsnsnsn  6240  op1sta  6245  snres0  6318  funtp  6623  funopdmsn  7170  frrlem14  8324  wfrlem13OLD  8361  wfrlem16OLD  8364  tfrlem10  8427  ac6sfi  9320  dcomex  10487  axdc3lem4  10493  cnfldfunALT  21379  cnfldfunALTOLD  21392  cnfldfunALTOLDOLD  21393  noextend  27711  nosupbday  27750  nosupbnd1  27759  nosupbnd2  27761  noinfbday  27765  noinfbnd1  27774  noinfbnd2  27776  bnj1416  35053  bnj1421  35056  fineqvac  35111  subfacp1lem2a  35185  subfacp1lem5  35189