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 =