Step |
Hyp |
Ref |
Expression |
1 |
|
ustbasel |
|- ( U e. ( UnifOn ` X ) -> ( X X. X ) e. U ) |
2 |
|
ustssxp |
|- ( ( U e. ( UnifOn ` X ) /\ u e. U ) -> u C_ ( X X. X ) ) |
3 |
2
|
ralrimiva |
|- ( U e. ( UnifOn ` X ) -> A. u e. U u C_ ( X X. X ) ) |
4 |
|
pwssb |
|- ( U C_ ~P ( X X. X ) <-> A. u e. U u C_ ( X X. X ) ) |
5 |
3 4
|
sylibr |
|- ( U e. ( UnifOn ` X ) -> U C_ ~P ( X X. X ) ) |
6 |
|
elpwuni |
|- ( ( X X. X ) e. U -> ( U C_ ~P ( X X. X ) <-> U. U = ( X X. X ) ) ) |
7 |
6
|
biimpa |
|- ( ( ( X X. X ) e. U /\ U C_ ~P ( X X. X ) ) -> U. U = ( X X. X ) ) |
8 |
1 5 7
|
syl2anc |
|- ( U e. ( UnifOn ` X ) -> U. U = ( X X. X ) ) |