Metamath Proof Explorer


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 𝐵 ↔ ( ∃ 𝑥𝐵 𝐴 = { 𝑥 } ∨ 𝐴 = ∅ ) )