Step |
Hyp |
Ref |
Expression |
1 |
|
ac6sg.1 |
|- ( y = ( f ` x ) -> ( ph <-> ps ) ) |
2 |
|
raleq |
|- ( z = A -> ( A. x e. z E. y e. B ph <-> A. x e. A E. y e. B ph ) ) |
3 |
|
feq2 |
|- ( z = A -> ( f : z --> B <-> f : A --> B ) ) |
4 |
|
raleq |
|- ( z = A -> ( A. x e. z ps <-> A. x e. A ps ) ) |
5 |
3 4
|
anbi12d |
|- ( z = A -> ( ( f : z --> B /\ A. x e. z ps ) <-> ( f : A --> B /\ A. x e. A ps ) ) ) |
6 |
5
|
exbidv |
|- ( z = A -> ( E. f ( f : z --> B /\ A. x e. z ps ) <-> E. f ( f : A --> B /\ A. x e. A ps ) ) ) |
7 |
2 6
|
imbi12d |
|- ( z = A -> ( ( A. x e. z E. y e. B ph -> E. f ( f : z --> B /\ A. x e. z ps ) ) <-> ( A. x e. A E. y e. B ph -> E. f ( f : A --> B /\ A. x e. A ps ) ) ) ) |
8 |
|
vex |
|- z e. _V |
9 |
8 1
|
ac6s |
|- ( A. x e. z E. y e. B ph -> E. f ( f : z --> B /\ A. x e. z ps ) ) |
10 |
7 9
|
vtoclg |
|- ( A e. V -> ( A. x e. A E. y e. B ph -> E. f ( f : A --> B /\ A. x e. A ps ) ) ) |