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

Step	Hyp	Ref	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 ) )
3	1, 2	ax-mp 5	1 |- ( A e. dom B <-> E. y <. A , y >. e. B )

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