Theorem elima3

Description: Membership in an image. Theorem 34 of Suppes p. 65. (Contributed by NM, 14-Aug-1994)

	Ref	Expression
Hypothesis	elima.1	|- A e. _V
Assertion	elima3	|- ( A e. ( B " C ) <-> E. x ( x e. C /\ <. x , A >. e. B ) )

Proof

Step	Hyp	Ref	Expression
1		elima.1	|- A e. _V
2	1	elima2	|- ( A e. ( B " C ) <-> E. x ( x e. C /\ x B A ) )
3		df-br	|- ( x B A <-> <. x , A >. e. B )
4	3	anbi2i	|- ( ( x e. C /\ x B A ) <-> ( x e. C /\ <. x , A >. e. B ) )
5	4	exbii	|- ( E. x ( x e. C /\ x B A ) <-> E. x ( x e. C /\ <. x , A >. e. B ) )
6	2 5	bitri	|- ( A e. ( B " C ) <-> E. x ( x e. C /\ <. x , A >. e. B ) )