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

Metamath Proof Explorer

Theorem ab0

Description: The class of sets verifying a property is the empty class if and only if that property is a contradiction. See also abn0 (from which it could be proved using as many essential proof steps but one fewer syntactic step, at the cost of depending on df-ne ). (Contributed by BJ, 19-Mar-2021) Avoid df-clel , ax-8 . (Revised by GG, 30-Aug-2024) (Proof shortened by SN, 8-Sep-2024)

		Ref	Expression
	Assertion	ab0	⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ ∀ 𝑥 ¬ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		abbib	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊥ } ↔ ∀ 𝑥 ( 𝜑 ↔ ⊥ ) )
2		dfnul4	⊢ ∅ = { 𝑥 ∣ ⊥ }
3	2	eqeq2i	⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊥ } )
4		nbfal	⊢ ( ¬ 𝜑 ↔ ( 𝜑 ↔ ⊥ ) )
5	4	albii	⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ∀ 𝑥 ( 𝜑 ↔ ⊥ ) )
6	1 3 5	3bitr4i	⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ ∀ 𝑥 ¬ 𝜑 )