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)

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

Proof

Step	Hyp	Ref	Expression
1		df-rab	$$⊢\left\{x\in \varnothing |\phi \right\}=\left\{x|\left(x\in \varnothing \wedge \phi \right)\right\}$$
2		ab0	$$⊢\left\{x|\left(x\in \varnothing \wedge \phi \right)\right\}=\varnothing \leftrightarrow \forall x\neg \left(x\in \varnothing \wedge \phi \right)$$
3		noel	$$⊢\neg x\in \varnothing$$
4	3	intnanr	$$⊢\neg \left(x\in \varnothing \wedge \phi \right)$$
5	2 4	mpgbir	$$⊢\left\{x|\left(x\in \varnothing \wedge \phi \right)\right\}=\varnothing$$
6	1 5	eqtri	$$⊢\left\{x\in \varnothing |\phi \right\}=\varnothing$$