Theorem f1of 5580

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 5579	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)
2		f1f 5539	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4  ⟶wf 5320  –1-1→wf1 5321  –1-1-onto→wf1o 5323

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 5329  df-f1o 5331

This theorem is referenced by:  f1ofn  5581  f1oabexg  5592  f1ompt  5794  f1oresrab  5808  fsn  5815  fsnunf  5849  f1ocnvfv1  5913  f1ocnvfv2  5914  f1ocnvdm  5917  fcof1o  5925  isocnv  5947  isores2  5949  isotr  5952  isopolem  5958  isosolem  5960  f1oiso2  5963  f1ofveu  6001  smoiso  6463  mapsn  6854  f1oen2g  6923  en1  6968  enm  6999  mapen  7027  fidceq  7051  dif1en  7063  fin0  7069  fin0or  7070  ac6sfi  7082  en2eqpr  7094  fiintim  7118  isotilem  7199  supisoex  7202  supisoti  7203  ordiso2  7228  caseinl  7284  caseinr  7285  omp1eomlem  7287  ctm  7302  enomnilem  7331  enmkvlem  7354  enwomnilem  7362  pr2cv1  7394  cc3  7480  frecuzrdgg  10671  fnn0nninf  10693  fxnn0nninf  10694  0tonninf  10695  1tonninf  10696  iseqf1olemkle  10752  iseqf1olemklt  10753  iseqf1olemqcl  10754  iseqf1olemnab  10756  iseqf1olemmo  10760  iseqf1olemqk  10762  iseqf1olemjpcl  10763  iseqf1olemfvp  10765  seq3f1olemqsumkj  10766  seq3f1olemqsumk  10767  seq3f1olemqsum  10768  seq3f1olemstep  10769  seq3f1olemp  10770  seq3f1oleml  10771  seq3f1o  10772  seqf1oglem1  10774  seqf1oglem2  10775  seqf1og  10776  hashfz1  11038  omgadd  11058  hashfacen  11093  leisorel  11094  zfz1isolemiso  11096  seq3coll  11099  cnrecnv  11464  sumeq2  11913  summodclem3  11934  summodclem2a  11935  fsumgcl  11940  fsum3  11941  fsumf1o  11944  fisumss  11946  fsumcl2lem  11952  fsumadd  11960  fsummulc2  12002  prodeq2  12111  prodmodclem3  12129  prodmodclem2a  12130  fprodseq  12137  fprodf1o  12142  fprodssdc  12144  fprodmul  12145  nninfctlemfo  12604  sqpweven  12740  2sqpwodd  12741  phimullem  12790  eulerthlem1  12792  eulerthlemrprm  12794  eulerthlema  12795  eulerthlemh  12796  eulerthlemth  12797  ennnfonelemjn  13016  ennnfonelemp1  13020  ennnfonelemhdmp1  13023  ennnfonelemss  13024  ennnfonelemkh  13026  ennnfonelemhf1o  13027  ennnfonelemex  13028  ennnfonelemnn0  13036  ennnfonelemim  13038  ctinfomlemom  13041  ctiunctlemudc  13051  ctiunctlemfo  13053  ssnnctlemct  13060  idmhm  13545  mhmf1o  13546  idghm  13839  ghmf1o  13855  gsumfzreidx  13917  psrnegcl  14690  psrlinv  14691  ssidcn  14927  txhmeo  15036  dvid  15412  dvidre  15414  dvexp  15428  dfrelog  15577  relogcl  15579  uspgriedgedg  16023  012of  16542  2o01f  16543  iswomninnlem  16603  gfsumval  16630  gsumgfsumlem  16633