Theorem f1of 5577

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

Syntax hints:   → wi 4  ⟶wf 5317  –1-1→wf1 5318  –1-1-onto→wf1o 5320

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 5326  df-f1o 5328

This theorem is referenced by:  f1ofn  5578  f1oabexg  5589  f1ompt  5791  f1oresrab  5805  fsn  5812  fsnunf  5846  f1ocnvfv1  5910  f1ocnvfv2  5911  f1ocnvdm  5914  fcof1o  5922  isocnv  5944  isores2  5946  isotr  5949  isopolem  5955  isosolem  5957  f1oiso2  5960  f1ofveu  5998  smoiso  6459  mapsn  6850  f1oen2g  6919  en1  6964  enm  6992  mapen  7020  fidceq  7044  dif1en  7054  fin0  7060  fin0or  7061  ac6sfi  7073  en2eqpr  7085  fiintim  7109  isotilem  7189  supisoex  7192  supisoti  7193  ordiso2  7218  caseinl  7274  caseinr  7275  omp1eomlem  7277  ctm  7292  enomnilem  7321  enmkvlem  7344  enwomnilem  7352  pr2cv1  7384  cc3  7470  frecuzrdgg  10655  fnn0nninf  10677  fxnn0nninf  10678  0tonninf  10679  1tonninf  10680  iseqf1olemkle  10736  iseqf1olemklt  10737  iseqf1olemqcl  10738  iseqf1olemnab  10740  iseqf1olemmo  10744  iseqf1olemqk  10746  iseqf1olemjpcl  10747  iseqf1olemfvp  10749  seq3f1olemqsumkj  10750  seq3f1olemqsumk  10751  seq3f1olemqsum  10752  seq3f1olemstep  10753  seq3f1olemp  10754  seq3f1oleml  10755  seq3f1o  10756  seqf1oglem1  10758  seqf1oglem2  10759  seqf1og  10760  hashfz1  11022  omgadd  11041  hashfacen  11076  leisorel  11077  zfz1isolemiso  11079  seq3coll  11082  cnrecnv  11442  sumeq2  11891  summodclem3  11912  summodclem2a  11913  fsumgcl  11918  fsum3  11919  fsumf1o  11922  fisumss  11924  fsumcl2lem  11930  fsumadd  11938  fsummulc2  11980  prodeq2  12089  prodmodclem3  12107  prodmodclem2a  12108  fprodseq  12115  fprodf1o  12120  fprodssdc  12122  fprodmul  12123  nninfctlemfo  12582  sqpweven  12718  2sqpwodd  12719  phimullem  12768  eulerthlem1  12770  eulerthlemrprm  12772  eulerthlema  12773  eulerthlemh  12774  eulerthlemth  12775  ennnfonelemjn  12994  ennnfonelemp1  12998  ennnfonelemhdmp1  13001  ennnfonelemss  13002  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ennnfonelemex  13006  ennnfonelemnn0  13014  ennnfonelemim  13016  ctinfomlemom  13019  ctiunctlemudc  13029  ctiunctlemfo  13031  ssnnctlemct  13038  idmhm  13523  mhmf1o  13524  idghm  13817  ghmf1o  13833  gsumfzreidx  13895  psrnegcl  14668  psrlinv  14669  ssidcn  14905  txhmeo  15014  dvid  15390  dvidre  15392  dvexp  15406  dfrelog  15555  relogcl  15557  uspgriedgedg  15998  012of  16470  2o01f  16471  iswomninnlem  16531