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

Metamath Proof Explorer

Theorem elqsn0

Description: A quotient set does not contain the empty set. (Contributed by NM, 24-Aug-1995)

Ref Expression
Assertion elqsn0 ⊢ dom ⁡ R = A ∧ B ∈ A / R → B ≠ ∅

Proof

Step Hyp Ref Expression
1 eqid ⊢ A / R = A / R
2 neeq1 ⊢ x R = B → x R ≠ ∅ ↔ B ≠ ∅
3 eleq2 ⊢ dom ⁡ R = A → x ∈ dom ⁡ R ↔ x ∈ A
4 3 biimpar ⊢ dom ⁡ R = A ∧ x ∈ A → x ∈ dom ⁡ R
5 ecdmn0 ⊢ x ∈ dom ⁡ R ↔ x R ≠ ∅
6 4 5 sylib ⊢ dom ⁡ R = A ∧ x ∈ A → x R ≠ ∅
7 1 2 6 ectocld ⊢ dom ⁡ R = A ∧ B ∈ A / R → B ≠ ∅