Theorem rab0OLD

Description: Obsolete version of rab0 as of 10-Jun-2026. (Contributed by NM, 15-Oct-2003) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof shortened by JJ, 14-Jul-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	rab0OLD	⊢ { 𝑥 ∈ ∅ ∣ 𝜑 } = ∅

Proof

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