Metamath Proof Explorer


Syntax definition cint

Description: Extend class notation to include the intersection of a class. Read: "intersection (of) A ".

Ref Expression
Assertion cint class A