Theorem breldm 5863

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429  ⟨cop 4573   class class class wbr 5085  dom cdm 5631

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-dm 5641

This theorem is referenced by:  imaindm  6263  funcnv3  6568  opabiota  6922  dffv2  6935  dff13  7209  exse2  7868  reldmtpos  8184  rntpos  8189  dftpos4  8195  tpostpos  8196  fprlem1  8250  iserd  8670  dmttrcl  9642  ttrclse  9648  frrlem15  9681  dcomex  10369  axdc2lem  10370  dmrecnq  10891  cotr2g  14938  shftfval  15032  geolim2  15836  geomulcvg  15841  geoisum1c  15845  cvgrat  15848  ntrivcvg  15862  eftlub  16076  eflegeo  16088  rpnnen2lem5  16185  imasleval  17505  psdmrn  18539  psssdm2  18547  ovoliunnul  25474  vitalilem5  25579  dvcj  25917  dvrec  25922  dvef  25947  ftc1cn  26010  aaliou3lem3  26310  ulmdv  26368  dvradcnv  26386  abelthlem7  26403  abelthlem9  26405  logtayllem  26623  leibpi  26906  log2tlbnd  26909  zetacvg  26978  hhcms  31274  hhsscms  31349  occl  31375  gsummpt2co  33109  iprodgam  35924  imageval  36110  knoppcnlem6  36758  knoppndvlem6  36777  knoppf  36795  unccur  37924  ftc1cnnc  38013  geomcau  38080  dvradcnv2  44774  xpco2  49332