Description: Membership in an image. Theorem 34 of Suppes p. 65. (Contributed by NM, 11-Aug-2004)
Ref | Expression | ||
---|---|---|---|
Hypothesis | elima.1 | |- A e. _V |
|
Assertion | elima2 | |- ( A e. ( B " C ) <-> E. x ( x e. C /\ x B A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elima.1 | |- A e. _V |
|
2 | 1 | elima | |- ( A e. ( B " C ) <-> E. x e. C x B A ) |
3 | df-rex | |- ( E. x e. C x B A <-> E. x ( x e. C /\ x B A ) ) |
|
4 | 2 3 | bitri | |- ( A e. ( B " C ) <-> E. x ( x e. C /\ x B A ) ) |