Syntax Definition wrex 2476

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 2481 for more information.