Theorem eliniseg2

Description: Eliminate the class existence constraint in eliniseg . (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by Mario Carneiro, 17-Nov-2015)

	Ref	Expression
Assertion	eliniseg2	$$⊢\mathrm{Rel}A\to \left(C\in A^{-1}\left[\left\{B\right\}\right]\leftrightarrow CAB\right)$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{A}^{-1}$$
2		elrelimasn	$$⊢\mathrm{Rel}{A}^{-1}\to \left(C\in A^{-1}\left[\left\{B\right\}\right]\leftrightarrow B{A}^{-1}C\right)$$
3	1 2	ax-mp	$$⊢C\in A^{-1}\left[\left\{B\right\}\right]\leftrightarrow B{A}^{-1}C$$
4		relbrcnvg	$$⊢\mathrm{Rel}A\to \left(B{A}^{-1}C\leftrightarrow CAB\right)$$
5	3 4	bitrid	$$⊢\mathrm{Rel}A\to \left(C\in A^{-1}\left[\left\{B\right\}\right]\leftrightarrow CAB\right)$$