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

Theorem breldm 5919
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 5144 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 opeldm.1 . . 3 𝐴 ∈ V
3 opeldm.2 . . 3 𝐵 ∈ V
42, 3opeldm 5918 . 2 (⟨𝐴, 𝐵⟩ ∈ 𝑅𝐴 ∈ dom 𝑅)
51, 4sylbi 217 1 (𝐴𝑅𝐵𝐴 ∈ dom 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  Vcvv 3480  cop 4632   class class class wbr 5143  dom cdm 5685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-dm 5695
This theorem is referenced by:  imaindm  6319  funcnv3  6636  opabiota  6991  dffv2  7004  dff13  7275  exse2  7939  reldmtpos  8259  rntpos  8264  dftpos4  8270  tpostpos  8271  fprlem1  8325  wfrlem5OLD  8353  iserd  8771  dmttrcl  9761  ttrclse  9767  frrlem15  9797  dcomex  10487  axdc2lem  10488  dmrecnq  11008  cotr2g  15015  shftfval  15109  geolim2  15907  geomulcvg  15912  geoisum1c  15916  cvgrat  15919  ntrivcvg  15933  eftlub  16145  eflegeo  16157  rpnnen2lem5  16254  imasleval  17586  psdmrn  18618  psssdm2  18626  ovoliunnul  25542  vitalilem5  25647  dvcj  25988  dvrec  25993  dvef  26018  ftc1cn  26084  aaliou3lem3  26386  ulmdv  26446  dvradcnv  26464  abelthlem7  26482  abelthlem9  26484  logtayllem  26701  leibpi  26985  log2tlbnd  26988  zetacvg  27058  hhcms  31222  hhsscms  31297  occl  31323  gsummpt2co  33051  iprodgam  35742  imageval  35931  knoppcnlem6  36499  knoppndvlem6  36518  knoppf  36536  unccur  37610  ftc1cnnc  37699  geomcau  37766  dvradcnv2  44366
  Copyright terms: Public domain W3C validator