Step |
Hyp |
Ref |
Expression |
1 |
|
nfcv |
|- F/_ k A |
2 |
|
nfiu1 |
|- F/_ k U_ k e. A B |
3 |
1 2
|
nfxp |
|- F/_ k ( A X. U_ k e. A B ) |
4 |
3
|
iunssf |
|- ( U_ k e. A ( { k } X. B ) C_ ( A X. U_ k e. A B ) <-> A. k e. A ( { k } X. B ) C_ ( A X. U_ k e. A B ) ) |
5 |
|
snssi |
|- ( k e. A -> { k } C_ A ) |
6 |
|
ssiun2 |
|- ( k e. A -> B C_ U_ k e. A B ) |
7 |
|
xpss12 |
|- ( ( { k } C_ A /\ B C_ U_ k e. A B ) -> ( { k } X. B ) C_ ( A X. U_ k e. A B ) ) |
8 |
5 6 7
|
syl2anc |
|- ( k e. A -> ( { k } X. B ) C_ ( A X. U_ k e. A B ) ) |
9 |
4 8
|
mprgbir |
|- U_ k e. A ( { k } X. B ) C_ ( A X. U_ k e. A B ) |