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

Metamath Proof Explorer

Theorem n0elqs2

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

Ref Expression
Assertion n0elqs2 ⊢ ¬ ∅ ∈ A / R ↔ dom ⁡ R ↾ A = A

Proof

Step Hyp Ref Expression
1 n0elqs ⊢ ¬ ∅ ∈ A / R ↔ A ⊆ dom ⁡ R
2 ssdmres ⊢ A ⊆ dom ⁡ R ↔ dom ⁡ R ↾ A = A
3 1 2 bitri ⊢ ¬ ∅ ∈ A / R ↔ dom ⁡ R ↾ A = A