Theorem ralfal

Description: Two ways of expressing empty set. (Contributed by Glauco Siliprandi, 24-Jan-2024)

	Ref	Expression
Hypothesis	ralfal.1	⊢ Ⅎ 𝑥 𝐴
Assertion	ralfal	⊢ ( 𝐴 = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ⊥ )

Proof

Step	Hyp	Ref	Expression
1		ralfal.1	⊢ Ⅎ 𝑥 𝐴
2		df-fal	⊢ ( ⊥ ↔ ¬ ⊤ )
3	2	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ⊥ ↔ ∀ 𝑥 ∈ 𝐴 ¬ ⊤ )
4		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ⊤ ↔ ¬ ∃ 𝑥 ∈ 𝐴 ⊤ )
5	3 4	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ⊥ ↔ ¬ ∃ 𝑥 ∈ 𝐴 ⊤ )
6		rextru	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ⊤ )
7	6	notbii	⊢ ( ¬ ∃ 𝑥 𝑥 ∈ 𝐴 ↔ ¬ ∃ 𝑥 ∈ 𝐴 ⊤ )
8	1	neq0f	⊢ ( ¬ 𝐴 = ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
9	8	con1bii	⊢ ( ¬ ∃ 𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 = ∅ )
10	5 7 9	3bitr2ri	⊢ ( 𝐴 = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ⊥ )