![]() |
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 5360 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
2 | fnfun 5308 | . 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Fun wfun 5205 Fn wfn 5206 ⟶wf 5207 |
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 5214 df-f 5215 |
This theorem is referenced by: ffund 5364 funssxp 5380 f00 5402 fofun 5434 fun11iun 5477 fimacnv 5640 dff3im 5656 resflem 5675 fmptco 5677 fliftf 5793 smores2 6288 pmfun 6661 elmapfun 6665 pmresg 6669 ac6sfi 6891 casef 7080 omp1eomlem 7086 ctm 7101 exmidfodomrlemim 7193 nn0supp 9204 frecuzrdg0 10386 frecuzrdgsuc 10387 frecuzrdgdomlem 10390 frecuzrdg0t 10395 frecuzrdgsuctlem 10396 climdm 11274 sum0 11367 isumz 11368 fsumsersdc 11374 isumclim 11400 zprodap0 11560 iscnp3 13336 cnpnei 13352 cnclima 13356 cnrest2 13369 hmeores 13448 metcnp 13645 qtopbasss 13654 tgqioo 13680 dvaddxx 13800 dvmulxx 13801 dviaddf 13802 dvimulf 13803 dvef 13821 pilem3 13837 |
Copyright terms: Public domain | W3C validator |