Theorem breldm 5909

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475  ⟨cop 4635   class class class wbr 5149  dom cdm 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-dm 5687

This theorem is referenced by:  imaindm  6299  funcnv3  6619  opabiota  6975  dffv2  6987  dff13  7254  exse2  7908  reldmtpos  8219  rntpos  8224  dftpos4  8230  tpostpos  8231  fprlem1  8285  wfrlem5OLD  8313  iserd  8729  dmttrcl  9716  ttrclse  9722  frrlem15  9752  dcomex  10442  axdc2lem  10443  dmrecnq  10963  cotr2g  14923  shftfval  15017  geolim2  15817  geomulcvg  15822  geoisum1c  15826  cvgrat  15829  ntrivcvg  15843  eftlub  16052  eflegeo  16064  rpnnen2lem5  16161  imasleval  17487  psdmrn  18526  psssdm2  18534  ovoliunnul  25024  vitalilem5  25129  dvcj  25467  dvrec  25472  dvef  25497  ftc1cn  25560  aaliou3lem3  25857  ulmdv  25915  dvradcnv  25933  abelthlem7  25950  abelthlem9  25952  logtayllem  26167  leibpi  26447  log2tlbnd  26450  zetacvg  26519  hhcms  30487  hhsscms  30562  occl  30588  gsummpt2co  32231  iprodgam  34743  imageval  34933  knoppcnlem6  35422  knoppndvlem6  35441  knoppf  35459  unccur  36519  ftc1cnnc  36608  geomcau  36675  dvradcnv2  43154