Metamath Proof Explorer


Syntax definition corvc

Description: Extend class notation to include the preimage set mapping operator.

Ref Expression
Assertion corvc class ∘ RV/c ⁡ R