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

Theorem eldm2 4876
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 4874 . 2  |-  ( A  e.  _V  ->  ( A  e.  dom  B  <->  E. y <. A ,  y >.  e.  B ) )
31, 2ax-mp 10 1  |-  ( A  e.  dom  B  <->  E. y <. A ,  y >.  e.  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   E.wex 1533    e. wcel 1688   _Vcvv 2789   <.cop 3644   dom cdm 4688
This theorem is referenced by:  dmss  4877  opeldm  4881  dmin  4885  dmiun  4886  dmuni  4887  dm0  4891  reldm0  4895  dmrnssfld  4937  dmcoss  4943  dmcosseq  4945  dmres  4975  iss  4997  dmsnopg  5142  relssdmrn  5191  funssres  5259  fun11iun  5458  dmfco  5554  axdc3lem2  8072  gsum2d2  15219  cnlnssadj  22652  dfdm5  23533  wfrlem12  23668  frrlem11  23694  tfrqfree  23896  dmrngcmp  25150
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  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