Theorem releldmi 5922

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

Syntax hints:   → wi 4   ∈ wcel 2141   class class class wbr 5099  dom cdm 5645  Rel wrel 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5651  df-rel 5652  df-dm 5655

This theorem is referenced by:  fpwwe2lem10  10595  fpwwe2lem11  10596  fpwwe2lem12  10597  rlimpm  15510  rlimdm  15561  iserex  15667  caucvgrlem2  15685  caucvgr  15686  caurcvg2  15688  caucvg  15689  fsumcvg3  15739  cvgcmpce  15829  climcnds  15864  trirecip  15876  ledm  18605  cmetcaulem  25330  ovoliunlem1  25544  mbflimlem  25709  dvaddf  25984  dvmulf  25985  dvcof  25990  dvcnv  26019  abelthlem5  26475  emcllem6  27042  lgamgulmlem4  27073  hlimcaui  31385  brfvrcld2  44232  sumnnodd  46170  climliminf  46344  stirlinglem12  46623  fouriersw  46769  rlimdmafv  47735  rlimdmafv2  47816