Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cfi Unicode version

Syntax Definition cfi 7890
 Description: Extend class notation with the function whose value is the class of all the finite intersections of the elements of a given set.
Assertion
Ref Expression
cfi