Theorem f1of 5548

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

Syntax hints:   → wi 4  ⟶wf 5290  –1-1→wf1 5291  –1-1-onto→wf1o 5293

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 5299  df-f1o 5301

This theorem is referenced by:  f1ofn  5549  f1oabexg  5560  f1ompt  5759  f1oresrab  5773  fsn  5780  fsnunf  5812  f1ocnvfv1  5874  f1ocnvfv2  5875  f1ocnvdm  5878  fcof1o  5886  isocnv  5908  isores2  5910  isotr  5913  isopolem  5919  isosolem  5921  f1oiso2  5924  f1ofveu  5962  smoiso  6418  mapsn  6807  f1oen2g  6876  en1  6921  enm  6947  mapen  6975  fidceq  6999  dif1en  7009  fin0  7015  fin0or  7016  ac6sfi  7028  en2eqpr  7037  fiintim  7061  isotilem  7141  supisoex  7144  supisoti  7145  ordiso2  7170  caseinl  7226  caseinr  7227  omp1eomlem  7229  ctm  7244  enomnilem  7273  enmkvlem  7296  enwomnilem  7304  pr2cv1  7336  cc3  7422  frecuzrdgg  10605  fnn0nninf  10627  fxnn0nninf  10628  0tonninf  10629  1tonninf  10630  iseqf1olemkle  10686  iseqf1olemklt  10687  iseqf1olemqcl  10688  iseqf1olemnab  10690  iseqf1olemmo  10694  iseqf1olemqk  10696  iseqf1olemjpcl  10697  iseqf1olemfvp  10699  seq3f1olemqsumkj  10700  seq3f1olemqsumk  10701  seq3f1olemqsum  10702  seq3f1olemstep  10703  seq3f1olemp  10704  seq3f1oleml  10705  seq3f1o  10706  seqf1oglem1  10708  seqf1oglem2  10709  seqf1og  10710  hashfz1  10972  omgadd  10991  hashfacen  11025  leisorel  11026  zfz1isolemiso  11028  seq3coll  11031  cnrecnv  11387  sumeq2  11836  summodclem3  11857  summodclem2a  11858  fsumgcl  11863  fsum3  11864  fsumf1o  11867  fisumss  11869  fsumcl2lem  11875  fsumadd  11883  fsummulc2  11925  prodeq2  12034  prodmodclem3  12052  prodmodclem2a  12053  fprodseq  12060  fprodf1o  12065  fprodssdc  12067  fprodmul  12068  nninfctlemfo  12527  sqpweven  12663  2sqpwodd  12664  phimullem  12713  eulerthlem1  12715  eulerthlemrprm  12717  eulerthlema  12718  eulerthlemh  12719  eulerthlemth  12720  ennnfonelemjn  12939  ennnfonelemp1  12943  ennnfonelemhdmp1  12946  ennnfonelemss  12947  ennnfonelemkh  12949  ennnfonelemhf1o  12950  ennnfonelemex  12951  ennnfonelemnn0  12959  ennnfonelemim  12961  ctinfomlemom  12964  ctiunctlemudc  12974  ctiunctlemfo  12976  ssnnctlemct  12983  idmhm  13468  mhmf1o  13469  idghm  13762  ghmf1o  13778  gsumfzreidx  13840  psrnegcl  14612  psrlinv  14613  ssidcn  14849  txhmeo  14958  dvid  15334  dvidre  15336  dvexp  15350  dfrelog  15499  relogcl  15501  uspgriedgedg  15942  012of  16268  2o01f  16269  iswomninnlem  16328