![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fof | Unicode version |
Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
fof |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqimss 3233 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anim2i 342 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-fo 5260 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-f 5258 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3imtr4i 201 |
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 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2175 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2180 df-cleq 2186 df-clel 2189 df-in 3159 df-ss 3166 df-f 5258 df-fo 5260 |
This theorem is referenced by: fofun 5477 fofn 5478 dffo2 5480 foima 5481 resdif 5522 ffoss 5532 fconstfvm 5776 cocan2 5831 foeqcnvco 5833 focdmex 6167 algrflem 6282 algrflemg 6283 tposf2 6321 mapsn 6744 ssdomg 6832 fopwdom 6892 fidcenumlemrks 7012 fidcenumlemr 7014 ctmlemr 7167 ctm 7168 ctssdclemn0 7169 ctssdccl 7170 ctssdc 7172 enumctlemm 7173 enumct 7174 fodjuomnilemdc 7203 exmidfodomrlemr 7262 exmidfodomrlemrALT 7263 suplocexprlemdisj 7780 suplocexprlemub 7783 wrdsymb 10941 ennnfonelemdc 12556 ennnfonelemg 12560 ennnfonelemp1 12563 ennnfonelemhdmp1 12566 ennnfonelemkh 12569 ennnfonelemhf1o 12570 ennnfonelemex 12571 ennnfonelemhom 12572 ctinfomlemom 12584 ctinf 12587 ctiunctlemudc 12594 ctiunctlemf 12595 omctfn 12600 imasival 12889 imasbas 12890 imasplusg 12891 imasmulr 12892 imasaddfnlemg 12897 imasaddvallemg 12898 imasaddflemg 12899 imasgrp2 13180 mhmid 13185 mhmmnd 13186 mhmfmhm 13187 ghmgrp 13188 ghmfghm 13396 imasring 13560 znunit 14147 znrrg 14148 dvrecap 14862 gausslemma2dlem1f1o 15176 subctctexmid 15491 pw1nct 15493 |
Copyright terms: Public domain | W3C validator |