Theorem 0qs

Description: Quotient set with the empty set. (Contributed by Peter Mazsa, 14-Sep-2019)

	Ref	Expression
Assertion	0qs	⊢ ( ∅ / 𝑅 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		df-qs	⊢ ( ∅ / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ ∅ 𝑦 = [ 𝑥 ] 𝑅 }
2		rex0	⊢ ¬ ∃ 𝑥 ∈ ∅ 𝑦 = [ 𝑥 ] 𝑅
3	2	abf	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ ∅ 𝑦 = [ 𝑥 ] 𝑅 } = ∅
4	1 3	eqtri	⊢ ( ∅ / 𝑅 ) = ∅