Metamath Proof Explorer

Theorem bj-0eltag

Description: The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019)

Ref Expression
Assertion bj-0eltag ⊢ ∅ ∈ tag A

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 1 snid ⊢ ∅ ∈ ∅
3 2 olci ⊢ ∅ ∈ sngl A ∨ ∅ ∈ ∅
4 elun ⊢ ∅ ∈ sngl A ∪ ∅ ↔ ∅ ∈ sngl A ∨ ∅ ∈ ∅
5 3 4 mpbir ⊢ ∅ ∈ sngl A ∪ ∅
6 df-bj-tag ⊢ tag A = sngl A ∪ ∅
7 5 6 eleqtrri ⊢ ∅ ∈ tag A