Step |
Hyp |
Ref |
Expression |
1 |
|
0ex |
|- (/) e. _V |
2 |
|
suppval |
|- ( ( (/) e. _V /\ Z e. W ) -> ( (/) supp Z ) = { i e. dom (/) | ( (/) " { i } ) =/= { Z } } ) |
3 |
1 2
|
mpan |
|- ( Z e. W -> ( (/) supp Z ) = { i e. dom (/) | ( (/) " { i } ) =/= { Z } } ) |
4 |
|
dm0 |
|- dom (/) = (/) |
5 |
|
rabeq |
|- ( dom (/) = (/) -> { i e. dom (/) | ( (/) " { i } ) =/= { Z } } = { i e. (/) | ( (/) " { i } ) =/= { Z } } ) |
6 |
4 5
|
mp1i |
|- ( Z e. W -> { i e. dom (/) | ( (/) " { i } ) =/= { Z } } = { i e. (/) | ( (/) " { i } ) =/= { Z } } ) |
7 |
|
rab0 |
|- { i e. (/) | ( (/) " { i } ) =/= { Z } } = (/) |
8 |
7
|
a1i |
|- ( Z e. W -> { i e. (/) | ( (/) " { i } ) =/= { Z } } = (/) ) |
9 |
3 6 8
|
3eqtrd |
|- ( Z e. W -> ( (/) supp Z ) = (/) ) |