Theorem breldm 5859

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430  ⟨cop 4574   class class class wbr 5086  dom cdm 5626

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-dm 5636

This theorem is referenced by:  imaindm  6259  funcnv3  6564  opabiota  6918  dffv2  6931  dff13  7204  exse2  7863  reldmtpos  8179  rntpos  8184  dftpos4  8190  tpostpos  8191  fprlem1  8245  iserd  8665  dmttrcl  9637  ttrclse  9643  frrlem15  9676  dcomex  10364  axdc2lem  10365  dmrecnq  10886  cotr2g  14933  shftfval  15027  geolim2  15831  geomulcvg  15836  geoisum1c  15840  cvgrat  15843  ntrivcvg  15857  eftlub  16071  eflegeo  16083  rpnnen2lem5  16180  imasleval  17500  psdmrn  18534  psssdm2  18542  ovoliunnul  25488  vitalilem5  25593  dvcj  25931  dvrec  25936  dvef  25961  ftc1cn  26024  aaliou3lem3  26325  ulmdv  26385  dvradcnv  26403  abelthlem7  26420  abelthlem9  26422  logtayllem  26640  leibpi  26923  log2tlbnd  26926  zetacvg  26996  hhcms  31293  hhsscms  31368  occl  31394  gsummpt2co  33128  iprodgam  35944  imageval  36130  knoppcnlem6  36778  knoppndvlem6  36797  knoppf  36815  unccur  37944  ftc1cnnc  38033  geomcau  38100  dvradcnv2  44798  xpco2  49350