Theorem elimasn1

Description: Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) Use df-br and shorten proof. (Revised by BJ, 16-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		elimasn1.1	|- B e. _V
2		elimasn1.2	|- C e. _V
3		elimasng1	|- ( ( B e. _V /\ C e. _V ) -> ( C e. ( A " { B } ) <-> B A C ) )
4	1 2 3	mp2an	|- ( C e. ( A " { B } ) <-> B A C )