Theorem breldm 5899

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

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3461  ⟨cop 4598   class class class wbr 5111  dom cdm 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112  df-dm 5672

This theorem is referenced by:  imaindm  6301  funcnv3  6607  opabiota  6964  dffv2  6977  dff13  7253  exse2  7914  reldmtpos  8230  rntpos  8235  dftpos4  8241  tpostpos  8242  fprlem1  8297  iserd  8721  dmttrcl  9690  ttrclse  9696  frrlem15  9729  dcomex  10431  axdc2lem  10432  dmrecnq  10953  cotr2g  15013  shftfval  15107  geolim2  15925  geomulcvg  15930  geoisum1c  15934  cvgrat  15937  ntrivcvg  15951  eftlub  16165  eflegeo  16177  rpnnen2lem5  16274  imasleval  17595  psdmrn  18629  psssdm2  18637  ovoliunnul  25635  vitalilem5  25740  dvcj  26078  dvrec  26083  dvef  26108  ftc1cn  26171  aaliou3lem3  26474  ulmdv  26532  dvradcnv  26550  abelthlem7  26567  abelthlem9  26569  logtayllem  26790  leibpi  27073  log2tlbnd  27076  zetacvg  27145  hhcms  31496  hhsscms  31571  occl  31597  gsummpt2co  33309  iprodgam  36167  imageval  36353  knoppcnlem6  37010  knoppndvlem6  37029  knoppf  37047  unccur  38177  ftc1cnnc  38266  geomcau  38333  dvradcnv2  44984  xpco2  49555