Theorem bj-tagss

Description: The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-tagss	|- tag A C_ ~P A

Proof

Step	Hyp	Ref	Expression
1		df-bj-tag	|- tag A = ( sngl A u. { (/) } )
2		bj-snglss	|- sngl A C_ ~P A
3		0elpw	|- (/) e. ~P A
4		0ex	|- (/) e. _V
5	4	snss	|- ( (/) e. ~P A <-> { (/) } C_ ~P A )
6	3 5	mpbi	|- { (/) } C_ ~P A
7	2 6	unssi	|- ( sngl A u. { (/) } ) C_ ~P A
8	1 7	eqsstri	|- tag A C_ ~P A