Step |
Hyp |
Ref |
Expression |
1 |
|
ac6s.1 |
|- A e. _V |
2 |
|
ac6s.2 |
|- ( y = ( f ` x ) -> ( ph <-> ps ) ) |
3 |
|
rexv |
|- ( E. y e. _V ph <-> E. y ph ) |
4 |
3
|
ralbii |
|- ( A. x e. A E. y e. _V ph <-> A. x e. A E. y ph ) |
5 |
1 2
|
ac6s |
|- ( A. x e. A E. y e. _V ph -> E. f ( f : A --> _V /\ A. x e. A ps ) ) |
6 |
|
ffn |
|- ( f : A --> _V -> f Fn A ) |
7 |
6
|
anim1i |
|- ( ( f : A --> _V /\ A. x e. A ps ) -> ( f Fn A /\ A. x e. A ps ) ) |
8 |
7
|
eximi |
|- ( E. f ( f : A --> _V /\ A. x e. A ps ) -> E. f ( f Fn A /\ A. x e. A ps ) ) |
9 |
5 8
|
syl |
|- ( A. x e. A E. y e. _V ph -> E. f ( f Fn A /\ A. x e. A ps ) ) |
10 |
4 9
|
sylbir |
|- ( A. x e. A E. y ph -> E. f ( f Fn A /\ A. x e. A ps ) ) |