Step |
Hyp |
Ref |
Expression |
1 |
|
iunxdif3.1 |
|- F/_ x E |
2 |
|
inss2 |
|- ( A i^i E ) C_ E |
3 |
|
nfcv |
|- F/_ x A |
4 |
3 1
|
nfin |
|- F/_ x ( A i^i E ) |
5 |
4 1
|
ssrexf |
|- ( ( A i^i E ) C_ E -> ( E. x e. ( A i^i E ) y e. B -> E. x e. E y e. B ) ) |
6 |
|
eliun |
|- ( y e. U_ x e. ( A i^i E ) B <-> E. x e. ( A i^i E ) y e. B ) |
7 |
|
eliun |
|- ( y e. U_ x e. E B <-> E. x e. E y e. B ) |
8 |
5 6 7
|
3imtr4g |
|- ( ( A i^i E ) C_ E -> ( y e. U_ x e. ( A i^i E ) B -> y e. U_ x e. E B ) ) |
9 |
8
|
ssrdv |
|- ( ( A i^i E ) C_ E -> U_ x e. ( A i^i E ) B C_ U_ x e. E B ) |
10 |
2 9
|
ax-mp |
|- U_ x e. ( A i^i E ) B C_ U_ x e. E B |
11 |
|
iuneq2 |
|- ( A. x e. E B = (/) -> U_ x e. E B = U_ x e. E (/) ) |
12 |
|
iun0 |
|- U_ x e. E (/) = (/) |
13 |
11 12
|
eqtrdi |
|- ( A. x e. E B = (/) -> U_ x e. E B = (/) ) |
14 |
10 13
|
sseqtrid |
|- ( A. x e. E B = (/) -> U_ x e. ( A i^i E ) B C_ (/) ) |
15 |
|
ss0 |
|- ( U_ x e. ( A i^i E ) B C_ (/) -> U_ x e. ( A i^i E ) B = (/) ) |
16 |
14 15
|
syl |
|- ( A. x e. E B = (/) -> U_ x e. ( A i^i E ) B = (/) ) |
17 |
16
|
uneq1d |
|- ( A. x e. E B = (/) -> ( U_ x e. ( A i^i E ) B u. U_ x e. ( A \ E ) B ) = ( (/) u. U_ x e. ( A \ E ) B ) ) |
18 |
|
iunxun |
|- U_ x e. ( ( A i^i E ) u. ( A \ E ) ) B = ( U_ x e. ( A i^i E ) B u. U_ x e. ( A \ E ) B ) |
19 |
|
inundif |
|- ( ( A i^i E ) u. ( A \ E ) ) = A |
20 |
19
|
nfth |
|- F/ x ( ( A i^i E ) u. ( A \ E ) ) = A |
21 |
3 1
|
nfdif |
|- F/_ x ( A \ E ) |
22 |
4 21
|
nfun |
|- F/_ x ( ( A i^i E ) u. ( A \ E ) ) |
23 |
|
id |
|- ( ( ( A i^i E ) u. ( A \ E ) ) = A -> ( ( A i^i E ) u. ( A \ E ) ) = A ) |
24 |
|
eqidd |
|- ( ( ( A i^i E ) u. ( A \ E ) ) = A -> B = B ) |
25 |
20 22 3 23 24
|
iuneq12df |
|- ( ( ( A i^i E ) u. ( A \ E ) ) = A -> U_ x e. ( ( A i^i E ) u. ( A \ E ) ) B = U_ x e. A B ) |
26 |
19 25
|
ax-mp |
|- U_ x e. ( ( A i^i E ) u. ( A \ E ) ) B = U_ x e. A B |
27 |
18 26
|
eqtr3i |
|- ( U_ x e. ( A i^i E ) B u. U_ x e. ( A \ E ) B ) = U_ x e. A B |
28 |
27
|
a1i |
|- ( A. x e. E B = (/) -> ( U_ x e. ( A i^i E ) B u. U_ x e. ( A \ E ) B ) = U_ x e. A B ) |
29 |
|
uncom |
|- ( (/) u. U_ x e. ( A \ E ) B ) = ( U_ x e. ( A \ E ) B u. (/) ) |
30 |
|
un0 |
|- ( U_ x e. ( A \ E ) B u. (/) ) = U_ x e. ( A \ E ) B |
31 |
29 30
|
eqtri |
|- ( (/) u. U_ x e. ( A \ E ) B ) = U_ x e. ( A \ E ) B |
32 |
31
|
a1i |
|- ( A. x e. E B = (/) -> ( (/) u. U_ x e. ( A \ E ) B ) = U_ x e. ( A \ E ) B ) |
33 |
17 28 32
|
3eqtr3rd |
|- ( A. x e. E B = (/) -> U_ x e. ( A \ E ) B = U_ x e. A B ) |