Metamath Proof Explorer


Theorem bj-tagcg

Description: Characterization of the elements of B in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-tagcg A V A B A tag B

Proof

Step Hyp Ref Expression
1 bj-snglc A B A sngl B
2 bj-sngltag A V A sngl B A tag B
3 1 2 syl5bb A V A B A tag B