Metamath Proof Explorer


Theorem bj-taginv

Description: Inverse of tagging. (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-taginv A=x|xtagA

Proof

Step Hyp Ref Expression
1 bj-snglinv A=x|xsnglA
2 bj-sngltag xVxsnglAxtagA
3 2 elv xsnglAxtagA
4 3 abbii x|xsnglA=x|xtagA
5 1 4 eqtri A=x|xtagA