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

Metamath Proof Explorer

Theorem n0elim

Description: Implication of that the empty set is not an element of a class. (Contributed by Peter Mazsa, 30-Dec-2024)

Ref Expression
Assertion n0elim ⊢ ¬ ∅ ∈ A → dom ⁡ E -1 ↾ A / E -1 ↾ A = A

Proof

Step Hyp Ref Expression
1 n0el2 ⊢ ¬ ∅ ∈ A ↔ dom ⁡ E -1 ↾ A = A
2 1 biimpi ⊢ ¬ ∅ ∈ A → dom ⁡ E -1 ↾ A = A
3 2 qseq1d ⊢ ¬ ∅ ∈ A → dom ⁡ E -1 ↾ A / E -1 ↾ A = A / E -1 ↾ A
4 qsresid ⊢ A / E -1 ↾ A = A / E -1
5 qsid ⊢ A / E -1 = A
6 4 5 eqtri ⊢ A / E -1 ↾ A = A
7 3 6 eqtrdi ⊢ ¬ ∅ ∈ A → dom ⁡ E -1 ↾ A / E -1 ↾ A = A