Theorem elinisegg

Description: Membership in the inverse image of a singleton. (Contributed by NM, 28-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) Put in closed form and shorten. (Revised by BJ, 16-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		elimasng1	|- ( ( B e. V /\ C e. W ) -> ( C e. ( `' A " { B } ) <-> B `' A C ) )
2		brcnvg	|- ( ( B e. V /\ C e. W ) -> ( B `' A C <-> C A B ) )
3	1 2	bitrd	|- ( ( B e. V /\ C e. W ) -> ( C e. ( `' A " { B } ) <-> C A B ) )