Theorem releldmi 5890

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 5886	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
3	1, 2	mpan 690	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5092  dom cdm 5619  Rel wrel 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-rel 5626  df-dm 5629

This theorem is referenced by:  fpwwe2lem10  10534  fpwwe2lem11  10535  fpwwe2lem12  10536  rlimpm  15407  rlimdm  15458  iserex  15564  caucvgrlem2  15582  caucvgr  15583  caurcvg2  15585  caucvg  15586  fsumcvg3  15636  cvgcmpce  15725  climcnds  15758  trirecip  15770  ledm  18496  cmetcaulem  25186  ovoliunlem1  25401  mbflimlem  25566  dvaddf  25843  dvmulf  25844  dvcof  25850  dvcnv  25879  abelthlem5  26343  emcllem6  26909  lgamgulmlem4  26940  hlimcaui  31184  brfvrcld2  43685  sumnnodd  45631  climliminf  45807  stirlinglem12  46086  fouriersw  46232  rlimdmafv  47181  rlimdmafv2  47262