Theorem releldmi 5394

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

Syntax hints:   → wi 4   ∈ wcel 2030   class class class wbr 4685  dom cdm 5143  Rel wrel 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-rel 5150  df-dm 5153

This theorem is referenced by:  fpwwe2lem11  9500  fpwwe2lem12  9501  fpwwe2lem13  9502  rlimpm  14275  rlimdm  14326  iserex  14431  caucvgrlem2  14449  caucvgr  14450  caurcvg2  14452  caucvg  14453  fsumcvg3  14504  cvgcmpce  14594  climcnds  14627  trirecip  14639  ledm  17271  cmetcaulem  23132  ovoliunlem1  23316  mbflimlem  23479  dvaddf  23750  dvmulf  23751  dvcof  23756  dvcnv  23785  abelthlem5  24234  emcllem6  24772  lgamgulmlem4  24803  hlimcaui  28221  brfvrcld2  38301  sumnnodd  40180  climliminf  40356  stirlinglem12  40620  fouriersw  40766  rlimdmafv  41578