Theorem dfnul3

Description: Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004)

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

Proof

Step	Hyp	Ref	Expression
1		pm3.24	⊢ ¬ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐴 )
2		equid	⊢ 𝑥 = 𝑥
3	1 2	2th	⊢ ( ¬ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐴 ) ↔ 𝑥 = 𝑥 )
4	3	con1bii	⊢ ( ¬ 𝑥 = 𝑥 ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐴 ) )
5	4	abbii	⊢ { 𝑥 ∣ ¬ 𝑥 = 𝑥 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐴 ) }
6		dfnul2	⊢ ∅ = { 𝑥 ∣ ¬ 𝑥 = 𝑥 }
7		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐴 ) }
8	5 6 7	3eqtr4i	⊢ ∅ = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴 }