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

Theorem releldmi 5959
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 5955 . 2 ((Rel 𝑅𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
31, 2mpan 690 1 (𝐴𝑅𝐵𝐴 ∈ dom 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108   class class class wbr 5143  dom cdm 5685  Rel wrel 5690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-dm 5695
This theorem is referenced by:  fpwwe2lem10  10680  fpwwe2lem11  10681  fpwwe2lem12  10682  rlimpm  15536  rlimdm  15587  iserex  15693  caucvgrlem2  15711  caucvgr  15712  caurcvg2  15714  caucvg  15715  fsumcvg3  15765  cvgcmpce  15854  climcnds  15887  trirecip  15899  ledm  18635  cmetcaulem  25322  ovoliunlem1  25537  mbflimlem  25702  dvaddf  25979  dvmulf  25980  dvcof  25986  dvcnv  26015  abelthlem5  26479  emcllem6  27044  lgamgulmlem4  27075  hlimcaui  31255  brfvrcld2  43705  sumnnodd  45645  climliminf  45821  stirlinglem12  46100  fouriersw  46246  rlimdmafv  47189  rlimdmafv2  47270
  Copyright terms: Public domain W3C validator