Theorem dfnul3

Description: Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004) (Proof shortened by BJ, 23-Sep-2024)

	Ref	Expression
Assertion	dfnul3	⊢ ∅ = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		fal	⊢ ¬ ⊥
2		pm3.24	⊢ ¬ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐴 )
3	1 2	2false	⊢ ( ⊥ ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐴 ) )
4	3	abbii	⊢ { 𝑥 ∣ ⊥ } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐴 ) }
5		dfnul4	⊢ ∅ = { 𝑥 ∣ ⊥ }
6		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐴 ) }
7	4 5 6	3eqtr4i	⊢ ∅ = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴 }