![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ffun | Unicode version |
Description: A mapping is a function. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
ffun |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffn 5384 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fnfun 5332 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem depends on definitions: df-bi 117 df-fn 5238 df-f 5239 |
This theorem is referenced by: ffund 5388 funssxp 5404 f00 5426 fofun 5458 fun11iun 5501 fimacnv 5666 dff3im 5682 resflem 5701 fmptco 5703 fliftf 5821 smores2 6319 pmfun 6694 elmapfun 6698 pmresg 6702 ac6sfi 6926 casef 7117 omp1eomlem 7123 ctm 7138 exmidfodomrlemim 7230 nn0supp 9258 frecuzrdg0 10444 frecuzrdgsuc 10445 frecuzrdgdomlem 10448 frecuzrdg0t 10453 frecuzrdgsuctlem 10454 climdm 11335 sum0 11428 isumz 11429 fsumsersdc 11435 isumclim 11461 zprodap0 11621 psrbaglesuppg 13950 iscnp3 14163 cnpnei 14179 cnclima 14183 cnrest2 14196 hmeores 14275 metcnp 14472 qtopbasss 14481 tgqioo 14507 dvaddxx 14627 dvmulxx 14628 dviaddf 14629 dvimulf 14630 dvef 14648 pilem3 14664 |
Copyright terms: Public domain | W3C validator |