![]() |
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 5135 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
2 | 1 | simplbi 272 | 1 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 3076 ran crn 4548 Fn wfn 5126 ⟶wf 5127 |
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-f 5135 |
This theorem is referenced by: ffnd 5281 ffun 5283 frel 5285 fdm 5286 fresin 5309 fcoi1 5311 feu 5313 f0bi 5323 fnconstg 5328 f1fn 5338 fofn 5355 dffo2 5357 f1ofn 5376 feqmptd 5482 fvco3 5500 ffvelrn 5561 dff2 5572 dffo3 5575 dffo4 5576 dffo5 5577 f1ompt 5579 ffnfv 5586 fcompt 5598 fsn2 5602 fconst2g 5643 fconstfvm 5646 fex 5655 dff13 5677 cocan1 5696 off 6002 suppssof1 6007 ofco 6008 caofref 6011 caofrss 6014 caoftrn 6015 fo1stresm 6067 fo2ndresm 6068 1stcof 6069 2ndcof 6070 fo2ndf 6132 tposf2 6173 smoiso 6207 tfrcllemssrecs 6257 tfrcllemsucaccv 6259 elmapfn 6573 mapsn 6592 mapen 6748 updjudhcoinlf 6973 updjudhcoinrg 6974 updjud 6975 omp1eomlem 6987 dfz2 9147 uzn0 9365 unirnioo 9786 dfioo2 9787 ioorebasg 9788 fzen 9854 fseq1p1m1 9905 2ffzeq 9949 fvinim0ffz 10049 frecuzrdglem 10215 frecuzrdgtcl 10216 frecuzrdg0 10217 frecuzrdgfunlem 10223 frecuzrdg0t 10226 seq3val 10262 seqvalcd 10263 ser0f 10319 ffz0hash 10608 fnfzo0hash 10610 shftf 10634 uzin2 10791 rexanuz 10792 prodf1f 11344 eff2 11423 reeff1 11443 tanvalap 11451 lmbr2 12422 cncnpi 12436 cncnp 12438 cnpdis 12450 lmff 12457 tx1cn 12477 tx2cn 12478 upxp 12480 txcnmpt 12481 uptx 12482 xmettpos 12578 blrnps 12619 blrn 12620 xmeterval 12643 qtopbasss 12729 cnbl0 12742 cnblcld 12743 tgioo 12754 tgqioo 12755 dvfre 12882 reeff1o 12902 pilem1 12908 ioocosf1o 12983 dfrelog 12989 012of 13363 2o01f 13364 taupi 13430 |
Copyright terms: Public domain | W3C validator |