Description: Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-eltag |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-bj-tag | ||
2 | 1 | eleq2i | |
3 | elun | ||
4 | bj-elsngl | ||
5 | 0ex | ||
6 | 5 | elsn2 | |
7 | 4 6 | orbi12i | |
8 | 2 3 7 | 3bitri |