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 2139 | . . 3 | |
2 | 1 | biantru 300 | . 2 |
3 | df-fn 5126 | . 2 | |
4 | 2, 3 | bitr4i 186 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wceq 1331 cdm 4539 wfun 5117 wfn 5118 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1425 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-cleq 2132 df-fn 5126 |
This theorem is referenced by: funfnd 5154 funssxp 5292 funforn 5352 funbrfvb 5464 funopfvb 5465 ssimaex 5482 fvco 5491 eqfunfv 5523 fvimacnvi 5534 unpreima 5545 respreima 5548 elrnrexdm 5559 elrnrexdmb 5560 ffvresb 5583 funresdfunsnss 5623 resfunexg 5641 funex 5643 elunirn 5667 smores 6189 smores2 6191 tfrlem1 6205 funresdfunsndc 6402 fundmfibi 6827 resunimafz0 10574 fclim 11063 |
Copyright terms: Public domain | W3C validator |