Theorem eldm2

Description: Membership in a domain. Theorem 4 of Suppes p. 59. (Contributed by NM, 1-Aug-1994)

	Ref	Expression
Hypothesis	eldm.1	|- A e. _V
Assertion	eldm2	|- ( A e. dom B <-> E. y <. A , y >. e. B )

Proof

Step	Hyp	Ref	Expression
1		eldm.1	|- A e. _V
2		eldm2g	|- ( A e. _V -> ( A e. dom B <-> E. y <. A , y >. e. B ) )
3	1 2	ax-mp	|- ( A e. dom B <-> E. y <. A , y >. e. B )