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

Proof

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