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

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 ( ¬ ∅ ∈ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑢 𝑢 ∈ 𝑥 )

Proof

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