Home
Metamath Proof Explorer
< Previous
Next >
Related theorems
Unicode version
Syntax Definition
cvv
1802
Description:
Extend class notation to include the universal class symbol.
Assertion
Ref
Expression
cvv
See definition
df-v
1803
for more information.
Colors of variables:
wff
set
class
Copyright terms:
Public domain