Step |
Hyp |
Ref |
Expression |
1 |
|
mptsuppdifd.f |
|- F = ( x e. A |-> B ) |
2 |
|
mptsuppdifd.a |
|- ( ph -> A e. V ) |
3 |
|
mptsuppdifd.z |
|- ( ph -> Z e. W ) |
4 |
|
mptsuppd.b |
|- ( ( ph /\ x e. A ) -> B e. U ) |
5 |
1 2 3
|
mptsuppdifd |
|- ( ph -> ( F supp Z ) = { x e. A | B e. ( _V \ { Z } ) } ) |
6 |
|
eldifsn |
|- ( B e. ( _V \ { Z } ) <-> ( B e. _V /\ B =/= Z ) ) |
7 |
4
|
elexd |
|- ( ( ph /\ x e. A ) -> B e. _V ) |
8 |
7
|
biantrurd |
|- ( ( ph /\ x e. A ) -> ( B =/= Z <-> ( B e. _V /\ B =/= Z ) ) ) |
9 |
6 8
|
bitr4id |
|- ( ( ph /\ x e. A ) -> ( B e. ( _V \ { Z } ) <-> B =/= Z ) ) |
10 |
9
|
rabbidva |
|- ( ph -> { x e. A | B e. ( _V \ { Z } ) } = { x e. A | B =/= Z } ) |
11 |
5 10
|
eqtrd |
|- ( ph -> ( F supp Z ) = { x e. A | B =/= Z } ) |