Theorem breldm 5888

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

Step	Hyp	Ref	Expression
1		df-br 5120	. 2 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2		opeldm.1	. . 3 ⊢ 𝐴 ∈ V
3		opeldm.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	opeldm 5887	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝑅 → 𝐴 ∈ dom 𝑅)
5	1, 4	sylbi 217	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3459  ⟨cop 4607   class class class wbr 5119  dom cdm 5654

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-dm 5664

This theorem is referenced by:  imaindm  6288  funcnv3  6605  opabiota  6960  dffv2  6973  dff13  7246  exse2  7911  reldmtpos  8231  rntpos  8236  dftpos4  8242  tpostpos  8243  fprlem1  8297  wfrlem5OLD  8325  iserd  8743  dmttrcl  9733  ttrclse  9739  frrlem15  9769  dcomex  10459  axdc2lem  10460  dmrecnq  10980  cotr2g  14993  shftfval  15087  geolim2  15885  geomulcvg  15890  geoisum1c  15894  cvgrat  15897  ntrivcvg  15911  eftlub  16125  eflegeo  16137  rpnnen2lem5  16234  imasleval  17553  psdmrn  18581  psssdm2  18589  ovoliunnul  25458  vitalilem5  25563  dvcj  25904  dvrec  25909  dvef  25934  ftc1cn  26000  aaliou3lem3  26302  ulmdv  26362  dvradcnv  26380  abelthlem7  26398  abelthlem9  26400  logtayllem  26618  leibpi  26902  log2tlbnd  26905  zetacvg  26975  hhcms  31130  hhsscms  31205  occl  31231  gsummpt2co  32988  iprodgam  35705  imageval  35894  knoppcnlem6  36462  knoppndvlem6  36481  knoppf  36499  unccur  37573  ftc1cnnc  37662  geomcau  37729  dvradcnv2  44319