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 5097 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
2 | 1 | simplbi 272 | 1 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 3041 ran crn 4510 Fn wfn 5088 ⟶wf 5089 |
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 5097 |
This theorem is referenced by: ffnd 5243 ffun 5245 frel 5247 fdm 5248 fresin 5271 fcoi1 5273 feu 5275 f0bi 5285 fnconstg 5290 f1fn 5300 fofn 5317 dffo2 5319 f1ofn 5336 feqmptd 5442 fvco3 5460 ffvelrn 5521 dff2 5532 dffo3 5535 dffo4 5536 dffo5 5537 f1ompt 5539 ffnfv 5546 fcompt 5558 fsn2 5562 fconst2g 5603 fconstfvm 5606 fex 5615 dff13 5637 cocan1 5656 off 5962 suppssof1 5967 ofco 5968 caofref 5971 caofrss 5974 caoftrn 5975 fo1stresm 6027 fo2ndresm 6028 1stcof 6029 2ndcof 6030 fo2ndf 6092 tposf2 6133 smoiso 6167 tfrcllemssrecs 6217 tfrcllemsucaccv 6219 elmapfn 6533 mapsn 6552 mapen 6708 updjudhcoinlf 6933 updjudhcoinrg 6934 updjud 6935 omp1eomlem 6947 dfz2 9091 uzn0 9309 unirnioo 9724 dfioo2 9725 ioorebasg 9726 fzen 9791 fseq1p1m1 9842 2ffzeq 9886 fvinim0ffz 9986 frecuzrdglem 10152 frecuzrdgtcl 10153 frecuzrdg0 10154 frecuzrdgfunlem 10160 frecuzrdg0t 10163 seq3val 10199 seqvalcd 10200 ser0f 10256 ffz0hash 10544 fnfzo0hash 10546 shftf 10570 uzin2 10727 rexanuz 10728 eff2 11313 reeff1 11334 tanvalap 11342 lmbr2 12310 cncnpi 12324 cncnp 12326 cnpdis 12338 lmff 12345 tx1cn 12365 tx2cn 12366 upxp 12368 txcnmpt 12369 uptx 12370 xmettpos 12466 blrnps 12507 blrn 12508 xmeterval 12531 qtopbasss 12617 cnbl0 12630 cnblcld 12631 tgioo 12642 tgqioo 12643 dvfre 12770 pilem1 12787 isomninnlem 13152 taupi 13166 |
Copyright terms: Public domain | W3C validator |