Syntax Definition wlim 2200

Description: Extend the definition of a wff to include the limit ordinal predicate.

Hypothesis

Ref	Expression
cA	class A

Assertion

Ref	Expression
wlim	wff Lim A

See definition df-lim 2204 for more information.

metamath.org