Theorem rab0

Description: Any restricted class abstraction restricted to the empty set is empty. (Contributed by NM, 15-Oct-2003) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof shortened by JJ, 14-Jul-2021) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)

	Ref	Expression
Assertion	rab0	$$⊢\left\{x\in \varnothing |\phi \right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		rex0	$$⊢\neg \exists x\in \varnothing \neg \phi$$
2		dfral2	$$⊢\forall x\in \varnothing \phi \leftrightarrow \neg \exists x\in \varnothing \neg \phi$$
3	1 2	mpbir	$$⊢\forall x\in \varnothing \phi$$
4	3	rspec	$$⊢x\in \varnothing \to \phi$$
5	4	rabeqc	$$⊢\left\{x\in \varnothing |\phi \right\}=\varnothing$$