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

Theorem eldm 4850
Description: Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.)
Hypothesis
Ref Expression
eldm.1  |-  A  e. 
_V
Assertion
Ref Expression
eldm  |-  ( A  e.  dom  B  <->  E. y  A B y )
Distinct variable groups:    y, A    y, B

Proof of Theorem eldm
StepHypRef Expression
1 eldm.1 . 2  |-  A  e. 
_V
2 eldmg 4848 . 2  |-  ( A  e.  _V  ->  ( A  e.  dom  B  <->  E. y  A B y ) )
31, 2ax-mp 10 1  |-  ( A  e.  dom  B  <->  E. y  A B y )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   E.wex 1537    e. wcel 1621   _Vcvv 2757   class class class wbr 3983   dom cdm 4647
This theorem is referenced by:  dmi  4867  dmcoss  4918  dmcosseq  4920  dminss  5069  dmsnn0  5111  dffun7  5205  dffun8  5206  fnres  5284  fndmdif  5549  dff3  5593  frxp  6145  reldmtpos  6162  dmtpos  6166  opabiota  6245  aceq3lem  7701  axdc2lem  8028  axdclem2  8101  fpwwe2lem12  8217  nqerf  8508  shftdm  11517  xpsfrnel2  13415  bcthlem4  18697  dchrisumlem3  20588  eupath  23263  fundmpss  23477  elfix  23805  fnsingle  23819  fnimage  23829  funpartfun  23842  funpartfv  23844  dfrdg4  23849  dmhmph  24886  prtlem16  26090
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609  df-br 3984  df-dm 4665
  Copyright terms: Public domain W3C validator