![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ffn | GIF version |
Description: A mapping is a function. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
ffn | ⊢ (𝐹:A⟶B → 𝐹 Fn A) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f 4849 | . 2 ⊢ (𝐹:A⟶B ↔ (𝐹 Fn A ∧ ran 𝐹 ⊆ B)) | |
2 | 1 | simplbi 259 | 1 ⊢ (𝐹:A⟶B → 𝐹 Fn A) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 2911 ran crn 4289 Fn wfn 4840 ⟶wf 4841 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 |
This theorem depends on definitions: df-bi 110 df-f 4849 |
This theorem is referenced by: ffun 4991 frel 4992 fdm 4993 fresin 5011 fcoi1 5013 feu 5015 fnconstg 5027 f1fn 5036 fofn 5051 dffo2 5053 f1ofn 5070 feqmptd 5169 fvco3 5187 ffvelrn 5243 dff2 5254 dffo3 5257 dffo4 5258 dffo5 5259 f1ompt 5263 ffnfv 5266 fcompt 5276 fsn2 5280 fconst2g 5319 fconstfvm 5322 fex 5331 dff13 5350 cocan1 5370 off 5666 suppssof1 5670 ofco 5671 caofref 5674 caofrss 5677 caoftrn 5678 fo1stresm 5730 fo2ndresm 5731 1stcof 5732 2ndcof 5733 fo2ndf 5790 tposf2 5824 smoiso 5858 dfz2 8089 uzn0 8264 unirnioo 8612 dfioo2 8613 ioorebasg 8614 fzen 8677 fseq1p1m1 8726 2ffzeq 8768 |
Copyright terms: Public domain | W3C validator |