Theorem elimasn

Description: Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Hypotheses	elimasn.1	$$⊢B\in \mathrm{V}$$
	elimasn.2	$$⊢C\in \mathrm{V}$$
Assertion	elimasn	$$⊢C\in A\left[\left\{B\right\}\right]\leftrightarrow ⟨B,C⟩\in A$$

Proof

Step	Hyp	Ref	Expression
1		elimasn.1	$$⊢B\in \mathrm{V}$$
2		elimasn.2	$$⊢C\in \mathrm{V}$$
3		breq2	$$⊢x=C\to \left(BAx\leftrightarrow BAC\right)$$
4		imasng	$$⊢B\in \mathrm{V}\to A\left[\left\{B\right\}\right]=\left\{x|BAx\right\}$$
5	1 4	ax-mp	$$⊢A\left[\left\{B\right\}\right]=\left\{x|BAx\right\}$$
6	2 3 5	elab2	$$⊢C\in A\left[\left\{B\right\}\right]\leftrightarrow BAC$$
7		df-br	$$⊢BAC\leftrightarrow ⟨B,C⟩\in A$$
8	6 7	bitri	$$⊢C\in A\left[\left\{B\right\}\right]\leftrightarrow ⟨B,C⟩\in A$$