This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		df-rab	⊢ { 𝑥 ∈ ∅ ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ ∅ ∧ 𝜑 ) }
2		ab0	⊢ ( { 𝑥 ∣ ( 𝑥 ∈ ∅ ∧ 𝜑 ) } = ∅ ↔ ∀ 𝑥 ¬ ( 𝑥 ∈ ∅ ∧ 𝜑 ) )
3		noel	⊢ ¬ 𝑥 ∈ ∅
4	3	intnanr	⊢ ¬ ( 𝑥 ∈ ∅ ∧ 𝜑 )
5	2 4	mpgbir	⊢ { 𝑥 ∣ ( 𝑥 ∈ ∅ ∧ 𝜑 ) } = ∅
6	1 5	eqtri	⊢ { 𝑥 ∈ ∅ ∣ 𝜑 } = ∅