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

Metamath Proof Explorer

Theorem n0el2

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

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

Proof

Step Hyp Ref Expression
1 dmopab3 ⊢ ∀ x ∈ A ∃ y y ∈ x ↔ dom ⁡ x y | x ∈ A ∧ y ∈ x = A
2 n0el ⊢ ¬ ∅ ∈ A ↔ ∀ x ∈ A ∃ y y ∈ x
3 cnvepres ⊢ E -1 ↾ A = x y | x ∈ A ∧ y ∈ x
4 3 dmeqi ⊢ dom ⁡ E -1 ↾ A = dom ⁡ x y | x ∈ A ∧ y ∈ x
5 4 eqeq1i ⊢ dom ⁡ E -1 ↾ A = A ↔ dom ⁡ x y | x ∈ A ∧ y ∈ x = A
6 1 2 5 3bitr4i ⊢ ¬ ∅ ∈ A ↔ dom ⁡ E -1 ↾ A = A