![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > f1ofn | Unicode version |
Description: A one-to-one onto mapping is function on its domain. (Contributed by NM, 12-Dec-2003.) |
Ref | Expression |
---|---|
f1ofn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1of 5821 | . 2 | |
2 | ffn 5736 | . 2 | |
3 | 1, 2 | syl 16 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 Fn wfn 5588
--> wf 5589 -1-1-onto-> wf1o 5592 |
This theorem is referenced by: f1ofun 5823 f1odm 5825 fveqf1o 6205 isomin 6233 isoini 6234 isofrlem 6236 isoselem 6237 weniso 6250 bren 7545 enfixsn 7646 phplem4 7719 php3 7723 domunfican 7813 fiint 7817 supisolem 7952 ordiso2 7961 unxpwdom2 8035 wemapwe 8160 wemapweOLD 8161 infxpenlem 8412 ackbij2lem2 8641 ackbij2lem3 8642 fpwwe2lem9 9037 canthp1lem2 9052 hashfacen 12503 hashf1lem1 12504 fprodss 13755 phimullem 14309 unbenlem 14426 0ram 14538 symgfixelsi 16460 symgfixf1 16462 f1omvdmvd 16468 f1omvdcnv 16469 f1omvdconj 16471 f1otrspeq 16472 symggen 16495 psgnunilem1 16518 dprdf1o 17079 znleval 18593 znunithash 18603 mdetdiaglem 19100 basqtop 20212 tgqtop 20213 reghmph 20294 ordthmeolem 20302 qtophmeo 20318 imasf1oxmet 20878 imasf1omet 20879 imasf1obl 20991 imasf1oxms 20992 cnheiborlem 21454 ovolctb 21901 mbfimaopnlem 22062 axcontlem5 24271 vdgr1d 24903 vdgr1b 24904 vdgr1a 24906 eupai 24967 eupatrl 24968 eupap1 24976 eupath2lem3 24979 vdegp1ai 24984 vdegp1bi 24985 nvinvfval 25535 adjbd1o 27004 isoun 27520 indf1ofs 28039 eulerpartgbij 28311 eulerpartlemgh 28317 ballotlemsima 28454 derangenlem 28615 subfacp1lem3 28626 subfacp1lem4 28627 subfacp1lem5 28628 kelac1 31009 gicabl 31047 stoweidlem27 31809 usgra2adedglem1 32356 ltrnid 35859 ltrneq2 35872 cdleme51finvN 36282 diaintclN 36785 dibintclN 36894 mapdcl 37380 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 185 df-an 371 df-f 5597 df-f1 5598 df-f1o 5600 |
Copyright terms: Public domain | W3C validator |