Theorem breldm 5741

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3441  ⟨cop 4531   class class class wbr 5030  dom cdm 5519

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-dm 5529

This theorem is referenced by:  funcnv3  6394  opabiota  6721  dffv2  6733  dff13  6991  exse2  7604  reldmtpos  7883  rntpos  7888  dftpos4  7894  tpostpos  7895  wfrlem5  7942  iserd  8298  dcomex  9858  axdc2lem  9859  axdclem2  9931  dmrecnq  10379  cotr2g  14327  shftfval  14421  geolim2  15219  geomulcvg  15224  geoisum1c  15228  cvgrat  15231  ntrivcvg  15245  eftlub  15454  eflegeo  15466  rpnnen2lem5  15563  imasleval  16806  psdmrn  17809  psssdm2  17817  ovoliunnul  24111  vitalilem5  24216  dvcj  24553  dvrec  24558  dvef  24583  ftc1cn  24646  aaliou3lem3  24940  ulmdv  24998  dvradcnv  25016  abelthlem7  25033  abelthlem9  25035  logtayllem  25250  leibpi  25528  log2tlbnd  25531  zetacvg  25600  hhcms  28986  hhsscms  29061  occl  29087  gsummpt2co  30733  iprodgam  33087  imaindm  33135  fprlem1  33250  frrlem15  33255  imageval  33504  knoppcnlem6  33950  knoppndvlem6  33969  knoppf  33987  unccur  35040  ftc1cnnc  35129  geomcau  35197  dvradcnv2  41051