Theorem elimasn

Description: Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Hypotheses	elimasn.1	|- B e. _V
	elimasn.2	|- C e. _V
Assertion	elimasn	|- ( C e. ( A " { B } ) <-> <. B , C >. e. A )

Proof

Step	Hyp	Ref	Expression
1		elimasn.1	|- B e. _V
2		elimasn.2	|- C e. _V
3		breq2	|- ( x = C -> ( B A x <-> B A C ) )
4		imasng	|- ( B e. _V -> ( A " { B } ) = { x | B A x } )
5	1 4	ax-mp	|- ( A " { B } ) = { x | B A x }
6	2 3 5	elab2	|- ( C e. ( A " { B } ) <-> B A C )
7		df-br	|- ( B A C <-> <. B , C >. e. A )
8	6 7	bitri	|- ( C e. ( A " { B } ) <-> <. B , C >. e. A )