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

Theorem releldmi 5176
Description: The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015.)
Hypothesis
Ref Expression
releldm.1  |-  Rel  R
Assertion
Ref Expression
releldmi  |-  ( A R B  ->  A  e.  dom  R )

Proof of Theorem releldmi
StepHypRef Expression
1 releldm.1 . 2  |-  Rel  R
2 releldm 5172 . 2  |-  ( ( Rel  R  /\  A R B )  ->  A  e.  dom  R )
31, 2mpan 670 1  |-  ( A R B  ->  A  e.  dom  R )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   class class class wbr 4392   dom cdm 4940   Rel wrel 4945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4513  ax-nul 4521  ax-pr 4631
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3072  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-sn 3978  df-pr 3980  df-op 3984  df-br 4393  df-opab 4451  df-xp 4946  df-rel 4947  df-dm 4950
This theorem is referenced by:  fpwwe2lem11  8910  fpwwe2lem12  8911  fpwwe2lem13  8912  rlimpm  13082  rlimdm  13133  iserex  13238  caucvgrlem2  13256  caucvgr  13257  caurcvg2  13259  caucvg  13260  fsumcvg3  13310  cvgcmpce  13385  climcnds  13418  trirecip  13429  ledm  15498  cmetcaulem  20917  ovoliunlem1  21103  mbflimlem  21263  dvaddf  21534  dvmulf  21535  dvcof  21540  dvcnv  21567  abelthlem5  22018  emcllem6  22512  hlimcaui  24776  lgamgulmlem4  27154  stirlinglem12  30020  rlimdmafv  30223
  Copyright terms: Public domain W3C validator