Description: Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-eltag | ⊢ ( 𝐴 ∈ tag 𝐵 ↔ ( ∃ 𝑥 ∈ 𝐵 𝐴 = { 𝑥 } ∨ 𝐴 = ∅ ) ) |
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 𝐵 ↔ ( ∃ 𝑥 ∈ 𝐵 𝐴 = { 𝑥 } ∨ 𝐴 = ∅ ) ) |