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

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

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