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	⊢ ◡ ◡ 𝐴 ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		cnvcnv2	⊢ ◡ ◡ 𝐴 = ( 𝐴 ↾ V )
2		resss	⊢ ( 𝐴 ↾ V ) ⊆ 𝐴
3	1 2	eqsstri	⊢ ◡ ◡ 𝐴 ⊆ 𝐴