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 C_ B -> `' A C_ `' B )

Proof

Step	Hyp	Ref	Expression
1		ssbr	|- ( A C_ B -> ( y A x -> y B x ) )
2	1	ssopab2dv	|- ( A C_ B -> { <. x , y >. | y A x } C_ { <. x , y >. | y B x } )
3		df-cnv	|- `' A = { <. x , y >. | y A x }
4		df-cnv	|- `' B = { <. x , y >. | y B x }
5	2 3 4	3sstr4g	|- ( A C_ B -> `' A C_ `' B )