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

Theorem breldm 5049
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 4298 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  R )
2 opeldm.1 . . 3  |-  A  e. 
_V
3 opeldm.2 . . 3  |-  B  e. 
_V
42, 3opeldm 5048 . 2  |-  ( <. A ,  B >.  e.  R  ->  A  e.  dom  R )
51, 4sylbi 195 1  |-  ( A R B  ->  A  e.  dom  R )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   _Vcvv 2977   <.cop 3888   class class class wbr 4297   dom cdm 4845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-br 4298  df-dm 4855
This theorem is referenced by:  funcnv3  5484  opabiota  5759  dffv2  5769  dff13  5976  exse2  6522  reldmtpos  6758  rntpos  6763  dftpos4  6769  tpostpos  6770  iserd  7132  dcomex  8621  axdc2lem  8622  axdclem2  8694  dmrecnq  9142  shftfval  12564  geolim2  13336  geomulcvg  13341  geoisum1c  13345  cvgrat  13348  eftlub  13398  eflegeo  13410  rpnnen2lem5  13506  imasleval  14484  psdmrn  15382  psssdm2  15390  ovoliunnul  20995  vitalilem5  21097  dvcj  21429  dvrec  21434  dvef  21457  ftc1cn  21520  aaliou3lem3  21815  ulmdv  21873  dvradcnv  21891  abelthlem7  21908  abelthlem9  21910  logtayllem  22109  leibpi  22342  log2tlbnd  22345  hhcms  24610  hhsscms  24685  occl  24712  gsummpt2co  26254  zetacvg  27006  ntrivcvg  27417  iprodgam  27511  wfrlem5  27733  frrlem5  27777  imageval  27966  ftc1cnnc  28471  geomcau  28660
  Copyright terms: Public domain W3C validator