Theorem releldmi 5961

Description: The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015.)

Hypothesis

Ref	Expression
releldm.1	⊢ Rel 𝑅

Assertion

Ref	Expression
releldmi	⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)

Proof of Theorem releldmi

Step	Hyp	Ref	Expression
1		releldm.1	. 2 ⊢ Rel 𝑅
2		releldm 5957	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
3	1, 2	mpan 690	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∈ wcel 2105   class class class wbr 5147  dom cdm 5688  Rel wrel 5693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-rel 5695  df-dm 5698

This theorem is referenced by:  fpwwe2lem10  10677  fpwwe2lem11  10678  fpwwe2lem12  10679  rlimpm  15532  rlimdm  15583  iserex  15689  caucvgrlem2  15707  caucvgr  15708  caurcvg2  15710  caucvg  15711  fsumcvg3  15761  cvgcmpce  15850  climcnds  15883  trirecip  15895  ledm  18647  cmetcaulem  25335  ovoliunlem1  25550  mbflimlem  25715  dvaddf  25993  dvmulf  25994  dvcof  26000  dvcnv  26029  abelthlem5  26493  emcllem6  27058  lgamgulmlem4  27089  hlimcaui  31264  brfvrcld2  43681  sumnnodd  45585  climliminf  45761  stirlinglem12  46040  fouriersw  46186  rlimdmafv  47126  rlimdmafv2  47207