Theorem cnvss

Description: Subset theorem for converse. (Contributed by NM, 22-Mar-1998) (Proof shortened by Kyle Wyonch, 27-Apr-2021)

	Ref	Expression
Assertion	cnvss	$$⊢A\subseteq B\to A^{-1}\subseteq B^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		ssbr	$$⊢A\subseteq B\to \left(yAx\to yBx\right)$$
2	1	ssopab2dv	$$⊢A\subseteq B\to \left\{⟨x,y⟩|yAx\right\}\subseteq \left\{⟨x,y⟩|yBx\right\}$$
3		df-cnv	$$⊢A^{-1}=\left\{⟨x,y⟩|yAx\right\}$$
4		df-cnv	$$⊢B^{-1}=\left\{⟨x,y⟩|yBx\right\}$$
5	2 3 4	3sstr4g	$$⊢A\subseteq B\to A^{-1}\subseteq B^{-1}$$