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

Theorem eldm 4829
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 4827 . 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 2740   class class class wbr 3963   dom cdm 4626
This theorem is referenced by:  dmi  4846  dmcoss  4897  dmcosseq  4899  dminss  5048  dmsnn0  5090  dffun7  5184  dffun8  5185  fnres  5263  fndmdif  5528  dff3  5572  frxp  6124  reldmtpos  6141  dmtpos  6145  opabiota  6224  aceq3lem  7680  axdc2lem  8007  axdclem2  8080  fpwwe2lem12  8196  nqerf  8487  shftdm  11496  xpsfrnel2  13394  bcthlem4  18676  dchrisumlem3  20567  eupath  23242  fundmpss  23456  elfix  23784  fnsingle  23798  fnimage  23808  funpartfun  23821  funpartfv  23823  dfrdg4  23828  dmhmph  24865  prtlem16  26069
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 2523  df-v 2742  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-op 3590  df-br 3964  df-dm 4644
  Copyright terms: Public domain W3C validator