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 ) ) |
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 ) ) |