Theorem bj-2upleq

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

	Ref	Expression
Assertion	bj-2upleq	$$⊢A=B\to \left(C=D\to ⦅A,C⦆=⦅B,D⦆\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-1upleq	$$⊢A=B\to ⦅A⦆=⦅B⦆$$
2		bj-xtageq	$$⊢C=D\to \left\{1_{𝑜}\right\}\times tagC=\left\{1_{𝑜}\right\}\times tagD$$
3		uneq12	$$⊢\left(⦅A⦆=⦅B⦆\wedge \left\{1_{𝑜}\right\}\times tagC=\left\{1_{𝑜}\right\}\times tagD\right)\to ⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagC\right)=⦅B⦆\cup \left(\left\{1_{𝑜}\right\}\times tagD\right)$$
4	3	ex	$$⊢⦅A⦆=⦅B⦆\to \left(\left\{1_{𝑜}\right\}\times tagC=\left\{1_{𝑜}\right\}\times tagD\to ⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagC\right)=⦅B⦆\cup \left(\left\{1_{𝑜}\right\}\times tagD\right)\right)$$
5	1 2 4	syl2im	$$⊢A=B\to \left(C=D\to ⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagC\right)=⦅B⦆\cup \left(\left\{1_{𝑜}\right\}\times tagD\right)\right)$$
6		df-bj-2upl	$$⊢⦅A,C⦆=⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagC\right)$$
7		df-bj-2upl	$$⊢⦅B,D⦆=⦅B⦆\cup \left(\left\{1_{𝑜}\right\}\times tagD\right)$$
8	6 7	eqeq12i	$$⊢⦅A,C⦆=⦅B,D⦆\leftrightarrow ⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagC\right)=⦅B⦆\cup \left(\left\{1_{𝑜}\right\}\times tagD\right)$$
9	5 8	syl6ibr	$$⊢A=B\to \left(C=D\to ⦅A,C⦆=⦅B,D⦆\right)$$