Theorem releldmi 5566

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

Syntax hints:   → wi 4   ∈ wcel 2157   class class class wbr 4843  dom cdm 5312  Rel wrel 5317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-nul 4983  ax-pr 5097

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-br 4844  df-opab 4906  df-xp 5318  df-rel 5319  df-dm 5322

This theorem is referenced by:  fpwwe2lem11  9750  fpwwe2lem12  9751  fpwwe2lem13  9752  rlimpm  14572  rlimdm  14623  iserex  14728  caucvgrlem2  14746  caucvgr  14747  caurcvg2  14749  caucvg  14750  fsumcvg3  14801  cvgcmpce  14888  climcnds  14921  trirecip  14933  ledm  17539  cmetcaulem  23414  ovoliunlem1  23610  mbflimlem  23775  dvaddf  24046  dvmulf  24047  dvcof  24052  dvcnv  24081  abelthlem5  24530  emcllem6  25079  lgamgulmlem4  25110  hlimcaui  28618  brfvrcld2  38767  sumnnodd  40606  climliminf  40782  stirlinglem12  41045  fouriersw  41191  rlimdmafv  42031  rlimdmafv2  42112