Theorem f1of 5637

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

Syntax hints:   → wi 4  ⟶wf 5371  –1-1→wf1 5372  –1-1-onto→wf1o 5374

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 5380  df-f1o 5382

This theorem is referenced by:  f1ofn  5638  f1oabexg  5649  f1ompt  5853  f1oresrab  5867  fsn  5874  fsnunf  5909  f1ocnvfv1  5977  f1ocnvfv2  5978  f1ocnvdm  5981  fcof1o  5989  isocnv  6011  isores2  6013  isotr  6016  isopolem  6022  isosolem  6024  f1oiso2  6027  f1ofveu  6067  suppsnopdc  6484  smoiso  6567  mapsnd  6964  mapsn  6966  f1oen2g  7035  en1  7080  enm  7112  mapen  7140  fidceq  7165  dif1en  7177  fin0  7183  fin0or  7184  ac6sfi  7196  en2eqpr  7208  fiintim  7232  isotilem  7340  supisoex  7343  supisoti  7344  ordiso2  7369  caseinl  7425  caseinr  7426  omp1eomlem  7428  ctm  7443  enomnilem  7472  enmkvlem  7495  enwomnilem  7503  pr2cv1  7535  cc3  7628  frecuzrdgg  10836  fnn0nninf  10858  fxnn0nninf  10859  0tonninf  10860  1tonninf  10861  iseqf1olemkle  10917  iseqf1olemklt  10918  iseqf1olemqcl  10919  iseqf1olemnab  10921  iseqf1olemmo  10925  iseqf1olemqk  10927  iseqf1olemjpcl  10928  iseqf1olemfvp  10930  seq3f1olemqsumkj  10931  seq3f1olemqsumk  10932  seq3f1olemqsum  10933  seq3f1olemstep  10934  seq3f1olemp  10935  seq3f1oleml  10936  seq3f1o  10937  seqf1oglem1  10939  seqf1oglem2  10940  seqf1og  10941  hashfz1  11205  omgadd  11225  hashfacen  11267  hashf1lem1  11268  leisorel  11272  zfz1isolemiso  11274  seq3coll  11277  cnrecnv  11659  sumeq2  12108  summodclem3  12130  summodclem2a  12131  fsumgcl  12136  fsum3  12137  fsumf1o  12140  fisumss  12142  fsumcl2lem  12148  fsumadd  12156  fsummulc2  12198  prodeq2  12307  prodmodclem3  12325  prodmodclem2a  12326  fprodseq  12333  fprodf1o  12338  fprodssdc  12340  fprodmul  12341  nninfctlemfo  12800  sqpweven  12936  2sqpwodd  12937  phimullem  12986  eulerthlem1  12988  eulerthlemrprm  12990  eulerthlema  12991  eulerthlemh  12992  eulerthlemth  12993  ballotfilemsima  13242  ennnfonelemjn  13276  ennnfonelemp1  13280  ennnfonelemhdmp1  13283  ennnfonelemss  13284  ennnfonelemkh  13286  ennnfonelemhf1o  13287  ennnfonelemex  13288  ennnfonelemnn0  13296  ennnfonelemim  13298  ctinfomlemom  13301  ctiunctlemudc  13311  ctiunctlemfo  13313  ssnnctlemct  13320  idmhm  13759  mhmf1o  13760  idghm  14045  ghmf1o  14061  gzsumreidx  14124  gzsumshift  14132  gsumvalfi  14135  gsump1  14140  gsumf1ofi  14143  gsummhmfi  14147  gsumressfi  14150  psrnegcl  15057  psrlinv  15058  ssidcn  15294  txhmeo  15403  dvid  15779  dvidre  15781  dvexp  15795  dfrelog  15944  relogcl  15946  uspgriedgedg  16403  012of  17006  2o01f  17007  iswomninnlem  17073