Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ffun | GIF version |
Description: A mapping is a function. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
ffun | ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffn 5331 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
2 | fnfun 5279 | . 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Fun wfun 5176 Fn wfn 5177 ⟶wf 5178 |
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 5185 df-f 5186 |
This theorem is referenced by: ffund 5335 funssxp 5351 f00 5373 fofun 5405 fun11iun 5447 fimacnv 5608 dff3im 5624 resflem 5643 fmptco 5645 fliftf 5761 smores2 6253 pmfun 6625 elmapfun 6629 pmresg 6633 ac6sfi 6855 casef 7044 omp1eomlem 7050 ctm 7065 exmidfodomrlemim 7148 nn0supp 9157 frecuzrdg0 10338 frecuzrdgsuc 10339 frecuzrdgdomlem 10342 frecuzrdg0t 10347 frecuzrdgsuctlem 10348 climdm 11222 sum0 11315 isumz 11316 fsumsersdc 11322 isumclim 11348 zprodap0 11508 iscnp3 12750 cnpnei 12766 cnclima 12770 cnrest2 12783 hmeores 12862 metcnp 13059 qtopbasss 13068 tgqioo 13094 dvaddxx 13214 dvmulxx 13215 dviaddf 13216 dvimulf 13217 dvef 13235 pilem3 13251 |
Copyright terms: Public domain | W3C validator |