Metamath Proof Explorer

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 C_ A

Proof

Step Hyp Ref Expression
1 cnvcnv2 
 |-  `' `' A = ( A |` _V )
2 resss 
 |-  ( A |` _V ) C_ A
3 1 2 eqsstri 
 |-  `' `' A C_ A