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  9652  ttrclse  9658  frrlem15  9688  dcomex  10378  axdc2lem  10379  dmrecnq  10899  cotr2g  14919  shftfval  15013  geolim2  15814  geomulcvg  15819  geoisum1c  15823  cvgrat  15826  ntrivcvg  15840  eftlub  16054  eflegeo  16066  rpnnen2lem5  16163  imasleval  17481  psdmrn  18515  psssdm2  18523  ovoliunnul  25442  vitalilem5  25547  dvcj  25888  dvrec  25893  dvef  25918  ftc1cn  25984  aaliou3lem3  26286  ulmdv  26346  dvradcnv  26364  abelthlem7  26382  abelthlem9  26384  logtayllem  26602  leibpi  26886  log2tlbnd  26889  zetacvg  26959  hhcms  31183  hhsscms  31258  occl  31284  gsummpt2co  33032  iprodgam  35723  imageval  35912  knoppcnlem6  36480  knoppndvlem6  36499  knoppf  36517  unccur  37591  ftc1cnnc  37680  geomcau  37747  dvradcnv2  44330  xpco2  48839