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 5267 | . 2 | |
2 | fnfun 5215 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wfun 5112 wfn 5113 wf 5114 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-fn 5121 df-f 5122 |
This theorem is referenced by: ffund 5271 funssxp 5287 f00 5309 fofun 5341 fun11iun 5381 fimacnv 5542 dff3im 5558 resflem 5577 fmptco 5579 fliftf 5693 smores2 6184 pmfun 6555 elmapfun 6559 pmresg 6563 ac6sfi 6785 casef 6966 omp1eomlem 6972 ctm 6987 exmidfodomrlemim 7050 nn0supp 9022 frecuzrdg0 10179 frecuzrdgsuc 10180 frecuzrdgdomlem 10183 frecuzrdg0t 10188 frecuzrdgsuctlem 10189 climdm 11057 sum0 11150 isumz 11151 fsumsersdc 11157 isumclim 11183 iscnp3 12361 cnpnei 12377 cnclima 12381 cnrest2 12394 hmeores 12473 metcnp 12670 qtopbasss 12679 tgqioo 12705 dvaddxx 12825 dvmulxx 12826 dviaddf 12827 dvimulf 12828 dvef 12845 pilem3 12853 |
Copyright terms: Public domain | W3C validator |