Metamath Proof Explorer

Theorem bj-sngltag

Description: The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-sngltag ⊢ A ∈ V → A ∈ sngl B ↔ A ∈ tag B

Proof

Step Hyp Ref Expression
1 bj-sngltagi ⊢ A ∈ sngl B → A ∈ tag B
2 df-bj-tag ⊢ tag B = sngl B ∪ ∅
3 2 eleq2i ⊢ A ∈ tag B ↔ A ∈ sngl B ∪ ∅
4 elun ⊢ A ∈ sngl B ∪ ∅ ↔ A ∈ sngl B ∨ A ∈ ∅
5 idd ⊢ A ∈ V → A ∈ sngl B → A ∈ sngl B
6 elsni ⊢ A ∈ ∅ → A = ∅
7 snprc ⊢ ¬ A ∈ V ↔ A = ∅
8 elex ⊢ A ∈ V → A ∈ V
9 8 pm2.24d ⊢ A ∈ V → ¬ A ∈ V → A ∈ sngl B
10 7 9 biimtrrid ⊢ A ∈ V → A = ∅ → A ∈ sngl B
11 6 10 syl5 ⊢ A ∈ V → A ∈ ∅ → A ∈ sngl B
12 5 11 jaod ⊢ A ∈ V → A ∈ sngl B ∨ A ∈ ∅ → A ∈ sngl B
13 4 12 biimtrid ⊢ A ∈ V → A ∈ sngl B ∪ ∅ → A ∈ sngl B
14 3 13 biimtrid ⊢ A ∈ V → A ∈ tag B → A ∈ sngl B
15 1 14 impbid2 ⊢ A ∈ V → A ∈ sngl B ↔ A ∈ tag B