Theorem elimasng

Description: Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006) TODO: replace existing usages by usages of elimasng1 , remove, and relabel elimasng1 to "elimasng".

	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		elimasng1	$$⊢\left(B\in V\wedge C\in W\right)\to \left(C\in A\left[\left\{B\right\}\right]\leftrightarrow BAC\right)$$
2		df-br	$$⊢BAC\leftrightarrow ⟨B,C⟩\in A$$
3	1 2	bitrdi	$$⊢\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)$$