Step |
Hyp |
Ref |
Expression |
1 |
|
fvssunirn |
|- ( f ` x ) C_ U. ran f |
2 |
|
simpr |
|- ( ( x e. A /\ B e. ( f ` x ) ) -> B e. ( f ` x ) ) |
3 |
1 2
|
sselid |
|- ( ( x e. A /\ B e. ( f ` x ) ) -> B e. U. ran f ) |
4 |
3
|
ralimiaa |
|- ( A. x e. A B e. ( f ` x ) -> A. x e. A B e. U. ran f ) |
5 |
|
eqid |
|- ( x e. A |-> B ) = ( x e. A |-> B ) |
6 |
5
|
fmpt |
|- ( A. x e. A B e. U. ran f <-> ( x e. A |-> B ) : A --> U. ran f ) |
7 |
4 6
|
sylib |
|- ( A. x e. A B e. ( f ` x ) -> ( x e. A |-> B ) : A --> U. ran f ) |
8 |
|
id |
|- ( A e. V -> A e. V ) |
9 |
|
vex |
|- f e. _V |
10 |
9
|
rnex |
|- ran f e. _V |
11 |
10
|
uniex |
|- U. ran f e. _V |
12 |
|
fex2 |
|- ( ( ( x e. A |-> B ) : A --> U. ran f /\ A e. V /\ U. ran f e. _V ) -> ( x e. A |-> B ) e. _V ) |
13 |
11 12
|
mp3an3 |
|- ( ( ( x e. A |-> B ) : A --> U. ran f /\ A e. V ) -> ( x e. A |-> B ) e. _V ) |
14 |
7 8 13
|
syl2anr |
|- ( ( A e. V /\ A. x e. A B e. ( f ` x ) ) -> ( x e. A |-> B ) e. _V ) |
15 |
5
|
fvmpt2 |
|- ( ( x e. A /\ B e. ( f ` x ) ) -> ( ( x e. A |-> B ) ` x ) = B ) |
16 |
15 2
|
eqeltrd |
|- ( ( x e. A /\ B e. ( f ` x ) ) -> ( ( x e. A |-> B ) ` x ) e. ( f ` x ) ) |
17 |
16
|
ralimiaa |
|- ( A. x e. A B e. ( f ` x ) -> A. x e. A ( ( x e. A |-> B ) ` x ) e. ( f ` x ) ) |
18 |
17
|
adantl |
|- ( ( A e. V /\ A. x e. A B e. ( f ` x ) ) -> A. x e. A ( ( x e. A |-> B ) ` x ) e. ( f ` x ) ) |
19 |
|
nfmpt1 |
|- F/_ x ( x e. A |-> B ) |
20 |
19
|
nfeq2 |
|- F/ x g = ( x e. A |-> B ) |
21 |
|
fveq1 |
|- ( g = ( x e. A |-> B ) -> ( g ` x ) = ( ( x e. A |-> B ) ` x ) ) |
22 |
21
|
eleq1d |
|- ( g = ( x e. A |-> B ) -> ( ( g ` x ) e. ( f ` x ) <-> ( ( x e. A |-> B ) ` x ) e. ( f ` x ) ) ) |
23 |
20 22
|
ralbid |
|- ( g = ( x e. A |-> B ) -> ( A. x e. A ( g ` x ) e. ( f ` x ) <-> A. x e. A ( ( x e. A |-> B ) ` x ) e. ( f ` x ) ) ) |
24 |
14 18 23
|
spcedv |
|- ( ( A e. V /\ A. x e. A B e. ( f ` x ) ) -> E. g A. x e. A ( g ` x ) e. ( f ` x ) ) |