Theorem breldm 5921

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477  ⟨cop 4636   class class class wbr 5147  dom cdm 5688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-dm 5698

This theorem is referenced by:  imaindm  6320  funcnv3  6637  opabiota  6990  dffv2  7003  dff13  7274  exse2  7939  reldmtpos  8257  rntpos  8262  dftpos4  8268  tpostpos  8269  fprlem1  8323  wfrlem5OLD  8351  iserd  8769  dmttrcl  9758  ttrclse  9764  frrlem15  9794  dcomex  10484  axdc2lem  10485  dmrecnq  11005  cotr2g  15011  shftfval  15105  geolim2  15903  geomulcvg  15908  geoisum1c  15912  cvgrat  15915  ntrivcvg  15929  eftlub  16141  eflegeo  16153  rpnnen2lem5  16250  imasleval  17587  psdmrn  18630  psssdm2  18638  ovoliunnul  25555  vitalilem5  25660  dvcj  26002  dvrec  26007  dvef  26032  ftc1cn  26098  aaliou3lem3  26400  ulmdv  26460  dvradcnv  26478  abelthlem7  26496  abelthlem9  26498  logtayllem  26715  leibpi  26999  log2tlbnd  27002  zetacvg  27072  hhcms  31231  hhsscms  31306  occl  31332  gsummpt2co  33033  iprodgam  35721  imageval  35911  knoppcnlem6  36480  knoppndvlem6  36499  knoppf  36517  unccur  37589  ftc1cnnc  37678  geomcau  37745  dvradcnv2  44342