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	⊢ { 𝑥 ∈ ∅ ∣ 𝜑 } = ∅

Proof

Step	Hyp	Ref	Expression
1		rex0	⊢ ¬ ∃ 𝑥 ∈ ∅ ¬ 𝜑
2		dfral2	⊢ ( ∀ 𝑥 ∈ ∅ 𝜑 ↔ ¬ ∃ 𝑥 ∈ ∅ ¬ 𝜑 )
3	1 2	mpbir	⊢ ∀ 𝑥 ∈ ∅ 𝜑
4	3	rspec	⊢ ( 𝑥 ∈ ∅ → 𝜑 )
5	4	rabeqc	⊢ { 𝑥 ∈ ∅ ∣ 𝜑 } = ∅