![]() |
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 2037 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biantru 286 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-fn 4848 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | bitr4i 176 |
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 99 ax-ia2 100 ax-ia3 101 ax-gen 1335 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 df-fn 4848 |
This theorem is referenced by: funssxp 5003 funforn 5056 funbrfvb 5159 funopfvb 5160 ssimaex 5177 fvco 5186 eqfunfv 5213 fvimacnvi 5224 unpreima 5235 respreima 5238 elrnrexdm 5249 elrnrexdmb 5250 ffvresb 5271 resfunexg 5325 funex 5327 elunirn 5348 smores 5848 smores2 5850 tfrlem1 5864 |
Copyright terms: Public domain | W3C validator |