Metamath Proof Explorer

Theorem n0el

Description: Negated membership of the empty set in another class. (Contributed by Rodolfo Medina, 25-Sep-2010)

Ref Expression
Assertion n0el ⊢ ¬ ∅ ∈ A ↔ ∀ x ∈ A ∃ u u ∈ x

Proof

Step Hyp Ref Expression
1 df-ral ⊢ ∀ x ∈ A ¬ ∀ u ¬ u ∈ x ↔ ∀ x x ∈ A → ¬ ∀ u ¬ u ∈ x
2 df-ex ⊢ ∃ u u ∈ x ↔ ¬ ∀ u ¬ u ∈ x
3 2 ralbii ⊢ ∀ x ∈ A ∃ u u ∈ x ↔ ∀ x ∈ A ¬ ∀ u ¬ u ∈ x
4 alnex ⊢ ∀ x ¬ x ∈ A ∧ ∀ u ¬ u ∈ x ↔ ¬ ∃ x x ∈ A ∧ ∀ u ¬ u ∈ x
5 imnang ⊢ ∀ x x ∈ A → ¬ ∀ u ¬ u ∈ x ↔ ∀ x ¬ x ∈ A ∧ ∀ u ¬ u ∈ x
6 0el ⊢ ∅ ∈ A ↔ ∃ x ∈ A ∀ u ¬ u ∈ x
7 df-rex ⊢ ∃ x ∈ A ∀ u ¬ u ∈ x ↔ ∃ x x ∈ A ∧ ∀ u ¬ u ∈ x
8 6 7 bitri ⊢ ∅ ∈ A ↔ ∃ x x ∈ A ∧ ∀ u ¬ u ∈ x
9 8 notbii ⊢ ¬ ∅ ∈ A ↔ ¬ ∃ x x ∈ A ∧ ∀ u ¬ u ∈ x
10 4 5 9 3bitr4ri ⊢ ¬ ∅ ∈ A ↔ ∀ x x ∈ A → ¬ ∀ u ¬ u ∈ x
11 1 3 10 3bitr4ri ⊢ ¬ ∅ ∈ A ↔ ∀ x ∈ A ∃ u u ∈ x