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 2164 | . . 3 | |
2 | 1 | biantru 300 | . 2 |
3 | df-fn 5185 | . 2 | |
4 | 2, 3 | bitr4i 186 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wceq 1342 cdm 4598 wfun 5176 wfn 5177 |
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 1436 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 df-fn 5185 |
This theorem is referenced by: funfnd 5213 funssxp 5351 funforn 5411 funbrfvb 5523 funopfvb 5524 ssimaex 5541 fvco 5550 eqfunfv 5582 fvimacnvi 5593 unpreima 5604 respreima 5607 elrnrexdm 5618 elrnrexdmb 5619 ffvresb 5642 funresdfunsnss 5682 resfunexg 5700 funex 5702 elunirn 5728 smores 6251 smores2 6253 tfrlem1 6267 funresdfunsndc 6465 fundmfibi 6895 resunimafz0 10730 fclim 11221 |
Copyright terms: Public domain | W3C validator |