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 5173 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
2 | 1 | simplbi 272 | 1 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 3102 ran crn 4586 Fn wfn 5164 ⟶wf 5165 |
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 5173 |
This theorem is referenced by: ffnd 5319 ffun 5321 frel 5323 fdm 5324 fresin 5347 fcoi1 5349 feu 5351 f0bi 5361 fnconstg 5366 f1fn 5376 fofn 5393 dffo2 5395 f1ofn 5414 feqmptd 5520 fvco3 5538 ffvelrn 5599 dff2 5610 dffo3 5613 dffo4 5614 dffo5 5615 f1ompt 5617 ffnfv 5624 fcompt 5636 fsn2 5640 fconst2g 5681 fconstfvm 5684 fex 5693 dff13 5715 cocan1 5734 off 6041 suppssof1 6046 ofco 6047 caofref 6050 caofrss 6053 caoftrn 6054 fo1stresm 6106 fo2ndresm 6107 1stcof 6108 2ndcof 6109 fo2ndf 6171 tposf2 6212 smoiso 6246 tfrcllemssrecs 6296 tfrcllemsucaccv 6298 elmapfn 6613 mapsn 6632 mapen 6788 updjudhcoinlf 7019 updjudhcoinrg 7020 updjud 7021 omp1eomlem 7033 dfz2 9231 uzn0 9449 unirnioo 9872 dfioo2 9873 ioorebasg 9874 fzen 9940 fseq1p1m1 9991 2ffzeq 10035 fvinim0ffz 10135 frecuzrdglem 10305 frecuzrdgtcl 10306 frecuzrdg0 10307 frecuzrdgfunlem 10313 frecuzrdg0t 10316 seq3val 10352 seqvalcd 10353 ser0f 10409 ffz0hash 10699 fnfzo0hash 10701 shftf 10725 uzin2 10882 rexanuz 10883 prodf1f 11435 eff2 11572 reeff1 11592 tanvalap 11600 lmbr2 12601 cncnpi 12615 cncnp 12617 cnpdis 12629 lmff 12636 tx1cn 12656 tx2cn 12657 upxp 12659 txcnmpt 12660 uptx 12661 xmettpos 12757 blrnps 12798 blrn 12799 xmeterval 12822 qtopbasss 12908 cnbl0 12921 cnblcld 12922 tgioo 12933 tgqioo 12934 dvfre 13061 reeff1o 13081 pilem1 13087 ioocosf1o 13162 dfrelog 13168 012of 13554 2o01f 13555 taupi 13628 |
Copyright terms: Public domain | W3C validator |