![]() |
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 2115 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biantru 298 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-fn 5084 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | bitr4i 186 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1408 ax-ext 2097 |
This theorem depends on definitions: df-bi 116 df-cleq 2108 df-fn 5084 |
This theorem is referenced by: funfnd 5112 funssxp 5250 funforn 5310 funbrfvb 5418 funopfvb 5419 ssimaex 5436 fvco 5445 eqfunfv 5477 fvimacnvi 5488 unpreima 5499 respreima 5502 elrnrexdm 5513 elrnrexdmb 5514 ffvresb 5537 funresdfunsnss 5577 resfunexg 5595 funex 5597 elunirn 5621 smores 6143 smores2 6145 tfrlem1 6159 funresdfunsndc 6356 fundmfibi 6779 resunimafz0 10467 fclim 10955 |
Copyright terms: Public domain | W3C validator |