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