Syntax Definition ccnv 2409

Description: Extend the definition of a class to include the converse of a class.

Hypothesis

Ref	Expression
cA	class A

Assertion

Ref	Expression
ccnv	class ◡A

See definition df-cnv 2426 for more information.

metamath.org