Theorem elimasng

Description: Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006)

	Ref	Expression
Assertion	elimasng	$$⊢\left(B\in V\wedge C\in W\right)\to \left(C\in A\left[\left\{B\right\}\right]\leftrightarrow ⟨B,C⟩\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		sneq	$$⊢y=B\to \left\{y\right\}=\left\{B\right\}$$
2	1	imaeq2d	$$⊢y=B\to A\left[\left\{y\right\}\right]=A\left[\left\{B\right\}\right]$$
3	2	eleq2d	$$⊢y=B\to \left(z\in A\left[\left\{y\right\}\right]\leftrightarrow z\in A\left[\left\{B\right\}\right]\right)$$
4		opeq1	$$⊢y=B\to ⟨y,z⟩=⟨B,z⟩$$
5	4	eleq1d	$$⊢y=B\to \left(⟨y,z⟩\in A\leftrightarrow ⟨B,z⟩\in A\right)$$
6	3 5	bibi12d	$$⊢y=B\to \left(\left(z\in A\left[\left\{y\right\}\right]\leftrightarrow ⟨y,z⟩\in A\right)\leftrightarrow \left(z\in A\left[\left\{B\right\}\right]\leftrightarrow ⟨B,z⟩\in A\right)\right)$$
7		eleq1	$$⊢z=C\to \left(z\in A\left[\left\{B\right\}\right]\leftrightarrow C\in A\left[\left\{B\right\}\right]\right)$$
8		opeq2	$$⊢z=C\to ⟨B,z⟩=⟨B,C⟩$$
9	8	eleq1d	$$⊢z=C\to \left(⟨B,z⟩\in A\leftrightarrow ⟨B,C⟩\in A\right)$$
10	7 9	bibi12d	$$⊢z=C\to \left(\left(z\in A\left[\left\{B\right\}\right]\leftrightarrow ⟨B,z⟩\in A\right)\leftrightarrow \left(C\in A\left[\left\{B\right\}\right]\leftrightarrow ⟨B,C⟩\in A\right)\right)$$
11		vex	$$⊢y\in \mathrm{V}$$
12		vex	$$⊢z\in \mathrm{V}$$
13	11 12	elimasn	$$⊢z\in A\left[\left\{y\right\}\right]\leftrightarrow ⟨y,z⟩\in A$$
14	6 10 13	vtocl2g	$$⊢\left(B\in V\wedge C\in W\right)\to \left(C\in A\left[\left\{B\right\}\right]\leftrightarrow ⟨B,C⟩\in A\right)$$