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	|- { x e. (/) | ph } = (/)

Proof

Step	Hyp	Ref	Expression
1		rex0	|- -. E. x e. (/) -. ph
2		dfral2	|- ( A. x e. (/) ph <-> -. E. x e. (/) -. ph )
3	1 2	mpbir	|- A. x e. (/) ph
4	3	rspec	|- ( x e. (/) -> ph )
5	4	rabeqc	|- { x e. (/) | ph } = (/)