term-obj - bfol.mm Proof Explorer

	bfol.mm Proof Explorer		< Wrap Next > Nearby theorems
Mirrors > Home > PE Home > Th. List > term-obj

Syntax Definition term-obj 1

Description: If '𝑥' is an object variable, then '𝑥' is a term.

**Hypothesis**
Ref	Expression
objvar-x	objvar 𝑥

**Assertion**
Ref	Expression
term-obj	term 𝑥

This syntax is primitive. The first axiom using it is ax-L1 11.

Colors of variables: wff objvar term class