Step |
Hyp |
Ref |
Expression |
1 |
|
xpeq2 |
|- ( B = (/) -> ( A X. B ) = ( A X. (/) ) ) |
2 |
|
xp0 |
|- ( A X. (/) ) = (/) |
3 |
1 2
|
eqtrdi |
|- ( B = (/) -> ( A X. B ) = (/) ) |
4 |
3
|
dmeqd |
|- ( B = (/) -> dom ( A X. B ) = dom (/) ) |
5 |
|
dm0 |
|- dom (/) = (/) |
6 |
4 5
|
eqtrdi |
|- ( B = (/) -> dom ( A X. B ) = (/) ) |
7 |
|
0ss |
|- (/) C_ A |
8 |
6 7
|
eqsstrdi |
|- ( B = (/) -> dom ( A X. B ) C_ A ) |
9 |
|
dmxp |
|- ( B =/= (/) -> dom ( A X. B ) = A ) |
10 |
|
eqimss |
|- ( dom ( A X. B ) = A -> dom ( A X. B ) C_ A ) |
11 |
9 10
|
syl |
|- ( B =/= (/) -> dom ( A X. B ) C_ A ) |
12 |
8 11
|
pm2.61ine |
|- dom ( A X. B ) C_ A |