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

Proof

Step Hyp Ref Expression
1 cnvcnv ⊢ ◡ ◡ 𝐴 = ( 𝐴 ∩ ( V × V ) )
2 inss1 ⊢ ( 𝐴 ∩ ( V × V ) ) ⊆ 𝐴
3 1 2 eqsstri ⊢ ◡ ◡ 𝐴 ⊆ 𝐴