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

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

Proof of Theorem eldm2
StepHypRef Expression
1 eldm.1 . 2  |-  A  e. 
_V
2 eldm2g 5050 . 2  |-  ( A  e.  _V  ->  ( A  e.  dom  B  <->  E. y <. A ,  y >.  e.  B ) )
31, 2ax-mp 5 1  |-  ( A  e.  dom  B  <->  E. y <. A ,  y >.  e.  B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189   E.wex 1674    e. wcel 1898   _Vcvv 3057   <.cop 3986   dom cdm 4853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417  df-dm 4863
This theorem is referenced by:  dmss  5053  opeldm  5057  dmin  5061  dmiun  5062  dmuni  5063  dm0  5067  reldm0  5071  dmrnssfld  5112  dmcoss  5113  dmcosseq  5115  dmres  5144  iss  5171  dmsnopg  5326  relssdmrn  5375  funssres  5641  dmfco  5962  fun11iun  6780  wfrlem12  7073  axdc3lem2  8907  gsum2d2  17655  cnlnssadj  27782  prsdm  28769  eldm3  30451  dfdm5  30467  frrlem11  30575
  Copyright terms: Public domain W3C validator