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 ⊢ A ∈ tag B ↔ ∃ x ∈ B A = x ∨ A = ∅

Proof

Step Hyp Ref Expression
1 df-bj-tag ⊢ tag B = sngl B ∪ ∅
2 1 eleq2i ⊢ A ∈ tag B ↔ A ∈ sngl B ∪ ∅
3 elun ⊢ A ∈ sngl B ∪ ∅ ↔ A ∈ sngl B ∨ A ∈ ∅
4 bj-elsngl ⊢ A ∈ sngl B ↔ ∃ x ∈ B A = x
5 0ex ⊢ ∅ ∈ V
6 5 elsn2 ⊢ A ∈ ∅ ↔ A = ∅
7 4 6 orbi12i ⊢ A ∈ sngl B ∨ A ∈ ∅ ↔ ∃ x ∈ B A = x ∨ A = ∅
8 2 3 7 3bitri ⊢ A ∈ tag B ↔ ∃ x ∈ B A = x ∨ A = ∅