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

Theorem eldm 5189
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 5187 . 2  |-  ( A  e.  _V  ->  ( A  e.  dom  B  <->  E. y  A B y ) )
31, 2ax-mp 5 1  |-  ( A  e.  dom  B  <->  E. y  A B y )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   E.wex 1617    e. wcel 1823   _Vcvv 3106   class class class wbr 4439   dom cdm 4988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-dm 4998
This theorem is referenced by:  dmi  5206  dmcoss  5251  dmcosseq  5253  dminss  5405  dmsnn0  5456  dffun7  5596  dffun8  5597  fnres  5679  opabiota  5911  fndmdif  5967  dff3  6020  frxp  6883  suppvalbr  6895  reldmtpos  6955  dmtpos  6959  aceq3lem  8492  axdc2lem  8819  axdclem2  8891  fpwwe2lem12  9008  nqerf  9297  shftdm  12986  xpsfrnel2  15054  bcthlem4  21932  dchrisumlem3  23874  eupath  25183  fundmpss  29437  elfix  29781  fnsingle  29797  fnimage  29807  funpartlem  29820  dfrdg4  29828  prtlem16  30850
  Copyright terms: Public domain W3C validator