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

Theorem eldm 4875
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 4873 . 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 1529    e. wcel 1685   _Vcvv 2789   class class class wbr 4024   dom cdm 4688
This theorem is referenced by:  dmi  4892  dmcoss  4943  dmcosseq  4945  dminss  5094  dmsnn0  5136  dffun7  5246  dffun8  5247  fnres  5325  fndmdif  5590  dff3  5634  frxp  6186  reldmtpos  6203  dmtpos  6207  opabiota  6286  aceq3lem  7742  axdc2lem  8069  axdclem2  8142  fpwwe2lem12  8258  nqerf  8549  shftdm  11560  xpsfrnel2  13461  bcthlem4  18743  dchrisumlem3  20634  eupath  23309  fundmpss  23523  elfix  23851  fnsingle  23865  fnimage  23875  funpartfun  23888  funpartfv  23890  dfrdg4  23895  dmhmph  24932  prtlem16  26136
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025  df-dm 4698
  Copyright terms: Public domain W3C validator