Theorem bj-tageq

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

	Ref	Expression
Assertion	bj-tageq	⊢ ( 𝐴 = 𝐵 → tag 𝐴 = tag 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		bj-sngleq	⊢ ( 𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵 )
2	1	uneq1d	⊢ ( 𝐴 = 𝐵 → ( sngl 𝐴 ∪ { ∅ } ) = ( sngl 𝐵 ∪ { ∅ } ) )
3		df-bj-tag	⊢ tag 𝐴 = ( sngl 𝐴 ∪ { ∅ } )
4		df-bj-tag	⊢ tag 𝐵 = ( sngl 𝐵 ∪ { ∅ } )
5	2 3 4	3eqtr4g	⊢ ( 𝐴 = 𝐵 → tag 𝐴 = tag 𝐵 )