Metamath Proof Explorer


Theorem bj-tagci

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-tagci A B A tag B

Proof

Step Hyp Ref Expression
1 bj-snglc A B A sngl B
2 bj-sngltagi A sngl B A tag B
3 1 2 sylbi A B A tag B