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 e. V -> ( A e. B <-> { A } e. tag B ) )

Proof

Step Hyp Ref Expression
1 bj-snglc
 |-  ( A e. B <-> { A } e. sngl B )
2 bj-sngltag
 |-  ( A e. V -> ( { A } e. sngl B <-> { A } e. tag B ) )
3 1 2 syl5bb
 |-  ( A e. V -> ( A e. B <-> { A } e. tag B ) )