Syntax Definition wff-equals 6

Description: If '𝑡' and '𝑢' are terms, then '𝑡 = 𝑢' is a well formed formula.

Hypotheses

Ref	Expression
term-t	term 𝑡
term-u	term 𝑢

Assertion

Ref	Expression
wff-equals	wff 𝑡 = 𝑢

This syntax is primitive. The first axiom using it is ax-L6 18.