Theorem breldm 5858

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441  ⟨cop 4587   class class class wbr 5099  dom cdm 5625

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-dm 5635

This theorem is referenced by:  imaindm  6258  funcnv3  6563  opabiota  6917  dffv2  6930  dff13  7202  exse2  7861  reldmtpos  8178  rntpos  8183  dftpos4  8189  tpostpos  8190  fprlem1  8244  iserd  8664  dmttrcl  9634  ttrclse  9640  frrlem15  9673  dcomex  10361  axdc2lem  10362  dmrecnq  10883  cotr2g  14903  shftfval  14997  geolim2  15798  geomulcvg  15803  geoisum1c  15807  cvgrat  15810  ntrivcvg  15824  eftlub  16038  eflegeo  16050  rpnnen2lem5  16147  imasleval  17466  psdmrn  18500  psssdm2  18508  ovoliunnul  25468  vitalilem5  25573  dvcj  25914  dvrec  25919  dvef  25944  ftc1cn  26010  aaliou3lem3  26312  ulmdv  26372  dvradcnv  26390  abelthlem7  26408  abelthlem9  26410  logtayllem  26628  leibpi  26912  log2tlbnd  26915  zetacvg  26985  hhcms  31282  hhsscms  31357  occl  31383  gsummpt2co  33133  iprodgam  35938  imageval  36124  knoppcnlem6  36700  knoppndvlem6  36719  knoppf  36737  unccur  37806  ftc1cnnc  37895  geomcau  37962  dvradcnv2  44655  xpco2  49169