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