Theorem releldmi 5973

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5166  dom cdm 5700  Rel wrel 5705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-rel 5707  df-dm 5710

This theorem is referenced by:  fpwwe2lem10  10709  fpwwe2lem11  10710  fpwwe2lem12  10711  rlimpm  15546  rlimdm  15597  iserex  15705  caucvgrlem2  15723  caucvgr  15724  caurcvg2  15726  caucvg  15727  fsumcvg3  15777  cvgcmpce  15866  climcnds  15899  trirecip  15911  ledm  18660  cmetcaulem  25341  ovoliunlem1  25556  mbflimlem  25721  dvaddf  25999  dvmulf  26000  dvcof  26006  dvcnv  26035  abelthlem5  26497  emcllem6  27062  lgamgulmlem4  27093  hlimcaui  31268  brfvrcld2  43654  sumnnodd  45551  climliminf  45727  stirlinglem12  46006  fouriersw  46152  rlimdmafv  47092  rlimdmafv2  47173