MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  releldmi Structured version   Visualization version   GIF version

Theorem releldmi 5900
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
StepHypRef Expression
1 releldm.1 . 2 Rel 𝑅
2 releldm 5896 . 2 ((Rel 𝑅𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
31, 2mpan 689 1 (𝐴𝑅𝐵𝐴 ∈ dom 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107   class class class wbr 5104  dom cdm 5631  Rel wrel 5636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pr 5383
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-xp 5637  df-rel 5638  df-dm 5641
This theorem is referenced by:  fpwwe2lem10  10510  fpwwe2lem11  10511  fpwwe2lem12  10512  rlimpm  15318  rlimdm  15369  iserex  15477  caucvgrlem2  15495  caucvgr  15496  caurcvg2  15498  caucvg  15499  fsumcvg3  15550  cvgcmpce  15639  climcnds  15672  trirecip  15684  ledm  18415  cmetcaulem  24580  ovoliunlem1  24794  mbflimlem  24959  dvaddf  25234  dvmulf  25235  dvcof  25240  dvcnv  25269  abelthlem5  25722  emcllem6  26278  lgamgulmlem4  26309  hlimcaui  29983  brfvrcld2  41763  sumnnodd  43662  climliminf  43838  stirlinglem12  44117  fouriersw  44263  rlimdmafv  45200  rlimdmafv2  45281
  Copyright terms: Public domain W3C validator