Syntax Definition weq 797

Description: Extend wff definition to include atomic formulas using the equality predicate.

Hypotheses

Ref	Expression
vx	set x
vy	set y

Assertion

Ref	Expression
weq	wff x = y

This syntax is primitive. The first axiom using it is ax-8 798.

metamath.org