Step |
Hyp |
Ref |
Expression |
1 |
|
df-wunc |
|- wUniCl = ( x e. _V |-> |^| { u e. WUni | x C_ u } ) |
2 |
|
sseq1 |
|- ( x = A -> ( x C_ u <-> A C_ u ) ) |
3 |
2
|
rabbidv |
|- ( x = A -> { u e. WUni | x C_ u } = { u e. WUni | A C_ u } ) |
4 |
3
|
inteqd |
|- ( x = A -> |^| { u e. WUni | x C_ u } = |^| { u e. WUni | A C_ u } ) |
5 |
|
elex |
|- ( A e. V -> A e. _V ) |
6 |
|
wunex |
|- ( A e. V -> E. u e. WUni A C_ u ) |
7 |
|
rabn0 |
|- ( { u e. WUni | A C_ u } =/= (/) <-> E. u e. WUni A C_ u ) |
8 |
6 7
|
sylibr |
|- ( A e. V -> { u e. WUni | A C_ u } =/= (/) ) |
9 |
|
intex |
|- ( { u e. WUni | A C_ u } =/= (/) <-> |^| { u e. WUni | A C_ u } e. _V ) |
10 |
8 9
|
sylib |
|- ( A e. V -> |^| { u e. WUni | A C_ u } e. _V ) |
11 |
1 4 5 10
|
fvmptd3 |
|- ( A e. V -> ( wUniCl ` A ) = |^| { u e. WUni | A C_ u } ) |