Step |
Hyp |
Ref |
Expression |
1 |
|
ixpf |
|- ( f e. X_ x e. A B -> f : A --> U_ x e. A B ) |
2 |
|
fssxp |
|- ( f : A --> U_ x e. A B -> f C_ ( A X. U_ x e. A B ) ) |
3 |
1 2
|
syl |
|- ( f e. X_ x e. A B -> f C_ ( A X. U_ x e. A B ) ) |
4 |
|
velpw |
|- ( f e. ~P ( A X. U_ x e. A B ) <-> f C_ ( A X. U_ x e. A B ) ) |
5 |
3 4
|
sylibr |
|- ( f e. X_ x e. A B -> f e. ~P ( A X. U_ x e. A B ) ) |
6 |
5
|
ssriv |
|- X_ x e. A B C_ ~P ( A X. U_ x e. A B ) |
7 |
|
sspwuni |
|- ( X_ x e. A B C_ ~P ( A X. U_ x e. A B ) <-> U. X_ x e. A B C_ ( A X. U_ x e. A B ) ) |
8 |
6 7
|
mpbi |
|- U. X_ x e. A B C_ ( A X. U_ x e. A B ) |