![]() |
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 5232 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
2 | 1 | simplbi 274 | 1 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 3141 ran crn 4639 Fn wfn 5223 ⟶wf 5224 |
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 5232 |
This theorem is referenced by: ffnd 5378 ffun 5380 frel 5382 fdm 5383 fresin 5406 fcoi1 5408 feu 5410 f0bi 5420 fnconstg 5425 f1fn 5435 fofn 5452 dffo2 5454 f1ofn 5474 feqmptd 5582 fvco3 5600 ffvelcdm 5662 dff2 5673 dffo3 5676 dffo4 5677 dffo5 5678 f1ompt 5680 ffnfv 5687 fcompt 5699 fsn2 5703 fconst2g 5744 fconstfvm 5747 fex 5758 dff13 5782 cocan1 5801 off 6109 suppssof1 6114 ofco 6115 caofref 6118 caofrss 6121 caoftrn 6122 fo1stresm 6176 fo2ndresm 6177 1stcof 6178 2ndcof 6179 fo2ndf 6242 tposf2 6283 smoiso 6317 tfrcllemssrecs 6367 tfrcllemsucaccv 6369 elmapfn 6685 mapsn 6704 mapen 6860 updjudhcoinlf 7093 updjudhcoinrg 7094 updjud 7095 omp1eomlem 7107 dfz2 9339 uzn0 9557 unirnioo 9987 dfioo2 9988 ioorebasg 9989 fzen 10057 fseq1p1m1 10108 2ffzeq 10155 fvinim0ffz 10255 frecuzrdglem 10425 frecuzrdgtcl 10426 frecuzrdg0 10427 frecuzrdgfunlem 10433 frecuzrdg0t 10436 seq3val 10472 seqvalcd 10473 ser0f 10529 ffz0hash 10827 fnfzo0hash 10829 shftf 10853 uzin2 11010 rexanuz 11011 prodf1f 11565 eff2 11702 reeff1 11722 tanvalap 11730 1arithlem4 12378 1arith 12379 isgrpinv 12951 cnfldplusf 13750 cnfldsub 13751 lmbr2 14010 cncnpi 14024 cncnp 14026 cnpdis 14038 lmff 14045 tx1cn 14065 tx2cn 14066 upxp 14068 txcnmpt 14069 uptx 14070 xmettpos 14166 blrnps 14207 blrn 14208 xmeterval 14231 qtopbasss 14317 cnbl0 14330 cnblcld 14331 tgioo 14342 tgqioo 14343 dvfre 14470 reeff1o 14490 pilem1 14496 ioocosf1o 14571 dfrelog 14577 012of 15042 2o01f 15043 taupi 15118 |
Copyright terms: Public domain | W3C validator |