Theorem breldm 5867

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442  ⟨cop 4588   class class class wbr 5100  dom cdm 5634

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-dm 5644

This theorem is referenced by:  imaindm  6267  funcnv3  6572  opabiota  6926  dffv2  6939  dff13  7212  exse2  7871  reldmtpos  8188  rntpos  8193  dftpos4  8199  tpostpos  8200  fprlem1  8254  iserd  8674  dmttrcl  9644  ttrclse  9650  frrlem15  9683  dcomex  10371  axdc2lem  10372  dmrecnq  10893  cotr2g  14913  shftfval  15007  geolim2  15808  geomulcvg  15813  geoisum1c  15817  cvgrat  15820  ntrivcvg  15834  eftlub  16048  eflegeo  16060  rpnnen2lem5  16157  imasleval  17476  psdmrn  18510  psssdm2  18518  ovoliunnul  25481  vitalilem5  25586  dvcj  25927  dvrec  25932  dvef  25957  ftc1cn  26023  aaliou3lem3  26325  ulmdv  26385  dvradcnv  26403  abelthlem7  26421  abelthlem9  26423  logtayllem  26641  leibpi  26925  log2tlbnd  26928  zetacvg  26998  hhcms  31297  hhsscms  31372  occl  31398  gsummpt2co  33148  iprodgam  35964  imageval  36150  knoppcnlem6  36726  knoppndvlem6  36745  knoppf  36763  unccur  37883  ftc1cnnc  37972  geomcau  38039  dvradcnv2  44732  xpco2  49245