Metamath Proof Explorer


Syntax definition cres

Description: Extend the definition of a class to include the restriction of a class. Read: "the restriction of A to B ".

Ref Expression
Assertion cres
class ( A |` B )