![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > f1of | GIF version |
Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.) |
Ref | Expression |
---|---|
f1of | ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1of1 5265 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵) | |
2 | f1f 5229 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⟶wf 5024 –1-1→wf1 5025 –1-1-onto→wf1o 5027 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-f1 5033 df-f1o 5035 |
This theorem is referenced by: f1ofn 5267 f1oabexg 5278 f1ompt 5464 f1oresrab 5477 fsn 5483 fsnunf 5511 f1ocnvfv1 5570 f1ocnvfv2 5571 f1ocnvdm 5574 fcof1o 5582 isocnv 5604 isores2 5606 isotr 5609 isopolem 5615 isosolem 5617 f1oiso2 5620 f1ofveu 5654 smoiso 6081 mapsn 6461 f1oen2g 6526 en1 6570 enm 6590 mapen 6616 fidceq 6639 dif1en 6649 fin0 6655 fin0or 6656 ac6sfi 6668 en2eqpr 6677 fiintim 6693 isotilem 6755 supisoex 6758 supisoti 6759 ordiso2 6782 djuin 6810 caseinl 6836 ctm 6845 enomnilem 6855 frecuzrdgg 9884 fnn0nninf 9904 fxnn0nninf 9905 0tonninf 9906 1tonninf 9907 iseqf1olemkle 9974 iseqf1olemklt 9975 iseqf1olemqcl 9976 iseqf1olemnab 9978 iseqf1olemmo 9982 iseqf1olemqk 9984 iseqf1olemjpcl 9985 iseqf1olemfvp 9987 seq3f1olemqsumkj 9988 seq3f1olemqsumk 9989 seq3f1olemqsum 9990 seq3f1olemstep 9991 seq3f1olemp 9992 seq3f1oleml 9993 seq3f1o 9994 hashfz1 10252 omgadd 10271 hashfacen 10302 leisorel 10303 zfz1isolemiso 10305 iseqcoll 10308 cnrecnv 10405 sumeq2 10809 isummolem3 10831 isummolem2a 10832 fsumgcl 10838 fisum 10839 fsumf1o 10843 fisumss 10845 fsumcl2lem 10853 fsumadd 10861 fsummulc2 10903 sqpweven 11492 2sqpwodd 11493 phimullem 11540 |
Copyright terms: Public domain | W3C validator |