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

Theorem eldm2 4865
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 4863 . 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 1537    e. wcel 1621   _Vcvv 2763   <.cop 3617   dom cdm 4661
This theorem is referenced by:  dmss  4866  opeldm  4870  dmin  4874  dmiun  4875  dmuni  4876  dm0  4880  reldm0  4884  dmrnssfld  4926  dmcoss  4932  dmcosseq  4934  dmres  4964  iss  4986  dmsnopg  5131  relssdmrn  5180  funssres  5232  fun11iun  5431  dmfco  5527  axdc3lem2  8045  gsum2d2  15187  cnlnssadj  22620  dfdm5  23501  wfrlem12  23636  frrlem11  23662  tfrqfree  23864  dmrngcmp  25118
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 2239
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-br 3998  df-dm 4679
  Copyright terms: Public domain W3C validator