Theorem breldm 5856

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3439  ⟨cop 4585   class class class wbr 5097  dom cdm 5623

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 2707

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 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-dm 5633

This theorem is referenced by:  imaindm  6256  funcnv3  6561  opabiota  6915  dffv2  6928  dff13  7200  exse2  7859  reldmtpos  8176  rntpos  8181  dftpos4  8187  tpostpos  8188  fprlem1  8242  iserd  8662  dmttrcl  9632  ttrclse  9638  frrlem15  9671  dcomex  10359  axdc2lem  10360  dmrecnq  10881  cotr2g  14901  shftfval  14995  geolim2  15796  geomulcvg  15801  geoisum1c  15805  cvgrat  15808  ntrivcvg  15822  eftlub  16036  eflegeo  16048  rpnnen2lem5  16145  imasleval  17464  psdmrn  18498  psssdm2  18506  ovoliunnul  25466  vitalilem5  25571  dvcj  25912  dvrec  25917  dvef  25942  ftc1cn  26008  aaliou3lem3  26310  ulmdv  26370  dvradcnv  26388  abelthlem7  26406  abelthlem9  26408  logtayllem  26626  leibpi  26910  log2tlbnd  26913  zetacvg  26983  hhcms  31259  hhsscms  31334  occl  31360  gsummpt2co  33110  iprodgam  35915  imageval  36101  knoppcnlem6  36671  knoppndvlem6  36690  knoppf  36708  unccur  37773  ftc1cnnc  37862  geomcau  37929  dvradcnv2  44625  xpco2  49139