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

Theorem breldm 5238
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 4578 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 opeldm.1 . . 3 𝐴 ∈ V
3 opeldm.2 . . 3 𝐵 ∈ V
42, 3opeldm 5237 . 2 (⟨𝐴, 𝐵⟩ ∈ 𝑅𝐴 ∈ dom 𝑅)
51, 4sylbi 205 1 (𝐴𝑅𝐵𝐴 ∈ dom 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  Vcvv 3172  cop 4130   class class class wbr 4577  dom cdm 5028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-dm 5038
This theorem is referenced by:  funcnv3  5859  opabiota  6156  dffv2  6166  dff13  6394  exse2  6976  reldmtpos  7225  rntpos  7230  dftpos4  7236  tpostpos  7237  wfrlem5  7284  iserd  7633  dcomex  9130  axdc2lem  9131  axdclem2  9203  dmrecnq  9647  cotr2g  13512  shftfval  13607  geolim2  14390  geomulcvg  14395  geoisum1c  14399  cvgrat  14403  ntrivcvg  14417  eftlub  14627  eflegeo  14639  rpnnen2lem5  14735  imasleval  15973  psdmrn  16979  psssdm2  16987  ovoliunnul  23027  vitalilem5  23132  dvcj  23464  dvrec  23469  dvef  23492  ftc1cn  23555  aaliou3lem3  23848  ulmdv  23906  dvradcnv  23924  abelthlem7  23941  abelthlem9  23943  logtayllem  24150  leibpi  24414  log2tlbnd  24417  zetacvg  24486  hhcms  27278  hhsscms  27354  occl  27381  gsummpt2co  28945  iprodgam  30715  frrlem5  30862  imageval  31041  knoppcnlem6  31492  knoppndvlem6  31512  knoppf  31530  unccur  32386  ftc1cnnc  32478  geomcau  32549  dvradcnv2  37392
  Copyright terms: Public domain W3C validator