![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ffun | Unicode version |
Description: A mapping is a function. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
ffun |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffn 5161 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fnfun 5111 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
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 104 |
This theorem depends on definitions: df-bi 115 df-fn 5018 df-f 5019 |
This theorem is referenced by: funssxp 5180 f00 5202 fofun 5234 fun11iun 5274 fimacnv 5428 dff3im 5444 resflem 5462 fmptco 5464 fliftf 5578 smores2 6059 pmfun 6423 elmapfun 6427 pmresg 6431 ac6sfi 6612 casef 6777 exmidfodomrlemim 6825 nn0supp 8723 frecuzrdg0 9816 frecuzrdgsuc 9817 frecuzrdgdomlem 9820 frecuzrdg0t 9825 frecuzrdgsuctlem 9826 climdm 10679 sum0 10776 isumz 10777 fisumsers 10784 isumclim 10811 |
Copyright terms: Public domain | W3C validator |