HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Syntax Definition cint 2537
Description: Extend class notation to include the intersection of a class (read: 'intersect A ').
Hypothesis
Ref Expression
cA class A
Assertion
Ref Expression
cint class |^|A

See definition df-int 2538 for more information.

Colors of variables: wff set class
Copyright terms: Public domain