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

Theorem eldm 5205
Description: Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.)
Hypothesis
Ref Expression
eldm.1
Assertion
Ref Expression
eldm
Distinct variable groups:   ,   ,

Proof of Theorem eldm
StepHypRef Expression
1 eldm.1 . 2
2 eldmg 5203 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  E.wex 1612  e.wcel 1818   cvv 3109   class class class wbr 4452  domcdm 5004
This theorem is referenced by:  dmi  5222  dmcoss  5267  dmcosseq  5269  dminss  5425  dmsnn0  5478  dffun7  5619  dffun8  5620  fnres  5702  opabiota  5936  fndmdif  5991  dff3  6044  frxp  6910  suppvalbr  6922  reldmtpos  6982  dmtpos  6986  aceq3lem  8522  axdc2lem  8849  axdclem2  8921  fpwwe2lem12  9040  nqerf  9329  shftdm  12904  xpsfrnel2  14962  bcthlem4  21766  dchrisumlem3  23676  eupath  24981  fundmpss  29196  elfix  29553  fnsingle  29569  fnimage  29579  funpartlem  29592  dfrdg4  29600  prtlem16  30610
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-dm 5014
  Copyright terms: Public domain W3C validator