Theorem releldmi 5897

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

Syntax hints:   → wi 4   ∈ wcel 2119   class class class wbr 5079  dom cdm 5625  Rel wrel 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-xp 5631  df-rel 5632  df-dm 5635

This theorem is referenced by:  fpwwe2lem10  10561  fpwwe2lem11  10562  fpwwe2lem12  10563  rlimpm  15460  rlimdm  15511  iserex  15617  caucvgrlem2  15635  caucvgr  15636  caurcvg2  15638  caucvg  15639  fsumcvg3  15689  cvgcmpce  15779  climcnds  15814  trirecip  15826  ledm  18554  cmetcaulem  25280  ovoliunlem1  25494  mbflimlem  25659  dvaddf  25934  dvmulf  25935  dvcof  25940  dvcnv  25969  abelthlem5  26425  emcllem6  26989  lgamgulmlem4  27020  hlimcaui  31332  brfvrcld2  44143  sumnnodd  46082  climliminf  46256  stirlinglem12  46535  fouriersw  46681  rlimdmafv  47647  rlimdmafv2  47728