Theorem elimasng1

Description: Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006) Revise to use df-br and to prove elimasn1 from it. (Revised by BJ, 16-Oct-2024)

	Ref	Expression
Assertion	elimasng1	$$⊢\left(B\in V\wedge C\in W\right)\to \left(C\in A\left[\left\{B\right\}\right]\leftrightarrow BAC\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(B\in V\wedge C\in W\right)\to C\in W$$
2		imasng	$$⊢B\in V\to A\left[\left\{B\right\}\right]=\left\{x|BAx\right\}$$
3	2	adantr	$$⊢\left(B\in V\wedge C\in W\right)\to A\left[\left\{B\right\}\right]=\left\{x|BAx\right\}$$
4		simpr	$$⊢\left(\left(B\in V\wedge C\in W\right)\wedge x=C\right)\to x=C$$
5	4	breq2d	$$⊢\left(\left(B\in V\wedge C\in W\right)\wedge x=C\right)\to \left(BAx\leftrightarrow BAC\right)$$
6	1 3 5	elabd2	$$⊢\left(B\in V\wedge C\in W\right)\to \left(C\in A\left[\left\{B\right\}\right]\leftrightarrow BAC\right)$$