Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1083.3 |
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) ) |
2 |
|
bnj1083.8 |
|- K = { f | E. n e. D ( f Fn n /\ ph /\ ps ) } |
3 |
|
df-rex |
|- ( E. n e. D ( f Fn n /\ ph /\ ps ) <-> E. n ( n e. D /\ ( f Fn n /\ ph /\ ps ) ) ) |
4 |
2
|
abeq2i |
|- ( f e. K <-> E. n e. D ( f Fn n /\ ph /\ ps ) ) |
5 |
|
bnj252 |
|- ( ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( n e. D /\ ( f Fn n /\ ph /\ ps ) ) ) |
6 |
1 5
|
bitri |
|- ( ch <-> ( n e. D /\ ( f Fn n /\ ph /\ ps ) ) ) |
7 |
6
|
exbii |
|- ( E. n ch <-> E. n ( n e. D /\ ( f Fn n /\ ph /\ ps ) ) ) |
8 |
3 4 7
|
3bitr4i |
|- ( f e. K <-> E. n ch ) |