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

Metamath Proof Explorer

Theorem n0el3

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

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

Proof

Step Hyp Ref Expression
1 n0elim ⊢ ¬ ∅ ∈ A → dom ⁡ E -1 ↾ A / E -1 ↾ A = A
2 n0eldmqseq ⊢ dom ⁡ E -1 ↾ A / E -1 ↾ A = A → ¬ ∅ ∈ A
3 1 2 impbii ⊢ ¬ ∅ ∈ A ↔ dom ⁡ E -1 ↾ A / E -1 ↾ A = A