Theorem bj-eltag

Description: Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-eltag	⊢ ( 𝐴 ∈ tag 𝐵 ↔ ( ∃ 𝑥 ∈ 𝐵 𝐴 = { 𝑥 } ∨ 𝐴 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		df-bj-tag	⊢ tag 𝐵 = ( sngl 𝐵 ∪ { ∅ } )
2	1	eleq2i	⊢ ( 𝐴 ∈ tag 𝐵 ↔ 𝐴 ∈ ( sngl 𝐵 ∪ { ∅ } ) )
3		elun	⊢ ( 𝐴 ∈ ( sngl 𝐵 ∪ { ∅ } ) ↔ ( 𝐴 ∈ sngl 𝐵 ∨ 𝐴 ∈ { ∅ } ) )
4		bj-elsngl	⊢ ( 𝐴 ∈ sngl 𝐵 ↔ ∃ 𝑥 ∈ 𝐵 𝐴 = { 𝑥 } )
5		0ex	⊢ ∅ ∈ V
6	5	elsn2	⊢ ( 𝐴 ∈ { ∅ } ↔ 𝐴 = ∅ )
7	4 6	orbi12i	⊢ ( ( 𝐴 ∈ sngl 𝐵 ∨ 𝐴 ∈ { ∅ } ) ↔ ( ∃ 𝑥 ∈ 𝐵 𝐴 = { 𝑥 } ∨ 𝐴 = ∅ ) )
8	2 3 7	3bitri	⊢ ( 𝐴 ∈ tag 𝐵 ↔ ( ∃ 𝑥 ∈ 𝐵 𝐴 = { 𝑥 } ∨ 𝐴 = ∅ ) )