Theorem bj-tageq

Description: Substitution property for tag . (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-tageq	|- ( A = B -> tag A = tag B )

Proof

Step	Hyp	Ref	Expression
1		bj-sngleq	|- ( A = B -> sngl A = sngl B )
2	1	uneq1d	|- ( A = B -> ( sngl A u. { (/) } ) = ( sngl B u. { (/) } ) )
3		df-bj-tag	|- tag A = ( sngl A u. { (/) } )
4		df-bj-tag	|- tag B = ( sngl B u. { (/) } )
5	2 3 4	3eqtr4g	|- ( A = B -> tag A = tag B )