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

Metamath Proof Explorer

Theorem n0elqs

Description: Two ways of expressing that the empty set is not an element of a quotient set. (Contributed by Peter Mazsa, 5-Dec-2019)

Ref Expression
Assertion n0elqs ⊢ ¬ ∅ ∈ A / R ↔ A ⊆ dom ⁡ R

Proof

Step Hyp Ref Expression
1 ecdmn0 ⊢ x ∈ dom ⁡ R ↔ x R ≠ ∅
2 1 ralbii ⊢ ∀ x ∈ A x ∈ dom ⁡ R ↔ ∀ x ∈ A x R ≠ ∅
3 dfss3 ⊢ A ⊆ dom ⁡ R ↔ ∀ x ∈ A x ∈ dom ⁡ R
4 nne ⊢ ¬ x R ≠ ∅ ↔ x R = ∅
5 4 rexbii ⊢ ∃ x ∈ A ¬ x R ≠ ∅ ↔ ∃ x ∈ A x R = ∅
6 5 notbii ⊢ ¬ ∃ x ∈ A ¬ x R ≠ ∅ ↔ ¬ ∃ x ∈ A x R = ∅
7 dfral2 ⊢ ∀ x ∈ A x R ≠ ∅ ↔ ¬ ∃ x ∈ A ¬ x R ≠ ∅
8 0ex ⊢ ∅ ∈ V
9 8 elqs ⊢ ∅ ∈ A / R ↔ ∃ x ∈ A ∅ = x R
10 eqcom ⊢ ∅ = x R ↔ x R = ∅
11 10 rexbii ⊢ ∃ x ∈ A ∅ = x R ↔ ∃ x ∈ A x R = ∅
12 9 11 bitri ⊢ ∅ ∈ A / R ↔ ∃ x ∈ A x R = ∅
13 12 notbii ⊢ ¬ ∅ ∈ A / R ↔ ¬ ∃ x ∈ A x R = ∅
14 6 7 13 3bitr4ri ⊢ ¬ ∅ ∈ A / R ↔ ∀ x ∈ A x R ≠ ∅
15 2 3 14 3bitr4ri ⊢ ¬ ∅ ∈ A / R ↔ A ⊆ dom ⁡ R