Theorem breldm 5862

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444  ⟨cop 4591   class class class wbr 5102  dom cdm 5631

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-dm 5641

This theorem is referenced by:  imaindm  6260  funcnv3  6570  opabiota  6925  dffv2  6938  dff13  7211  exse2  7873  reldmtpos  8190  rntpos  8195  dftpos4  8201  tpostpos  8202  fprlem1  8256  iserd  8674  dmttrcl  9650  ttrclse  9656  frrlem15  9686  dcomex  10376  axdc2lem  10377  dmrecnq  10897  cotr2g  14918  shftfval  15012  geolim2  15813  geomulcvg  15818  geoisum1c  15822  cvgrat  15825  ntrivcvg  15839  eftlub  16053  eflegeo  16065  rpnnen2lem5  16162  imasleval  17480  psdmrn  18514  psssdm2  18522  ovoliunnul  25441  vitalilem5  25546  dvcj  25887  dvrec  25892  dvef  25917  ftc1cn  25983  aaliou3lem3  26285  ulmdv  26345  dvradcnv  26363  abelthlem7  26381  abelthlem9  26383  logtayllem  26601  leibpi  26885  log2tlbnd  26888  zetacvg  26958  hhcms  31182  hhsscms  31257  occl  31283  gsummpt2co  33031  iprodgam  35722  imageval  35911  knoppcnlem6  36479  knoppndvlem6  36498  knoppf  36516  unccur  37590  ftc1cnnc  37679  geomcau  37746  dvradcnv2  44329  xpco2  48838