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 5202 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
2 | 1 | simplbi 272 | 1 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 3121 ran crn 4612 Fn wfn 5193 ⟶wf 5194 |
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 5202 |
This theorem is referenced by: ffnd 5348 ffun 5350 frel 5352 fdm 5353 fresin 5376 fcoi1 5378 feu 5380 f0bi 5390 fnconstg 5395 f1fn 5405 fofn 5422 dffo2 5424 f1ofn 5443 feqmptd 5549 fvco3 5567 ffvelrn 5629 dff2 5640 dffo3 5643 dffo4 5644 dffo5 5645 f1ompt 5647 ffnfv 5654 fcompt 5666 fsn2 5670 fconst2g 5711 fconstfvm 5714 fex 5725 dff13 5747 cocan1 5766 off 6073 suppssof1 6078 ofco 6079 caofref 6082 caofrss 6085 caoftrn 6086 fo1stresm 6140 fo2ndresm 6141 1stcof 6142 2ndcof 6143 fo2ndf 6206 tposf2 6247 smoiso 6281 tfrcllemssrecs 6331 tfrcllemsucaccv 6333 elmapfn 6649 mapsn 6668 mapen 6824 updjudhcoinlf 7057 updjudhcoinrg 7058 updjud 7059 omp1eomlem 7071 dfz2 9284 uzn0 9502 unirnioo 9930 dfioo2 9931 ioorebasg 9932 fzen 9999 fseq1p1m1 10050 2ffzeq 10097 fvinim0ffz 10197 frecuzrdglem 10367 frecuzrdgtcl 10368 frecuzrdg0 10369 frecuzrdgfunlem 10375 frecuzrdg0t 10378 seq3val 10414 seqvalcd 10415 ser0f 10471 ffz0hash 10768 fnfzo0hash 10770 shftf 10794 uzin2 10951 rexanuz 10952 prodf1f 11506 eff2 11643 reeff1 11663 tanvalap 11671 1arithlem4 12318 1arith 12319 isgrpinv 12756 lmbr2 13008 cncnpi 13022 cncnp 13024 cnpdis 13036 lmff 13043 tx1cn 13063 tx2cn 13064 upxp 13066 txcnmpt 13067 uptx 13068 xmettpos 13164 blrnps 13205 blrn 13206 xmeterval 13229 qtopbasss 13315 cnbl0 13328 cnblcld 13329 tgioo 13340 tgqioo 13341 dvfre 13468 reeff1o 13488 pilem1 13494 ioocosf1o 13569 dfrelog 13575 012of 14028 2o01f 14029 taupi 14102 |
Copyright terms: Public domain | W3C validator |