Step |
Hyp |
Ref |
Expression |
1 |
|
ancom |
|- ( ( A. x e. A E* y x F y /\ A. x e. A E. y x F y ) <-> ( A. x e. A E. y x F y /\ A. x e. A E* y x F y ) ) |
2 |
|
vex |
|- y e. _V |
3 |
2
|
brresi |
|- ( x ( F |` A ) y <-> ( x e. A /\ x F y ) ) |
4 |
3
|
mobii |
|- ( E* y x ( F |` A ) y <-> E* y ( x e. A /\ x F y ) ) |
5 |
|
moanimv |
|- ( E* y ( x e. A /\ x F y ) <-> ( x e. A -> E* y x F y ) ) |
6 |
4 5
|
bitri |
|- ( E* y x ( F |` A ) y <-> ( x e. A -> E* y x F y ) ) |
7 |
6
|
albii |
|- ( A. x E* y x ( F |` A ) y <-> A. x ( x e. A -> E* y x F y ) ) |
8 |
|
relres |
|- Rel ( F |` A ) |
9 |
|
dffun6 |
|- ( Fun ( F |` A ) <-> ( Rel ( F |` A ) /\ A. x E* y x ( F |` A ) y ) ) |
10 |
8 9
|
mpbiran |
|- ( Fun ( F |` A ) <-> A. x E* y x ( F |` A ) y ) |
11 |
|
df-ral |
|- ( A. x e. A E* y x F y <-> A. x ( x e. A -> E* y x F y ) ) |
12 |
7 10 11
|
3bitr4i |
|- ( Fun ( F |` A ) <-> A. x e. A E* y x F y ) |
13 |
|
dmres |
|- dom ( F |` A ) = ( A i^i dom F ) |
14 |
|
inss1 |
|- ( A i^i dom F ) C_ A |
15 |
13 14
|
eqsstri |
|- dom ( F |` A ) C_ A |
16 |
|
eqss |
|- ( dom ( F |` A ) = A <-> ( dom ( F |` A ) C_ A /\ A C_ dom ( F |` A ) ) ) |
17 |
15 16
|
mpbiran |
|- ( dom ( F |` A ) = A <-> A C_ dom ( F |` A ) ) |
18 |
|
dfss3 |
|- ( A C_ dom ( F |` A ) <-> A. x e. A x e. dom ( F |` A ) ) |
19 |
13
|
elin2 |
|- ( x e. dom ( F |` A ) <-> ( x e. A /\ x e. dom F ) ) |
20 |
19
|
baib |
|- ( x e. A -> ( x e. dom ( F |` A ) <-> x e. dom F ) ) |
21 |
|
vex |
|- x e. _V |
22 |
21
|
eldm |
|- ( x e. dom F <-> E. y x F y ) |
23 |
20 22
|
bitrdi |
|- ( x e. A -> ( x e. dom ( F |` A ) <-> E. y x F y ) ) |
24 |
23
|
ralbiia |
|- ( A. x e. A x e. dom ( F |` A ) <-> A. x e. A E. y x F y ) |
25 |
18 24
|
bitri |
|- ( A C_ dom ( F |` A ) <-> A. x e. A E. y x F y ) |
26 |
17 25
|
bitri |
|- ( dom ( F |` A ) = A <-> A. x e. A E. y x F y ) |
27 |
12 26
|
anbi12i |
|- ( ( Fun ( F |` A ) /\ dom ( F |` A ) = A ) <-> ( A. x e. A E* y x F y /\ A. x e. A E. y x F y ) ) |
28 |
|
r19.26 |
|- ( A. x e. A ( E. y x F y /\ E* y x F y ) <-> ( A. x e. A E. y x F y /\ A. x e. A E* y x F y ) ) |
29 |
1 27 28
|
3bitr4i |
|- ( ( Fun ( F |` A ) /\ dom ( F |` A ) = A ) <-> A. x e. A ( E. y x F y /\ E* y x F y ) ) |
30 |
|
df-fn |
|- ( ( F |` A ) Fn A <-> ( Fun ( F |` A ) /\ dom ( F |` A ) = A ) ) |
31 |
|
df-eu |
|- ( E! y x F y <-> ( E. y x F y /\ E* y x F y ) ) |
32 |
31
|
ralbii |
|- ( A. x e. A E! y x F y <-> A. x e. A ( E. y x F y /\ E* y x F y ) ) |
33 |
29 30 32
|
3bitr4i |
|- ( ( F |` A ) Fn A <-> A. x e. A E! y x F y ) |