Metamath Proof Explorer


Syntax definition cima

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

Ref Expression
Assertion cima class ( 𝐴𝐵 )