![]() |
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 5032 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 269 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-f 5032 |
This theorem is referenced by: ffnd 5175 ffun 5177 frel 5178 fdm 5179 fresin 5202 fcoi1 5204 feu 5206 f0bi 5216 fnconstg 5221 f1fn 5231 fofn 5248 dffo2 5250 f1ofn 5267 feqmptd 5370 fvco3 5388 ffvelrn 5446 dff2 5457 dffo3 5460 dffo4 5461 dffo5 5462 f1ompt 5464 ffnfv 5470 fcompt 5481 fsn2 5485 fconst2g 5526 fconstfvm 5529 fex 5538 dff13 5561 cocan1 5580 off 5882 suppssof1 5886 ofco 5887 caofref 5890 caofrss 5893 caoftrn 5894 fo1stresm 5946 fo2ndresm 5947 1stcof 5948 2ndcof 5949 fo2ndf 6006 tposf2 6047 smoiso 6081 tfrcllemssrecs 6131 tfrcllemsucaccv 6133 elmapfn 6442 mapsn 6461 mapen 6616 updjudhcoinlf 6825 updjudhcoinrg 6826 updjud 6827 dfz2 8880 uzn0 9095 unirnioo 9452 dfioo2 9453 ioorebasg 9454 fzen 9518 fseq1p1m1 9569 2ffzeq 9613 fvinim0ffz 9713 frecuzrdglem 9879 frecuzrdgtcl 9880 frecuzrdg0 9881 frecuzrdgfunlem 9887 frecuzrdg0t 9890 iseqvalt 9934 seq3val 9935 iseqoveq 9946 iseqsst 9947 iseqfeq2 9952 iseqfeq 9957 iser0f 10009 ser0f 10011 facnn 10196 fac0 10197 ffz0hash 10299 fnfzo0hash 10301 shftf 10325 uzin2 10481 rexanuz 10482 eff2 11031 reeff1 11052 tanvalap 11060 |
Copyright terms: Public domain | W3C validator |