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

Theorem breldm 5865
Description: Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.)
Hypotheses
Ref Expression
opeldm.1 𝐴 ∈ V
opeldm.2 𝐵 ∈ V
Assertion
Ref Expression
breldm (𝐴𝑅𝐵𝐴 ∈ dom 𝑅)

Proof of Theorem breldm
StepHypRef Expression
1 df-br 5107 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 opeldm.1 . . 3 𝐴 ∈ V
3 opeldm.2 . . 3 𝐵 ∈ V
42, 3opeldm 5864 . 2 (⟨𝐴, 𝐵⟩ ∈ 𝑅𝐴 ∈ dom 𝑅)
51, 4sylbi 216 1 (𝐴𝑅𝐵𝐴 ∈ dom 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Vcvv 3444  cop 4593   class class class wbr 5106  dom cdm 5634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-dm 5644
This theorem is referenced by:  imaindm  6252  funcnv3  6572  opabiota  6925  dffv2  6937  dff13  7203  exse2  7855  reldmtpos  8166  rntpos  8171  dftpos4  8177  tpostpos  8178  fprlem1  8232  wfrlem5OLD  8260  iserd  8677  dmttrcl  9662  ttrclse  9668  frrlem15  9698  dcomex  10388  axdc2lem  10389  dmrecnq  10909  cotr2g  14867  shftfval  14961  geolim2  15761  geomulcvg  15766  geoisum1c  15770  cvgrat  15773  ntrivcvg  15787  eftlub  15996  eflegeo  16008  rpnnen2lem5  16105  imasleval  17428  psdmrn  18467  psssdm2  18475  ovoliunnul  24887  vitalilem5  24992  dvcj  25330  dvrec  25335  dvef  25360  ftc1cn  25423  aaliou3lem3  25720  ulmdv  25778  dvradcnv  25796  abelthlem7  25813  abelthlem9  25815  logtayllem  26030  leibpi  26308  log2tlbnd  26311  zetacvg  26380  hhcms  30187  hhsscms  30262  occl  30288  gsummpt2co  31939  iprodgam  34371  imageval  34561  knoppcnlem6  35007  knoppndvlem6  35026  knoppf  35044  unccur  36107  ftc1cnnc  36196  geomcau  36264  dvradcnv2  42715
  Copyright terms: Public domain W3C validator