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

Theorem breldm 5906
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 5148 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 opeldm.1 . . 3 𝐴 ∈ V
3 opeldm.2 . . 3 𝐵 ∈ V
42, 3opeldm 5905 . 2 (⟨𝐴, 𝐵⟩ ∈ 𝑅𝐴 ∈ dom 𝑅)
51, 4sylbi 216 1 (𝐴𝑅𝐵𝐴 ∈ dom 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  Vcvv 3474  cop 4633   class class class wbr 5147  dom cdm 5675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-dm 5685
This theorem is referenced by:  imaindm  6295  funcnv3  6615  opabiota  6971  dffv2  6983  dff13  7250  exse2  7904  reldmtpos  8215  rntpos  8220  dftpos4  8226  tpostpos  8227  fprlem1  8281  wfrlem5OLD  8309  iserd  8725  dmttrcl  9712  ttrclse  9718  frrlem15  9748  dcomex  10438  axdc2lem  10439  dmrecnq  10959  cotr2g  14919  shftfval  15013  geolim2  15813  geomulcvg  15818  geoisum1c  15822  cvgrat  15825  ntrivcvg  15839  eftlub  16048  eflegeo  16060  rpnnen2lem5  16157  imasleval  17483  psdmrn  18522  psssdm2  18530  ovoliunnul  25015  vitalilem5  25120  dvcj  25458  dvrec  25463  dvef  25488  ftc1cn  25551  aaliou3lem3  25848  ulmdv  25906  dvradcnv  25924  abelthlem7  25941  abelthlem9  25943  logtayllem  26158  leibpi  26436  log2tlbnd  26439  zetacvg  26508  hhcms  30443  hhsscms  30518  occl  30544  gsummpt2co  32187  iprodgam  34700  imageval  34890  knoppcnlem6  35362  knoppndvlem6  35381  knoppf  35399  unccur  36459  ftc1cnnc  36548  geomcau  36615  dvradcnv2  43091
  Copyright terms: Public domain W3C validator