Metamath Proof Explorer

Theorem resss

Description: A class includes its restriction. Exercise 15 of TakeutiZaring p. 25. (Contributed by NM, 2-Aug-1994)

Ref Expression
Assertion resss 
|- ( A |` B ) C_ A

Proof

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