elimasni

Description: Membership in an image of a singleton. (Contributed by NM, 5-Aug-2010)

		Ref	Expression
	Assertion	elimasni	$⊢ C \in A [\{B\}] \to B A C$

Step	Hyp	Ref	Expression
1		noel	$⊢ \neg C \in \emptyset$
2		snprc	$⊢ \neg B \in V \leftrightarrow \{B\} = \emptyset$
3	2	biimpi	$⊢ \neg B \in V \to \{B\} = \emptyset$
4	3	imaeq2d	$⊢ \neg B \in V \to A [\{B\}] = A [\emptyset]$
5		ima0	$⊢ A [\emptyset] = \emptyset$
6	4 5	eqtrdi	$⊢ \neg B \in V \to A [\{B\}] = \emptyset$
7	6	eleq2d	$⊢ \neg B \in V \to (C \in A [\{B\}] \leftrightarrow C \in \emptyset)$
8	1 7	mtbiri	$⊢ \neg B \in V \to \neg C \in A [\{B\}]$
9	8	con4i	$⊢ C \in A [\{B\}] \to B \in V$
10		elex	$⊢ C \in A [\{B\}] \to C \in V$
11	9 10	jca	$⊢ C \in A [\{B\}] \to (B \in V \land C \in V)$
12		elimasng1	$⊢ (B \in V \land C \in V) \to (C \in A [\{B\}] \leftrightarrow B A C)$
13	12	biimpd	$⊢ (B \in V \land C \in V) \to (C \in A [\{B\}] \to B A C)$
14	11 13	mpcom	$⊢ C \in A [\{B\}] \to B A C$

Metamath Proof Explorer