Step |
Hyp |
Ref |
Expression |
1 |
|
ac5.1 |
|- A e. _V |
2 |
|
fneq2 |
|- ( y = A -> ( f Fn y <-> f Fn A ) ) |
3 |
|
raleq |
|- ( y = A -> ( A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) <-> A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) ) |
4 |
2 3
|
anbi12d |
|- ( y = A -> ( ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) <-> ( f Fn A /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) |
5 |
4
|
exbidv |
|- ( y = A -> ( E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) <-> E. f ( f Fn A /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) |
6 |
|
dfac4 |
|- ( CHOICE <-> A. y E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) |
7 |
6
|
axaci |
|- E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) |
8 |
1 5 7
|
vtocl |
|- E. f ( f Fn A /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) |