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

Theorem breldm 5776
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 5064 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 opeldm.1 . . 3 𝐴 ∈ V
3 opeldm.2 . . 3 𝐵 ∈ V
42, 3opeldm 5775 . 2 (⟨𝐴, 𝐵⟩ ∈ 𝑅𝐴 ∈ dom 𝑅)
51, 4sylbi 218 1 (𝐴𝑅𝐵𝐴 ∈ dom 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Vcvv 3500  cop 4570   class class class wbr 5063  dom cdm 5554
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-br 5064  df-dm 5564
This theorem is referenced by:  funcnv3  6421  opabiota  6743  dffv2  6753  dff13  7007  exse2  7610  reldmtpos  7891  rntpos  7896  dftpos4  7902  tpostpos  7903  wfrlem5  7950  iserd  8305  dcomex  9858  axdc2lem  9859  axdclem2  9931  dmrecnq  10379  cotr2g  14326  shftfval  14419  geolim2  15217  geomulcvg  15222  geoisum1c  15226  cvgrat  15229  ntrivcvg  15243  eftlub  15452  eflegeo  15464  rpnnen2lem5  15561  imasleval  16804  psdmrn  17807  psssdm2  17815  ovoliunnul  24023  vitalilem5  24128  dvcj  24462  dvrec  24467  dvef  24492  ftc1cn  24555  aaliou3lem3  24848  ulmdv  24906  dvradcnv  24924  abelthlem7  24941  abelthlem9  24943  logtayllem  25155  leibpi  25434  log2tlbnd  25437  zetacvg  25506  hhcms  28894  hhsscms  28969  occl  28995  gsummpt2co  30600  iprodgam  32858  imaindm  32906  fprlem1  33021  frrlem15  33026  imageval  33275  knoppcnlem6  33721  knoppndvlem6  33740  knoppf  33758  unccur  34742  ftc1cnnc  34833  geomcau  34902  dvradcnv2  40544
  Copyright terms: Public domain W3C validator