Theorem cnvcnvss

Description: The double converse of a class is a subclass. Exercise 2 of TakeutiZaring p. 25. (Contributed by NM, 23-Jul-2004) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)

	Ref	Expression
Assertion	cnvcnvss	$$⊢{A^{-1}}^{-1}\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		cnvcnv2	$$⊢{A^{-1}}^{-1}={A\upharpoonright }_{\mathrm{V}}$$
2		resss	$$⊢{A\upharpoonright }_{\mathrm{V}}\subseteq A$$
3	1 2	eqsstri	$$⊢{A^{-1}}^{-1}\subseteq A$$