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

Theorem breldm 4883
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 4024 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  R )
2 opeldm.1 . . 3  |-  A  e. 
_V
3 opeldm.2 . . 3  |-  B  e. 
_V
42, 3opeldm 4882 . 2  |-  ( <. A ,  B >.  e.  R  ->  A  e.  dom  R )
51, 4sylbi 187 1  |-  ( A R B  ->  A  e.  dom  R )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   _Vcvv 2788   <.cop 3643   class class class wbr 4023   dom cdm 4689
This theorem is referenced by:  exse2  5047  funcnv3  5311  dffv2  5592  dff13  5783  reldmtpos  6242  rntpos  6247  dftpos4  6253  tpostpos  6254  opabiota  6293  iserd  6686  dcomex  8073  axdc2lem  8074  axdclem2  8147  dmrecnq  8592  shftfval  11565  geolim2  12327  geomulcvg  12332  geoisum1c  12336  cvgrat  12339  eftlub  12389  eflegeo  12401  rpnnen2lem5  12497  imasleval  13443  psdmrn  14316  psssdm2  14324  ovoliunnul  18866  vitalilem5  18967  dvcj  19299  dvrec  19304  dvef  19327  ftc1cn  19390  aaliou3lem3  19724  ulmdv  19780  dvradcnv  19797  abelthlem7  19814  abelthlem9  19816  logtayllem  20006  leibpi  20238  log2tlbnd  20241  hhcms  21782  hhsscms  21856  occl  21883  zetacvg  23689  wfrlem5  24260  frrlem5  24285  imageval  24469  domfldrefc  25057  domrngref  25060  domintrefb  25063  tolat  25286  cntrset  25602  geomcau  26475
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-dm 4699
  Copyright terms: Public domain W3C validator