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 𝐴

Proof

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