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

Metamath Proof Explorer

Theorem n0eldmqseq

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

Ref Expression
Assertion n0eldmqseq ⊢ dom ⁡ R / R = A → ¬ ∅ ∈ A

Proof

Step Hyp Ref Expression
1 n0eldmqs ⊢ ¬ ∅ ∈ dom ⁡ R / R
2 eleq2 ⊢ dom ⁡ R / R = A → ∅ ∈ dom ⁡ R / R ↔ ∅ ∈ A
3 1 2 mtbii ⊢ dom ⁡ R / R = A → ¬ ∅ ∈ A