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

Theorem breldm 5196
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 4440 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  R )
2 opeldm.1 . . 3  |-  A  e. 
_V
3 opeldm.2 . . 3  |-  B  e. 
_V
42, 3opeldm 5195 . 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 1823   _Vcvv 3106   <.cop 4022   class class class wbr 4439   dom cdm 4988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-dm 4998
This theorem is referenced by:  funcnv3  5631  opabiota  5911  dffv2  5921  dff13  6141  exse2  6712  reldmtpos  6955  rntpos  6960  dftpos4  6966  tpostpos  6967  iserd  7329  dcomex  8818  axdc2lem  8819  axdclem2  8891  dmrecnq  9335  cotr2g  12894  shftfval  12985  geolim2  13762  geomulcvg  13767  geoisum1c  13771  cvgrat  13774  ntrivcvg  13788  eftlub  13926  eflegeo  13938  rpnnen2lem5  14036  imasleval  15030  psdmrn  16036  psssdm2  16044  ovoliunnul  22084  vitalilem5  22187  dvcj  22519  dvrec  22524  dvef  22547  ftc1cn  22610  aaliou3lem3  22906  ulmdv  22964  dvradcnv  22982  abelthlem7  22999  abelthlem9  23001  logtayllem  23208  leibpi  23470  log2tlbnd  23473  hhcms  26318  hhsscms  26393  occl  26420  gsummpt2co  28005  zetacvg  28821  iprodgam  29366  wfrlem5  29587  frrlem5  29631  imageval  29808  ftc1cnnc  30329  geomcau  30492  dvradcnv2  31493
  Copyright terms: Public domain W3C validator