Theorem f1of 5642

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

This proof depends on syntax axioms:   → wi 4  ⟶wf 5376  –1-1→wf1 5377  –1-1-onto→wf1o 5379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f1 5385  df-f1o 5387

This theorem is used by:  f1ofn  5643  f1oabexg  5654  f1ompt  5862  f1oresrab  5876  fsn  5883  fsnunf  5918  f1ocnvfv1  5986  f1ocnvfv2  5987  f1ocnvdm  5990  fcof1o  5998  isocnv  6020  isores2  6022  isotr  6025  isopolem  6031  isosolem  6033  f1oiso2  6036  f1ofveu  6076  suppsnopdc  6494  smoiso  6577  mapsnd  6975  mapsn  6977  f1oen2g  7046  en1  7091  enm  7123  mapen  7151  fidceq  7176  dif1en  7188  fin0  7194  fin0or  7195  ac6sfi  7207  en2eqpr  7219  fiintim  7243  isotilem  7353  supisoex  7356  supisoti  7357  ordiso2  7382  caseinl  7438  caseinr  7439  omp1eomlem  7441  ctm  7456  enomnilem  7485  enmkvlem  7508  enwomnilem  7516  pr2cv1  7548  cc3  7641  frecuzrdgg  10875  fnn0nninf  10897  fxnn0nninf  10898  0tonninf  10899  1tonninf  10900  iseqf1olemkle  10956  iseqf1olemklt  10957  iseqf1olemqcl  10958  iseqf1olemnab  10960  iseqf1olemmo  10964  iseqf1olemqk  10966  iseqf1olemjpcl  10967  iseqf1olemfvp  10969  seq3f1olemqsumkj  10970  seq3f1olemqsumk  10971  seq3f1olemqsum  10972  seq3f1olemstep  10973  seq3f1olemp  10974  seq3f1oleml  10975  seq3f1o  10976  seqf1oglem1  10978  seqf1oglem2  10979  seqf1og  10980  hashfz1  11245  omgadd  11265  hashfacen  11307  hashf1lem1  11308  leisorel  11312  zfz1isolemiso  11314  seq3coll  11317  cnrecnv  11699  sumeq2  12151  summodclem3  12173  summodclem2a  12174  fsumgcl  12179  fsum3  12180  fsumf1o  12183  fisumss  12185  fsumcl2lem  12191  fsumadd  12199  fsummulc2  12241  prodeq2  12350  prodmodclem3  12368  prodmodclem2a  12369  fprodseq  12376  fprodf1o  12381  fprodssdc  12383  fprodmul  12384  nninfctlemfo  12843  sqpweven  12981  2sqpwodd  12982  phimullem  13033  eulerthlem1  13035  eulerthlemrprm  13037  eulerthlema  13038  eulerthlemh  13039  eulerthlemth  13040  ballotfilemsima  13318  ennnfonelemjn  13352  ennnfonelemp1  13356  ennnfonelemhdmp1  13359  ennnfonelemss  13360  ennnfonelemkh  13362  ennnfonelemhf1o  13363  ennnfonelemex  13364  ennnfonelemnn0  13372  ennnfonelemim  13374  ctinfomlemom  13377  ctiunctlemudc  13387  ctiunctlemfo  13389  ssnnctlemct  13396  idmhm  13836  mhmf1o  13837  idghm  14122  ghmf1o  14138  gzsumreidx  14232  gzsumshift  14240  gsumvalfi  14243  gsump1  14248  gsumf1ofi  14251  gsummhmfi  14265  gsumressfi  14268  gsumcom2fi  14276  psrass1filem  15182  psrnegcl  15198  psrlinv  15199  ssidcn  15448  txhmeo  15557  dvid  15933  dvidre  15935  dvexp  15949  dfrelog  16101  relogcl  16103  uspgriedgedg  16637  012of  17240  2o01f  17241  iswomninnlem  17318