Syntax Definition c1st 3085

Description: Extend the definition of a class to include the first member an ordered pair function.

Assertion

Ref	Expression
c1st	class 1st

See definition df-1st 3087 for more information.

metamath.org