![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ffn | Unicode version |
Description: A mapping is a function. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
ffn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f 5239 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 274 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem depends on definitions: df-bi 117 df-f 5239 |
This theorem is referenced by: ffnd 5385 ffun 5387 frel 5389 fdm 5390 fresin 5413 fcoi1 5415 feu 5417 f0bi 5427 fnconstg 5432 f1fn 5442 fofn 5459 dffo2 5461 f1ofn 5481 feqmptd 5589 fvco3 5607 ffvelcdm 5669 dff2 5680 dffo3 5683 dffo4 5684 dffo5 5685 f1ompt 5687 ffnfv 5694 fcompt 5706 fsn2 5710 fconst2g 5751 fconstfvm 5754 fex 5765 dff13 5789 cocan1 5808 off 6118 suppssof1 6123 ofco 6124 caofref 6127 caofrss 6130 caoftrn 6131 fo1stresm 6185 fo2ndresm 6186 1stcof 6187 2ndcof 6188 fo2ndf 6251 tposf2 6292 smoiso 6326 tfrcllemssrecs 6376 tfrcllemsucaccv 6378 elmapfn 6696 mapsn 6715 pw2f1odclem 6861 mapen 6873 updjudhcoinlf 7108 updjudhcoinrg 7109 updjud 7110 omp1eomlem 7122 dfz2 9354 uzn0 9572 unirnioo 10002 dfioo2 10003 ioorebasg 10004 fzen 10072 fseq1p1m1 10123 2ffzeq 10170 fvinim0ffz 10270 frecuzrdglem 10441 frecuzrdgtcl 10442 frecuzrdg0 10443 frecuzrdgfunlem 10449 frecuzrdg0t 10452 seq3val 10488 seqvalcd 10489 ser0f 10545 ffz0hash 10844 fnfzo0hash 10846 shftf 10870 uzin2 11027 rexanuz 11028 prodf1f 11582 eff2 11719 reeff1 11739 tanvalap 11747 1arithlem4 12397 1arith 12398 isgrpinv 12995 kerf1ghm 13210 cnfldplusf 13874 cnfldsub 13875 lmbr2 14166 cncnpi 14180 cncnp 14182 cnpdis 14194 lmff 14201 tx1cn 14221 tx2cn 14222 upxp 14224 txcnmpt 14225 uptx 14226 xmettpos 14322 blrnps 14363 blrn 14364 xmeterval 14387 qtopbasss 14473 cnbl0 14486 cnblcld 14487 tgioo 14498 tgqioo 14499 dvfre 14626 reeff1o 14646 pilem1 14652 ioocosf1o 14727 dfrelog 14733 012of 15199 2o01f 15200 taupi 15275 |
Copyright terms: Public domain | W3C validator |