![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fof | Structured version Visualization version Unicode version |
Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
fof |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqimss 3484 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anim2i 573 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-fo 5588 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-f 5586 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3imtr4i 270 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-in 3411 df-ss 3418 df-f 5586 df-fo 5588 |
This theorem is referenced by: fofun 5794 fofn 5795 dffo2 5797 foima 5798 resdif 5834 fconst5 6122 fconstfvOLD 6127 cocan2 6190 foeqcnvco 6198 soisoi 6219 ffoss 6754 fornex 6762 algrflem 6905 tposf2 6997 smoiso2 7088 mapsn 7513 ssdomg 7615 fopwdom 7680 unfilem2 7836 fodomfib 7851 fofinf1o 7852 brwdomn0 8084 fowdom 8086 wdomtr 8090 wdomima2g 8101 fodomfi2 8491 wdomfil 8492 alephiso 8529 iunfictbso 8545 cofsmo 8699 isf32lem10 8792 fin1a2lem7 8836 fodomb 8954 iunfo 8964 tskuni 9208 gruima 9227 gruen 9237 axpre-sup 9593 supcvg 13914 ruclem13 14294 imasval 15411 imasvalOLD 15412 imasle 15424 imasaddfnlem 15434 imasaddflem 15436 imasvscafn 15443 imasvscaf 15445 imasless 15446 homadm 15935 homacd 15936 dmaf 15944 cdaf 15945 setcepi 15983 imasmnd2 16573 imasgrp2 16801 mhmid 16807 mhmmnd 16808 mhmfmhm 16809 ghmgrp 16810 efgred2 17403 ghmfghm 17471 ghmcyg 17530 gsumval3 17541 gsumzoppg 17577 gsum2dlem2 17603 imasring 17847 znunit 19134 znrrg 19136 cygznlem2a 19138 cygznlem3 19140 cncmp 20407 cnconn 20437 1stcfb 20460 dfac14 20633 qtopval2 20711 qtopuni 20717 qtopid 20720 qtopcld 20728 qtopcn 20729 qtopeu 20731 qtophmeo 20832 elfm3 20965 ovoliunnul 22460 uniiccdif 22535 dchrzrhcl 24173 lgsdchrval 24275 rpvmasumlem 24325 dchrmusum2 24332 dchrvmasumlem3 24337 dchrisum0ff 24345 dchrisum0flblem1 24346 rpvmasum2 24350 dchrisum0re 24351 dchrisum0lem2a 24355 fargshiftfo 25366 grpocl 25928 grporndm 25938 resgrprn 26008 subgores 26032 issubgoi 26038 ghgrplem2OLD 26095 ghgrpOLD 26096 rngosn 26132 rngodm1dm2 26146 rngosn3 26154 vafval 26222 smfval 26224 nvgf 26237 vsfval 26254 pjhf 27361 elunop 27525 unopf1o 27569 cnvunop 27571 pjinvari 27844 foresf1o 28139 rabfodom 28140 iunrdx 28179 fimacnvinrn 28235 xppreima 28248 qtophaus 28663 sigapildsys 28984 carsgclctunlem3 29152 mtyf 30190 ghomfo 30309 ghomcl 30310 ghomgsg 30311 ghomf1olem 30312 bdaydm 30567 poimirlem26 31966 poimirlem27 31967 volsupnfl 31985 cocanfo 32044 exidreslem 32175 founiiun 37446 founiiun0 37465 mapsnd 37476 sge0fodjrnlem 38258 ismeannd 38305 caragenunicl 38345 |
Copyright terms: Public domain | W3C validator |