Theorem f1of 5507

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

Syntax hints:   → wi 4  ⟶wf 5255  –1-1→wf1 5256  –1-1-onto→wf1o 5258

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 5264  df-f1o 5266

This theorem is referenced by:  f1ofn  5508  f1oabexg  5519  f1ompt  5716  f1oresrab  5730  fsn  5737  fsnunf  5765  f1ocnvfv1  5827  f1ocnvfv2  5828  f1ocnvdm  5831  fcof1o  5839  isocnv  5861  isores2  5863  isotr  5866  isopolem  5872  isosolem  5874  f1oiso2  5877  f1ofveu  5913  smoiso  6369  mapsn  6758  f1oen2g  6823  en1  6867  enm  6888  mapen  6916  fidceq  6939  dif1en  6949  fin0  6955  fin0or  6956  ac6sfi  6968  en2eqpr  6977  fiintim  7001  isotilem  7081  supisoex  7084  supisoti  7085  ordiso2  7110  caseinl  7166  caseinr  7167  omp1eomlem  7169  ctm  7184  enomnilem  7213  enmkvlem  7236  enwomnilem  7244  cc3  7353  frecuzrdgg  10527  fnn0nninf  10549  fxnn0nninf  10550  0tonninf  10551  1tonninf  10552  iseqf1olemkle  10608  iseqf1olemklt  10609  iseqf1olemqcl  10610  iseqf1olemnab  10612  iseqf1olemmo  10616  iseqf1olemqk  10618  iseqf1olemjpcl  10619  iseqf1olemfvp  10621  seq3f1olemqsumkj  10622  seq3f1olemqsumk  10623  seq3f1olemqsum  10624  seq3f1olemstep  10625  seq3f1olemp  10626  seq3f1oleml  10627  seq3f1o  10628  seqf1oglem1  10630  seqf1oglem2  10631  seqf1og  10632  hashfz1  10894  omgadd  10913  hashfacen  10947  leisorel  10948  zfz1isolemiso  10950  seq3coll  10953  cnrecnv  11094  sumeq2  11543  summodclem3  11564  summodclem2a  11565  fsumgcl  11570  fsum3  11571  fsumf1o  11574  fisumss  11576  fsumcl2lem  11582  fsumadd  11590  fsummulc2  11632  prodeq2  11741  prodmodclem3  11759  prodmodclem2a  11760  fprodseq  11767  fprodf1o  11772  fprodssdc  11774  fprodmul  11775  nninfctlemfo  12234  sqpweven  12370  2sqpwodd  12371  phimullem  12420  eulerthlem1  12422  eulerthlemrprm  12424  eulerthlema  12425  eulerthlemh  12426  eulerthlemth  12427  ennnfonelemjn  12646  ennnfonelemp1  12650  ennnfonelemhdmp1  12653  ennnfonelemss  12654  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ennnfonelemex  12658  ennnfonelemnn0  12666  ennnfonelemim  12668  ctinfomlemom  12671  ctiunctlemudc  12681  ctiunctlemfo  12683  ssnnctlemct  12690  idmhm  13173  mhmf1o  13174  idghm  13467  ghmf1o  13483  gsumfzreidx  13545  psrnegcl  14313  psrlinv  14314  ssidcn  14532  txhmeo  14641  dvid  15017  dvidre  15019  dvexp  15033  dfrelog  15182  relogcl  15184  012of  15726  2o01f  15727  iswomninnlem  15784