Theorem breldm 5886

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 5885	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝑅 → 𝐴 ∈ dom 𝑅)
5	1, 4	sylbi 219	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∈ wcel 2144  Vcvv 3456  ⟨cop 4590   class class class wbr 5102  dom cdm 5649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103  df-dm 5659

This theorem is referenced by:  imaindm  6288  funcnv3  6593  opabiota  6951  dffv2  6964  dff13  7240  exse2  7900  reldmtpos  8216  rntpos  8221  dftpos4  8227  tpostpos  8228  fprlem1  8283  iserd  8707  dmttrcl  9678  ttrclse  9684  frrlem15  9717  dcomex  10406  axdc2lem  10407  dmrecnq  10928  cotr2g  14991  shftfval  15085  geolim2  15903  geomulcvg  15908  geoisum1c  15912  cvgrat  15915  ntrivcvg  15929  eftlub  16143  eflegeo  16155  rpnnen2lem5  16252  imasleval  17573  psdmrn  18607  psssdm2  18615  ovoliunnul  25571  vitalilem5  25676  dvcj  26014  dvrec  26019  dvef  26044  ftc1cn  26107  aaliou3lem3  26410  ulmdv  26468  dvradcnv  26486  abelthlem7  26503  abelthlem9  26505  logtayllem  26726  leibpi  27009  log2tlbnd  27012  zetacvg  27081  hhcms  31408  hhsscms  31483  occl  31509  gsummpt2co  33230  iprodgam  36097  imageval  36283  knoppcnlem6  36941  knoppndvlem6  36960  knoppf  36978  unccur  38107  ftc1cnnc  38196  geomcau  38263  dvradcnv2  44928  xpco2  49483