Theorem releldmi 5940

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

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5110  dom cdm 5663  Rel wrel 5668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-rel 5670  df-dm 5673

This theorem is referenced by:  fpwwe2lem10  10626  fpwwe2lem11  10627  fpwwe2lem12  10628  rlimpm  15553  rlimdm  15604  iserex  15710  caucvgrlem2  15728  caucvgr  15729  caurcvg2  15731  caucvg  15732  fsumcvg3  15782  cvgcmpce  15872  climcnds  15907  trirecip  15919  ledm  18647  cmetcaulem  25428  ovoliunlem1  25642  mbflimlem  25807  dvaddf  26082  dvmulf  26083  dvcof  26088  dvcnv  26117  abelthlem5  26576  emcllem6  27143  lgamgulmlem4  27174  hlimcaui  31566  brfvrcld2  44398  sumnnodd  46326  climliminf  46500  stirlinglem12  46779  fouriersw  46925  rlimdmafv  47891  rlimdmafv2  47972