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

Theorem breldm 5543
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 4856 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 opeldm.1 . . 3 𝐴 ∈ V
3 opeldm.2 . . 3 𝐵 ∈ V
42, 3opeldm 5542 . 2 (⟨𝐴, 𝐵⟩ ∈ 𝑅𝐴 ∈ dom 𝑅)
51, 4sylbi 208 1 (𝐴𝑅𝐵𝐴 ∈ dom 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  Vcvv 3402  cop 4387   class class class wbr 4855  dom cdm 5324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-br 4856  df-dm 5334
This theorem is referenced by:  funcnv3  6179  opabiota  6491  dffv2  6501  dff13  6745  exse2  7344  reldmtpos  7604  rntpos  7609  dftpos4  7615  tpostpos  7616  wfrlem5  7664  iserd  8014  dcomex  9563  axdc2lem  9564  axdclem2  9636  dmrecnq  10084  cotr2g  13959  shftfval  14052  geolim2  14843  geomulcvg  14848  geoisum1c  14852  cvgrat  14855  ntrivcvg  14869  eftlub  15078  eflegeo  15090  rpnnen2lem5  15186  imasleval  16425  psdmrn  17431  psssdm2  17439  ovoliunnul  23510  vitalilem5  23615  dvcj  23949  dvrec  23954  dvef  23979  ftc1cn  24042  aaliou3lem3  24335  ulmdv  24393  dvradcnv  24411  abelthlem7  24428  abelthlem9  24430  logtayllem  24641  leibpi  24905  log2tlbnd  24908  zetacvg  24977  hhcms  28410  hhsscms  28486  occl  28513  gsummpt2co  30127  iprodgam  31971  imaindm  32023  frrlem5  32126  imageval  32379  knoppcnlem6  32826  knoppndvlem6  32846  knoppf  32864  unccur  33723  ftc1cnnc  33814  geomcau  33884  dvradcnv2  39063
  Copyright terms: Public domain W3C validator