Theorem releldmi 5959

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5143  dom cdm 5685  Rel wrel 5690

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-dm 5695

This theorem is referenced by:  fpwwe2lem10  10680  fpwwe2lem11  10681  fpwwe2lem12  10682  rlimpm  15536  rlimdm  15587  iserex  15693  caucvgrlem2  15711  caucvgr  15712  caurcvg2  15714  caucvg  15715  fsumcvg3  15765  cvgcmpce  15854  climcnds  15887  trirecip  15899  ledm  18635  cmetcaulem  25322  ovoliunlem1  25537  mbflimlem  25702  dvaddf  25979  dvmulf  25980  dvcof  25986  dvcnv  26015  abelthlem5  26479  emcllem6  27044  lgamgulmlem4  27075  hlimcaui  31255  brfvrcld2  43705  sumnnodd  45645  climliminf  45821  stirlinglem12  46100  fouriersw  46246  rlimdmafv  47189  rlimdmafv2  47270