Metamath Proof Explorer


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 V
Assertion eldm2 A dom B y A y B

Proof

Step Hyp Ref Expression
1 eldm.1 A V
2 eldm2g A V A dom B y A y B
3 1 2 ax-mp A dom B y A y B