Theorem elimasng1

Description: Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006) Revise to use df-br and to prove elimasn1 from it. (Revised by BJ, 16-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( B e. V /\ C e. W ) -> C e. W )
2		imasng	|- ( B e. V -> ( A " { B } ) = { x | B A x } )
3	2	adantr	|- ( ( B e. V /\ C e. W ) -> ( A " { B } ) = { x | B A x } )
4		simpr	|- ( ( ( B e. V /\ C e. W ) /\ x = C ) -> x = C )
5	4	breq2d	|- ( ( ( B e. V /\ C e. W ) /\ x = C ) -> ( B A x <-> B A C ) )
6	1 3 5	elabd2	|- ( ( B e. V /\ C e. W ) -> ( C e. ( A " { B } ) <-> B A C ) )