Syntax Definition wtr 2041

Description: Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35.

Hypothesis

Ref	Expression
cA	class A

Assertion

Ref	Expression
wtr	wff Tr A

See definition df-tr 2042 for more information.

metamath.org