Theorem brcnvssr

Description: The converse of a subset relation swaps arguments. (Contributed by Peter Mazsa, 1-Aug-2019)

	Ref	Expression
Assertion	brcnvssr	$$⊢A\in V\to \left(A{\mathrm{S}}^{-1}B\leftrightarrow B\subseteq A\right)$$

Proof

Step	Hyp	Ref	Expression
1		relssr	$$⊢\mathrm{Rel}\mathrm{S}$$
2	1	relbrcnv	$$⊢A{\mathrm{S}}^{-1}B\leftrightarrow B\mathrm{S}A$$
3		brssr	$$⊢A\in V\to \left(B\mathrm{S}A\leftrightarrow B\subseteq A\right)$$
4	2 3	bitrid	$$⊢A\in V\to \left(A{\mathrm{S}}^{-1}B\leftrightarrow B\subseteq A\right)$$