Metamath Proof Explorer


Syntax definition cseq

Description: Extend class notation with recursive sequence builder.

Ref Expression
Assertion cseq classseqM+˙F