Theorem elimasng

Description: Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006) TODO: replace existing usages by usages of elimasng1 , remove, and relabel elimasng1 to "elimasng".

	Ref	Expression
Assertion	elimasng	|- ( ( B e. V /\ C e. W ) -> ( C e. ( A " { B } ) <-> <. B , C >. e. A ) )

Proof

Step	Hyp	Ref	Expression
1		elimasng1	|- ( ( B e. V /\ C e. W ) -> ( C e. ( A " { B } ) <-> B A C ) )
2		df-br	|- ( B A C <-> <. B , C >. e. A )
3	1 2	bitrdi	|- ( ( B e. V /\ C e. W ) -> ( C e. ( A " { B } ) <-> <. B , C >. e. A ) )