Theorem elinisegg

Description: Membership in the inverse image of a singleton. (Contributed by NM, 28-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) Put in closed form and shorten proof. (Revised by BJ, 16-Oct-2024)

	Ref	Expression
Assertion	elinisegg	$$⊢\left(B\in V\wedge C\in W\right)\to \left(C\in A^{-1}\left[\left\{B\right\}\right]\leftrightarrow CAB\right)$$

Proof

Step	Hyp	Ref	Expression
1		elimasng1	$$⊢\left(B\in V\wedge C\in W\right)\to \left(C\in A^{-1}\left[\left\{B\right\}\right]\leftrightarrow B{A}^{-1}C\right)$$
2		brcnvg	$$⊢\left(B\in V\wedge C\in W\right)\to \left(B{A}^{-1}C\leftrightarrow CAB\right)$$
3	1 2	bitrd	$$⊢\left(B\in V\wedge C\in W\right)\to \left(C\in A^{-1}\left[\left\{B\right\}\right]\leftrightarrow CAB\right)$$