Theorem bj-tageq

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

	Ref	Expression
Assertion	bj-tageq	$$⊢A=B\to tagA=tagB$$

Proof

Step	Hyp	Ref	Expression
1		bj-sngleq	$$⊢A=B\to snglA=snglB$$
2	1	uneq1d	$$⊢A=B\to snglA\cup \left\{\varnothing \right\}=snglB\cup \left\{\varnothing \right\}$$
3		df-bj-tag	$$⊢tagA=snglA\cup \left\{\varnothing \right\}$$
4		df-bj-tag	$$⊢tagB=snglB\cup \left\{\varnothing \right\}$$
5	2 3 4	3eqtr4g	$$⊢A=B\to tagA=tagB$$