Theorem f1of 5586

Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1of	⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)

Proof of Theorem f1of

Step	Hyp	Ref	Expression
1		f1of1 5585	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)
2		f1f 5545	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4  ⟶wf 5324  –1-1→wf1 5325  –1-1-onto→wf1o 5327

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-f1 5333  df-f1o 5335

This theorem is referenced by:  f1ofn  5587  f1oabexg  5598  f1ompt  5801  f1oresrab  5815  fsn  5822  fsnunf  5857  f1ocnvfv1  5923  f1ocnvfv2  5924  f1ocnvdm  5927  fcof1o  5935  isocnv  5957  isores2  5959  isotr  5962  isopolem  5968  isosolem  5970  f1oiso2  5973  f1ofveu  6011  smoiso  6473  mapsn  6864  f1oen2g  6933  en1  6978  enm  7009  mapen  7037  fidceq  7061  dif1en  7073  fin0  7079  fin0or  7080  ac6sfi  7092  en2eqpr  7104  fiintim  7128  isotilem  7210  supisoex  7213  supisoti  7214  ordiso2  7239  caseinl  7295  caseinr  7296  omp1eomlem  7298  ctm  7313  enomnilem  7342  enmkvlem  7365  enwomnilem  7373  pr2cv1  7405  cc3  7492  frecuzrdgg  10684  fnn0nninf  10706  fxnn0nninf  10707  0tonninf  10708  1tonninf  10709  iseqf1olemkle  10765  iseqf1olemklt  10766  iseqf1olemqcl  10767  iseqf1olemnab  10769  iseqf1olemmo  10773  iseqf1olemqk  10775  iseqf1olemjpcl  10776  iseqf1olemfvp  10778  seq3f1olemqsumkj  10779  seq3f1olemqsumk  10780  seq3f1olemqsum  10781  seq3f1olemstep  10782  seq3f1olemp  10783  seq3f1oleml  10784  seq3f1o  10785  seqf1oglem1  10787  seqf1oglem2  10788  seqf1og  10789  hashfz1  11051  omgadd  11071  hashfacen  11106  leisorel  11107  zfz1isolemiso  11109  seq3coll  11112  cnrecnv  11493  sumeq2  11942  summodclem3  11964  summodclem2a  11965  fsumgcl  11970  fsum3  11971  fsumf1o  11974  fisumss  11976  fsumcl2lem  11982  fsumadd  11990  fsummulc2  12032  prodeq2  12141  prodmodclem3  12159  prodmodclem2a  12160  fprodseq  12167  fprodf1o  12172  fprodssdc  12174  fprodmul  12175  nninfctlemfo  12634  sqpweven  12770  2sqpwodd  12771  phimullem  12820  eulerthlem1  12822  eulerthlemrprm  12824  eulerthlema  12825  eulerthlemh  12826  eulerthlemth  12827  ennnfonelemjn  13046  ennnfonelemp1  13050  ennnfonelemhdmp1  13053  ennnfonelemss  13054  ennnfonelemkh  13056  ennnfonelemhf1o  13057  ennnfonelemex  13058  ennnfonelemnn0  13066  ennnfonelemim  13068  ctinfomlemom  13071  ctiunctlemudc  13081  ctiunctlemfo  13083  ssnnctlemct  13090  idmhm  13575  mhmf1o  13576  idghm  13869  ghmf1o  13885  gsumfzreidx  13947  psrnegcl  14726  psrlinv  14727  ssidcn  14963  txhmeo  15072  dvid  15448  dvidre  15450  dvexp  15464  dfrelog  15613  relogcl  15615  uspgriedgedg  16059  012of  16652  2o01f  16653  iswomninnlem  16721  gfsumval  16748  gsumgfsumlem  16751  gfsump1  16754