wff-forall - bfol.mm Proof Explorer

	bfol.mm Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > PE Home > Th. List > wff-forall

Syntax Definition wff-forall 8

Description: If '𝑥' is a object variable and '𝜑' is a well formed formula, then '∀𝑥𝜑' is a well formed formula.

**Hypotheses**
Ref	Expression
wff-ph	wff 𝜑
objvar-x	objvar 𝑥

**Assertion**
Ref	Expression
wff-forall	wff ∀𝑥𝜑

This syntax is primitive. The first axiom using it is ax-GEN 15.

Colors of variables: wff objvar term class