Syntax Definition wcdeq 2972

Description: Extend wff notation to include conditional equality. This is a technical device used in the proof that F/ is the not-free predicate, and that definitions are conservative as a result.

Hypotheses

Ref	Expression
wph	wff ph
vx	setvar x
vy	setvar y

Assertion

Ref	Expression
wcdeq	wff CondEq ( x = y -> ph )

See definition df-cdeq 2973 for more information.