Theorem releldmi 5894

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5095  dom cdm 5623  Rel wrel 5628

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 5238  ax-nul 5248  ax-pr 5374

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629  df-rel 5630  df-dm 5633

This theorem is referenced by:  fpwwe2lem10  10553  fpwwe2lem11  10554  fpwwe2lem12  10555  rlimpm  15425  rlimdm  15476  iserex  15582  caucvgrlem2  15600  caucvgr  15601  caurcvg2  15603  caucvg  15604  fsumcvg3  15654  cvgcmpce  15743  climcnds  15776  trirecip  15788  ledm  18514  cmetcaulem  25204  ovoliunlem1  25419  mbflimlem  25584  dvaddf  25861  dvmulf  25862  dvcof  25868  dvcnv  25897  abelthlem5  26361  emcllem6  26927  lgamgulmlem4  26958  hlimcaui  31198  brfvrcld2  43665  sumnnodd  45612  climliminf  45788  stirlinglem12  46067  fouriersw  46213  rlimdmafv  47162  rlimdmafv2  47243