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

Theorem dmsnop 5413
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  |-  B  e. 
_V
Assertion
Ref Expression
dmsnop  |-  dom  { <. A ,  B >. }  =  { A }

Proof of Theorem dmsnop
StepHypRef Expression
1 dmsnop.1 . 2  |-  B  e. 
_V
2 dmsnopg 5410 . 2  |-  ( B  e.  _V  ->  dom  {
<. A ,  B >. }  =  { A }
)
31, 2ax-mp 5 1  |-  dom  { <. A ,  B >. }  =  { A }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    e. wcel 1758   _Vcvv 3070   {csn 3977   <.cop 3983   dom cdm 4940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4513  ax-nul 4521  ax-pr 4631
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-rab 2804  df-v 3072  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-sn 3978  df-pr 3980  df-op 3984  df-br 4393  df-dm 4950
This theorem is referenced by:  dmtpop  5415  dmsnsnsn  5417  op1sta  5421  funtp  5570  tfrlem10  6948  ac6sfi  7659  dcomex  8719  axdc3lem4  8725  wlkntrllem1  23595  eupap1  23734  ablosn  23971  subfacp1lem2a  27204  subfacp1lem5  27208  wfrlem13  27872  wfrlem16  27875  bnj1416  32332  bnj1421  32335
  Copyright terms: Public domain W3C validator