![]() |
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 2088 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biantru 296 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-fn 5018 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | bitr4i 185 |
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 104 ax-ia2 105 ax-ia3 106 ax-gen 1383 ax-ext 2070 |
This theorem depends on definitions: df-bi 115 df-cleq 2081 df-fn 5018 |
This theorem is referenced by: funssxp 5180 funforn 5240 funbrfvb 5347 funopfvb 5348 ssimaex 5365 fvco 5374 eqfunfv 5402 fvimacnvi 5413 unpreima 5424 respreima 5427 elrnrexdm 5438 elrnrexdmb 5439 ffvresb 5461 funresdfunsnss 5500 resfunexg 5518 funex 5520 elunirn 5545 smores 6057 smores2 6059 tfrlem1 6073 fundmfibi 6646 resunimafz0 10232 fclim 10678 |
Copyright terms: Public domain | W3C validator |