Metamath Proof Explorer


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 syl6ibr
 |-  ( A = B -> ( C = D -> (| A ,, C |) = (| B ,, D |) ) )