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)

Ref Expression
Assertion cnvcnvss 
|- `' `' A C_ A

Proof

Step Hyp Ref Expression
1 cnvcnv 
 |-  `' `' A = ( A i^i ( _V X. _V ) )
2 inss1 
 |-  ( A i^i ( _V X. _V ) ) C_ A
3 1 2 eqsstri 
 |-  `' `' A C_ A