![]() |
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 2040 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biantru 286 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-fn 4905 |
. 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 1338 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 df-fn 4905 |
This theorem is referenced by: funssxp 5060 funforn 5113 funbrfvb 5216 funopfvb 5217 ssimaex 5234 fvco 5243 eqfunfv 5270 fvimacnvi 5281 unpreima 5292 respreima 5295 elrnrexdm 5306 elrnrexdmb 5307 ffvresb 5328 resfunexg 5382 funex 5384 elunirn 5405 smores 5907 smores2 5909 tfrlem1 5923 fclim 9815 |
Copyright terms: Public domain | W3C validator |