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

Theorem breldm 5074
Description: Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.)
Hypotheses
Ref Expression
opeldm.1  |-  A  e. 
_V
opeldm.2  |-  B  e. 
_V
Assertion
Ref Expression
breldm  |-  ( A R B  ->  A  e.  dom  R )

Proof of Theorem breldm
StepHypRef Expression
1 df-br 4213 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  R )
2 opeldm.1 . . 3  |-  A  e. 
_V
3 opeldm.2 . . 3  |-  B  e. 
_V
42, 3opeldm 5073 . 2  |-  ( <. A ,  B >.  e.  R  ->  A  e.  dom  R )
51, 4sylbi 188 1  |-  ( A R B  ->  A  e.  dom  R )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   _Vcvv 2956   <.cop 3817   class class class wbr 4212   dom cdm 4878
This theorem is referenced by:  exse2  5238  funcnv3  5512  dffv2  5796  dff13  6004  reldmtpos  6487  rntpos  6492  dftpos4  6498  tpostpos  6499  opabiota  6538  iserd  6931  dcomex  8327  axdc2lem  8328  axdclem2  8400  dmrecnq  8845  shftfval  11885  geolim2  12648  geomulcvg  12653  geoisum1c  12657  cvgrat  12660  eftlub  12710  eflegeo  12722  rpnnen2lem5  12818  imasleval  13766  psdmrn  14639  psssdm2  14647  ovoliunnul  19403  vitalilem5  19504  dvcj  19836  dvrec  19841  dvef  19864  ftc1cn  19927  aaliou3lem3  20261  ulmdv  20319  dvradcnv  20337  abelthlem7  20354  abelthlem9  20356  logtayllem  20550  leibpi  20782  log2tlbnd  20785  hhcms  22705  hhsscms  22779  occl  22806  zetacvg  24799  ntrivcvg  25225  iprodgam  25319  wfrlem5  25542  frrlem5  25586  imageval  25775  ftc1cnnc  26279  geomcau  26465
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213  df-dm 4888
  Copyright terms: Public domain W3C validator