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 syl5bir 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 syl5bi A V A sngl B A sngl B
14 3 13 syl5bi A V A tag B A sngl B
15 1 14 impbid2 A V A sngl B A tag B