This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elimasn

Description: Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by BJ, 16-Oct-2024) TODO: replace existing usages by usages of elimasn1 , remove, and relabel elimasn1 to "elimasn".

	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		elimasng	\|- ( ( B e. _V /\ C e. _V ) -> ( C e. ( A " { B } ) <-> <. B , C >. e. A ) )
4	1 2 3	mp2an	\|- ( C e. ( A " { B } ) <-> <. B , C >. e. A )