Theorem n0eldmqs

Description: The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 2-Mar-2018)

	Ref	Expression
Assertion	n0eldmqs	⊢ ¬ ∅ ∈ ( dom 𝑅 / 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ dom 𝑅 ⊆ dom 𝑅
2		n0elqs	⊢ ( ¬ ∅ ∈ ( dom 𝑅 / 𝑅 ) ↔ dom 𝑅 ⊆ dom 𝑅 )
3	1 2	mpbir	⊢ ¬ ∅ ∈ ( dom 𝑅 / 𝑅 )