Theorem breldm 5875

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450  ⟨cop 4598   class class class wbr 5110  dom cdm 5641

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-dm 5651

This theorem is referenced by:  imaindm  6275  funcnv3  6589  opabiota  6946  dffv2  6959  dff13  7232  exse2  7896  reldmtpos  8216  rntpos  8221  dftpos4  8227  tpostpos  8228  fprlem1  8282  iserd  8700  dmttrcl  9681  ttrclse  9687  frrlem15  9717  dcomex  10407  axdc2lem  10408  dmrecnq  10928  cotr2g  14949  shftfval  15043  geolim2  15844  geomulcvg  15849  geoisum1c  15853  cvgrat  15856  ntrivcvg  15870  eftlub  16084  eflegeo  16096  rpnnen2lem5  16193  imasleval  17511  psdmrn  18539  psssdm2  18547  ovoliunnul  25415  vitalilem5  25520  dvcj  25861  dvrec  25866  dvef  25891  ftc1cn  25957  aaliou3lem3  26259  ulmdv  26319  dvradcnv  26337  abelthlem7  26355  abelthlem9  26357  logtayllem  26575  leibpi  26859  log2tlbnd  26862  zetacvg  26932  hhcms  31139  hhsscms  31214  occl  31240  gsummpt2co  32995  iprodgam  35736  imageval  35925  knoppcnlem6  36493  knoppndvlem6  36512  knoppf  36530  unccur  37604  ftc1cnnc  37693  geomcau  37760  dvradcnv2  44343  xpco2  48849