Theorem bj-2upleq

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

	Ref	Expression
Assertion	bj-2upleq	|- ( A = B -> ( C = D -> (| A ,, C |) = (| B ,, D |) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-1upleq	|- ( A = B -> (| A |) = (| B |) )
2		bj-xtageq	|- ( C = D -> ( { 1o } X. tag C ) = ( { 1o } X. tag D ) )
3		uneq12	|- ( ( (| A |) = (| B |) /\ ( { 1o } X. tag C ) = ( { 1o } X. tag D ) ) -> ( (| A |) u. ( { 1o } X. tag C ) ) = ( (| B |) u. ( { 1o } X. tag D ) ) )
4	3	ex	|- ( (| A |) = (| B |) -> ( ( { 1o } X. tag C ) = ( { 1o } X. tag D ) -> ( (| A |) u. ( { 1o } X. tag C ) ) = ( (| B |) u. ( { 1o } X. tag D ) ) ) )
5	1 2 4	syl2im	|- ( A = B -> ( C = D -> ( (| A |) u. ( { 1o } X. tag C ) ) = ( (| B |) u. ( { 1o } X. tag D ) ) ) )
6		df-bj-2upl	|- (| A ,, C |) = ( (| A |) u. ( { 1o } X. tag C ) )
7		df-bj-2upl	|- (| B ,, D |) = ( (| B |) u. ( { 1o } X. tag D ) )
8	6 7	eqeq12i	|- ( (| A ,, C |) = (| B ,, D |) <-> ( (| A |) u. ( { 1o } X. tag C ) ) = ( (| B |) u. ( { 1o } X. tag D ) ) )
9	5 8	imbitrrdi	|- ( A = B -> ( C = D -> (| A ,, C |) = (| B ,, D |) ) )