Metamath Proof Explorer


Syntax definition bj-ctag

Description: Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-ctag class tag A