Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmsnop Structured version   Visualization version   GIF version

Theorem dmsnop 5597
 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
StepHypRef Expression
1 dmsnop.1 . 2 𝐵 ∈ V
2 dmsnopg 5594 . 2 (𝐵 ∈ V → dom {⟨𝐴, 𝐵⟩} = {𝐴})
31, 2ax-mp 5 1 dom {⟨𝐴, 𝐵⟩} = {𝐴}
 Colors of variables: wff setvar class Syntax hints:   = wceq 1481   ∈ wcel 1988  Vcvv 3195  {csn 4168  ⟨cop 4174  dom cdm 5104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-dm 5114 This theorem is referenced by:  dmtpop  5599  dmsnsnsn  5601  op1sta  5605  funtp  5933  funopdmsn  6400  wfrlem13  7412  wfrlem16  7415  tfrlem10  7468  ac6sfi  8189  dcomex  9254  axdc3lem4  9260  cnfldfun  19739  bnj1416  31081  bnj1421  31084  subfacp1lem2a  31136  subfacp1lem5  31140  noextend  31793  nosupbday  31825  nosupbnd1  31834  nosupbnd2  31836
 Copyright terms: Public domain W3C validator