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 |) ) ) |