![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > funfn | Unicode version |
Description: An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.) |
Ref | Expression |
---|---|
funfn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2177 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biantru 302 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-fn 5219 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | bitr4i 187 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-gen 1449 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-fn 5219 |
This theorem is referenced by: funfnd 5247 funssxp 5385 funforn 5445 funbrfvb 5558 funopfvb 5559 ssimaex 5577 fvco 5586 eqfunfv 5618 fvimacnvi 5630 unpreima 5641 respreima 5644 elrnrexdm 5655 elrnrexdmb 5656 ffvresb 5679 funresdfunsnss 5719 resfunexg 5737 funex 5739 elunirn 5766 smores 6292 smores2 6294 tfrlem1 6308 funresdfunsndc 6506 fundmfibi 6937 resunimafz0 10806 fclim 11297 |
Copyright terms: Public domain | W3C validator |