Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
"Singletonization" and tagging
bj-ctag
Next ⟩
df-bj-tag
Metamath Proof Explorer
Ascii
Unicode
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