Theorem 0el

Description: Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004)

	Ref	Expression
Assertion	0el	⊢ ( ∅ ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		risset	⊢ ( ∅ ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 = ∅ )
2		eq0	⊢ ( 𝑥 = ∅ ↔ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )
3	2	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 = ∅ ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )
4	1 3	bitri	⊢ ( ∅ ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )