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

Theorem eldm2 5033
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 5031 . 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 184   E.wex 1586    e. wcel 1756   _Vcvv 2967   <.cop 3878   dom cdm 4835
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288  df-dm 4845
This theorem is referenced by:  dmss  5034  opeldm  5038  dmin  5042  dmiun  5043  dmuni  5044  dm0  5048  reldm0  5052  dmrnssfld  5093  dmcoss  5094  dmcosseq  5096  dmres  5126  iss  5149  dmsnopg  5305  relssdmrn  5353  funssres  5453  dmfco  5760  fun11iun  6532  axdc3lem2  8612  gsum2d2  16454  cnlnssadj  25435  prsdm  26296  eldm3  27523  dfdm5  27538  wfrlem12  27686  frrlem11  27731  tfrqfree  27933
  Copyright terms: Public domain W3C validator