Step |
Hyp |
Ref |
Expression |
1 |
|
compss.a |
|- F = ( x e. ~P A |-> ( A \ x ) ) |
2 |
|
difeq2 |
|- ( x = a -> ( A \ x ) = ( A \ a ) ) |
3 |
2
|
cbvmptv |
|- ( x e. ~P A |-> ( A \ x ) ) = ( a e. ~P A |-> ( A \ a ) ) |
4 |
1 3
|
eqtri |
|- F = ( a e. ~P A |-> ( A \ a ) ) |
5 |
|
difeq2 |
|- ( a = X -> ( A \ a ) = ( A \ X ) ) |
6 |
|
elpw2g |
|- ( A e. V -> ( X e. ~P A <-> X C_ A ) ) |
7 |
6
|
biimpar |
|- ( ( A e. V /\ X C_ A ) -> X e. ~P A ) |
8 |
|
difexg |
|- ( A e. V -> ( A \ X ) e. _V ) |
9 |
8
|
adantr |
|- ( ( A e. V /\ X C_ A ) -> ( A \ X ) e. _V ) |
10 |
4 5 7 9
|
fvmptd3 |
|- ( ( A e. V /\ X C_ A ) -> ( F ` X ) = ( A \ X ) ) |