Theorem releldmi 5943

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5114  dom cdm 5666  Rel wrel 5671

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-rel 5673  df-dm 5676

This theorem is used by:  fpwwe2lem10  10643  fpwwe2lem11  10644  fpwwe2lem12  10645  rlimpm  15577  rlimdm  15628  iserex  15734  caucvgrlem2  15752  caucvgr  15753  caurcvg2  15755  caucvg  15756  fsumcvg3  15806  cvgcmpce  15896  climcnds  15931  trirecip  15943  ledm  18671  cmetcaulem  25484  ovoliunlem1  25698  mbflimlem  25863  dvaddf  26138  dvmulf  26139  dvcof  26144  dvcnv  26173  abelthlem5  26635  emcllem6  27202  lgamgulmlem4  27233  hlimcaui  31625  brfvrcld2  44459  sumnnodd  46387  climliminf  46561  stirlinglem12  46840  fouriersw  46986  rlimdmafv  47955  rlimdmafv2  48036