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 A

Proof

Step Hyp Ref Expression
1 df-res A B = A B × V
2 inss1 A B × V A
3 1 2 eqsstri A B A