![]() |
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 | ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f 5053 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
2 | 1 | simplbi 269 | 1 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 3013 ran crn 4468 Fn wfn 5044 ⟶wf 5045 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-f 5053 |
This theorem is referenced by: ffnd 5196 ffun 5198 frel 5200 fdm 5201 fresin 5224 fcoi1 5226 feu 5228 f0bi 5238 fnconstg 5243 f1fn 5253 fofn 5270 dffo2 5272 f1ofn 5289 feqmptd 5392 fvco3 5410 ffvelrn 5471 dff2 5482 dffo3 5485 dffo4 5486 dffo5 5487 f1ompt 5489 ffnfv 5495 fcompt 5506 fsn2 5510 fconst2g 5551 fconstfvm 5554 fex 5563 dff13 5585 cocan1 5604 off 5906 suppssof1 5910 ofco 5911 caofref 5914 caofrss 5917 caoftrn 5918 fo1stresm 5970 fo2ndresm 5971 1stcof 5972 2ndcof 5973 fo2ndf 6030 tposf2 6071 smoiso 6105 tfrcllemssrecs 6155 tfrcllemsucaccv 6157 elmapfn 6468 mapsn 6487 mapen 6642 updjudhcoinlf 6851 updjudhcoinrg 6852 updjud 6853 dfz2 8917 uzn0 9133 unirnioo 9539 dfioo2 9540 ioorebasg 9541 fzen 9606 fseq1p1m1 9657 2ffzeq 9701 fvinim0ffz 9801 frecuzrdglem 9967 frecuzrdgtcl 9968 frecuzrdg0 9969 frecuzrdgfunlem 9975 frecuzrdg0t 9978 seq3val 10013 ser0f 10065 ffz0hash 10353 fnfzo0hash 10355 shftf 10379 uzin2 10535 rexanuz 10536 eff2 11119 reeff1 11140 tanvalap 11148 lmbr2 12065 cncnpi 12079 cncnp 12081 cnpdis 12093 lmff 12100 xmettpos 12156 blrnps 12197 blrn 12198 xmeterval 12221 qtopbasss 12300 cnbl0 12313 cnblcld 12314 tgioo 12322 tgqioo 12323 |
Copyright terms: Public domain | W3C validator |