Step |
Hyp |
Ref |
Expression |
1 |
|
suppval |
|- ( ( X e. V /\ Z e. W ) -> ( X supp Z ) = { i e. dom X | ( X " { i } ) =/= { Z } } ) |
2 |
1
|
3adant1 |
|- ( ( Fun X /\ X e. V /\ Z e. W ) -> ( X supp Z ) = { i e. dom X | ( X " { i } ) =/= { Z } } ) |
3 |
|
funfn |
|- ( Fun X <-> X Fn dom X ) |
4 |
3
|
biimpi |
|- ( Fun X -> X Fn dom X ) |
5 |
4
|
3ad2ant1 |
|- ( ( Fun X /\ X e. V /\ Z e. W ) -> X Fn dom X ) |
6 |
|
fnsnfv |
|- ( ( X Fn dom X /\ i e. dom X ) -> { ( X ` i ) } = ( X " { i } ) ) |
7 |
5 6
|
sylan |
|- ( ( ( Fun X /\ X e. V /\ Z e. W ) /\ i e. dom X ) -> { ( X ` i ) } = ( X " { i } ) ) |
8 |
7
|
eqcomd |
|- ( ( ( Fun X /\ X e. V /\ Z e. W ) /\ i e. dom X ) -> ( X " { i } ) = { ( X ` i ) } ) |
9 |
8
|
neeq1d |
|- ( ( ( Fun X /\ X e. V /\ Z e. W ) /\ i e. dom X ) -> ( ( X " { i } ) =/= { Z } <-> { ( X ` i ) } =/= { Z } ) ) |
10 |
|
fvex |
|- ( X ` i ) e. _V |
11 |
|
sneqbg |
|- ( ( X ` i ) e. _V -> ( { ( X ` i ) } = { Z } <-> ( X ` i ) = Z ) ) |
12 |
10 11
|
mp1i |
|- ( ( ( Fun X /\ X e. V /\ Z e. W ) /\ i e. dom X ) -> ( { ( X ` i ) } = { Z } <-> ( X ` i ) = Z ) ) |
13 |
12
|
necon3bid |
|- ( ( ( Fun X /\ X e. V /\ Z e. W ) /\ i e. dom X ) -> ( { ( X ` i ) } =/= { Z } <-> ( X ` i ) =/= Z ) ) |
14 |
9 13
|
bitrd |
|- ( ( ( Fun X /\ X e. V /\ Z e. W ) /\ i e. dom X ) -> ( ( X " { i } ) =/= { Z } <-> ( X ` i ) =/= Z ) ) |
15 |
14
|
rabbidva |
|- ( ( Fun X /\ X e. V /\ Z e. W ) -> { i e. dom X | ( X " { i } ) =/= { Z } } = { i e. dom X | ( X ` i ) =/= Z } ) |
16 |
2 15
|
eqtrd |
|- ( ( Fun X /\ X e. V /\ Z e. W ) -> ( X supp Z ) = { i e. dom X | ( X ` i ) =/= Z } ) |