| 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 3246 |
. . 3
| |
| 2 | 1 | anim2i 342 |
. 2
|
| 3 | df-fo 5276 |
. 2
| |
| 4 | df-f 5274 |
. 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 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-11 1528 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-ext 2186 |
| This theorem depends on definitions: df-bi 117 df-nf 1483 df-sb 1785 df-clab 2191 df-cleq 2197 df-clel 2200 df-in 3171 df-ss 3178 df-f 5274 df-fo 5276 |
| This theorem is referenced by: fofun 5498 fofn 5499 dffo2 5501 foima 5502 resdif 5543 ffoss 5553 fconstfvm 5801 cocan2 5856 foeqcnvco 5858 focdmex 6199 algrflem 6314 algrflemg 6315 tposf2 6353 mapsn 6776 ssdomg 6869 fopwdom 6932 fidcenumlemrks 7054 fidcenumlemr 7056 ctmlemr 7209 ctm 7210 ctssdclemn0 7211 ctssdccl 7212 ctssdc 7214 enumctlemm 7215 enumct 7216 fodjuomnilemdc 7245 exmidfodomrlemr 7309 exmidfodomrlemrALT 7310 suplocexprlemdisj 7832 suplocexprlemub 7835 wrdsymb 11019 ennnfonelemdc 12712 ennnfonelemg 12716 ennnfonelemp1 12719 ennnfonelemhdmp1 12722 ennnfonelemkh 12725 ennnfonelemhf1o 12726 ennnfonelemex 12727 ennnfonelemhom 12728 ctinfomlemom 12740 ctinf 12743 ctiunctlemudc 12750 ctiunctlemf 12751 omctfn 12756 imasival 13080 imasbas 13081 imasplusg 13082 imasmulr 13083 imasaddfnlemg 13088 imasaddvallemg 13089 imasaddflemg 13090 imasmnd2 13226 imasgrp2 13388 mhmid 13393 mhmmnd 13394 mhmfmhm 13395 ghmgrp 13396 ghmfghm 13604 imasring 13768 znunit 14363 znrrg 14364 dvrecap 15127 gausslemma2dlem1f1o 15479 subctctexmid 15870 pw1nct 15873 |
| Copyright terms: Public domain | W3C validator |