Theorem breldm 5908

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 5149	. 2 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2		opeldm.1	. . 3 ⊢ 𝐴 ∈ V
3		opeldm.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	opeldm 5907	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝑅 → 𝐴 ∈ dom 𝑅)
5	1, 4	sylbi 216	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3474  ⟨cop 4634   class class class wbr 5148  dom cdm 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-dm 5686

This theorem is referenced by:  imaindm  6298  funcnv3  6618  opabiota  6974  dffv2  6986  dff13  7253  exse2  7907  reldmtpos  8218  rntpos  8223  dftpos4  8229  tpostpos  8230  fprlem1  8284  wfrlem5OLD  8312  iserd  8728  dmttrcl  9715  ttrclse  9721  frrlem15  9751  dcomex  10441  axdc2lem  10442  dmrecnq  10962  cotr2g  14922  shftfval  15016  geolim2  15816  geomulcvg  15821  geoisum1c  15825  cvgrat  15828  ntrivcvg  15842  eftlub  16051  eflegeo  16063  rpnnen2lem5  16160  imasleval  17486  psdmrn  18525  psssdm2  18533  ovoliunnul  25023  vitalilem5  25128  dvcj  25466  dvrec  25471  dvef  25496  ftc1cn  25559  aaliou3lem3  25856  ulmdv  25914  dvradcnv  25932  abelthlem7  25949  abelthlem9  25951  logtayllem  26166  leibpi  26444  log2tlbnd  26447  zetacvg  26516  hhcms  30451  hhsscms  30526  occl  30552  gsummpt2co  32195  iprodgam  34707  imageval  34897  knoppcnlem6  35369  knoppndvlem6  35388  knoppf  35406  unccur  36466  ftc1cnnc  36555  geomcau  36622  dvradcnv2  43096