Syntax Definition wrex 2449

Description: Extend wff notation to include restricted existential quantification.

Hypotheses

Ref	Expression
wph	wff 𝜑
vx	setvar 𝑥
cA	class 𝐴

Assertion

Ref	Expression
wrex	wff ∃𝑥 ∈ 𝐴 𝜑

See definition df-rex 2454 for more information.