Theorem breldm 5851

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436  ⟨cop 4583   class class class wbr 5092  dom cdm 5619

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-dm 5629

This theorem is referenced by:  imaindm  6247  funcnv3  6552  opabiota  6905  dffv2  6918  dff13  7191  exse2  7850  reldmtpos  8167  rntpos  8172  dftpos4  8178  tpostpos  8179  fprlem1  8233  iserd  8651  dmttrcl  9617  ttrclse  9623  frrlem15  9653  dcomex  10341  axdc2lem  10342  dmrecnq  10862  cotr2g  14883  shftfval  14977  geolim2  15778  geomulcvg  15783  geoisum1c  15787  cvgrat  15790  ntrivcvg  15804  eftlub  16018  eflegeo  16030  rpnnen2lem5  16127  imasleval  17445  psdmrn  18479  psssdm2  18487  ovoliunnul  25406  vitalilem5  25511  dvcj  25852  dvrec  25857  dvef  25882  ftc1cn  25948  aaliou3lem3  26250  ulmdv  26310  dvradcnv  26328  abelthlem7  26346  abelthlem9  26348  logtayllem  26566  leibpi  26850  log2tlbnd  26853  zetacvg  26923  hhcms  31151  hhsscms  31226  occl  31252  gsummpt2co  33010  iprodgam  35735  imageval  35924  knoppcnlem6  36492  knoppndvlem6  36511  knoppf  36529  unccur  37603  ftc1cnnc  37692  geomcau  37759  dvradcnv2  44340  xpco2  48861