Metamath Proof Explorer

Theorem relss

Description: Subclass theorem for relation predicate. Theorem 2 of Suppes p. 58. (Contributed by NM, 15-Aug-1994)

Ref Expression
Assertion relss 
|- ( A C_ B -> ( Rel B -> Rel A ) )

Proof

Step Hyp Ref Expression
1 sstr2 
 |-  ( A C_ B -> ( B C_ ( _V X. _V ) -> A C_ ( _V X. _V ) ) )
2 df-rel 
 |-  ( Rel B <-> B C_ ( _V X. _V ) )
3 df-rel 
 |-  ( Rel A <-> A C_ ( _V X. _V ) )
4 1 2 3 3imtr4g 
 |-  ( A C_ B -> ( Rel B -> Rel A ) )