Theorem f1of 5613

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

Syntax hints:   → wi 4  ⟶wf 5347  –1-1→wf1 5348  –1-1-onto→wf1o 5350

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 5356  df-f1o 5358

This theorem is referenced by:  f1ofn  5614  f1oabexg  5625  f1ompt  5827  f1oresrab  5841  fsn  5848  fsnunf  5883  f1ocnvfv1  5949  f1ocnvfv2  5950  f1ocnvdm  5953  fcof1o  5961  isocnv  5983  isores2  5985  isotr  5988  isopolem  5994  isosolem  5996  f1oiso2  5999  f1ofveu  6037  suppsnopdc  6449  smoiso  6532  mapsnd  6922  mapsn  6924  f1oen2g  6993  en1  7038  enm  7070  mapen  7098  fidceq  7123  dif1en  7135  fin0  7141  fin0or  7142  ac6sfi  7154  en2eqpr  7166  fiintim  7190  isotilem  7296  supisoex  7299  supisoti  7300  ordiso2  7325  caseinl  7381  caseinr  7382  omp1eomlem  7384  ctm  7399  enomnilem  7428  enmkvlem  7451  enwomnilem  7459  pr2cv1  7491  cc3  7578  frecuzrdgg  10774  fnn0nninf  10796  fxnn0nninf  10797  0tonninf  10798  1tonninf  10799  iseqf1olemkle  10855  iseqf1olemklt  10856  iseqf1olemqcl  10857  iseqf1olemnab  10859  iseqf1olemmo  10863  iseqf1olemqk  10865  iseqf1olemjpcl  10866  iseqf1olemfvp  10868  seq3f1olemqsumkj  10869  seq3f1olemqsumk  10870  seq3f1olemqsum  10871  seq3f1olemstep  10872  seq3f1olemp  10873  seq3f1oleml  10874  seq3f1o  10875  seqf1oglem1  10877  seqf1oglem2  10878  seqf1og  10879  hashfz1  11141  omgadd  11161  hashfacen  11201  leisorel  11202  zfz1isolemiso  11204  seq3coll  11207  cnrecnv  11588  sumeq2  12037  summodclem3  12059  summodclem2a  12060  fsumgcl  12065  fsum3  12066  fsumf1o  12069  fisumss  12071  fsumcl2lem  12077  fsumadd  12085  fsummulc2  12127  prodeq2  12236  prodmodclem3  12254  prodmodclem2a  12255  fprodseq  12262  fprodf1o  12267  fprodssdc  12269  fprodmul  12270  nninfctlemfo  12729  sqpweven  12865  2sqpwodd  12866  phimullem  12915  eulerthlem1  12917  eulerthlemrprm  12919  eulerthlema  12920  eulerthlemh  12921  eulerthlemth  12922  ennnfonelemjn  13142  ennnfonelemp1  13146  ennnfonelemhdmp1  13149  ennnfonelemss  13150  ennnfonelemkh  13152  ennnfonelemhf1o  13153  ennnfonelemex  13154  ennnfonelemnn0  13162  ennnfonelemim  13164  ctinfomlemom  13167  ctiunctlemudc  13177  ctiunctlemfo  13179  ssnnctlemct  13186  idmhm  13671  mhmf1o  13672  idghm  13965  ghmf1o  13981  gsumfzreidx  14043  psrnegcl  14825  psrlinv  14826  ssidcn  15062  txhmeo  15171  dvid  15547  dvidre  15549  dvexp  15563  dfrelog  15712  relogcl  15714  uspgriedgedg  16161  012of  16754  2o01f  16755  iswomninnlem  16821  gfsumval  16848  gsumgfsumlem  16851  gfsump1  16854