Metamath Proof Explorer

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 ⊢ ∅ = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴 }