Theorem rex0

Description: Vacuous restricted existential quantification is false. (Contributed by NM, 15-Oct-2003)

	Ref	Expression
Assertion	rex0	$$⊢\neg \exists x\in \varnothing \phi$$

Proof

Step	Hyp	Ref	Expression
1		noel	$$⊢\neg x\in \varnothing$$
2	1	pm2.21i	$$⊢x\in \varnothing \to \neg \phi$$
3	2	nrex	$$⊢\neg \exists x\in \varnothing \phi$$