Theorem f1of 5501

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

Syntax hints:   → wi 4  ⟶wf 5251  –1-1→wf1 5252  –1-1-onto→wf1o 5254

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 5260  df-f1o 5262

This theorem is referenced by:  f1ofn  5502  f1oabexg  5513  f1ompt  5710  f1oresrab  5724  fsn  5731  fsnunf  5759  f1ocnvfv1  5821  f1ocnvfv2  5822  f1ocnvdm  5825  fcof1o  5833  isocnv  5855  isores2  5857  isotr  5860  isopolem  5866  isosolem  5868  f1oiso2  5871  f1ofveu  5907  smoiso  6357  mapsn  6746  f1oen2g  6811  en1  6855  enm  6876  mapen  6904  fidceq  6927  dif1en  6937  fin0  6943  fin0or  6944  ac6sfi  6956  en2eqpr  6965  fiintim  6987  isotilem  7067  supisoex  7070  supisoti  7071  ordiso2  7096  caseinl  7152  caseinr  7153  omp1eomlem  7155  ctm  7170  enomnilem  7199  enmkvlem  7222  enwomnilem  7230  cc3  7330  frecuzrdgg  10490  fnn0nninf  10512  fxnn0nninf  10513  0tonninf  10514  1tonninf  10515  iseqf1olemkle  10571  iseqf1olemklt  10572  iseqf1olemqcl  10573  iseqf1olemnab  10575  iseqf1olemmo  10579  iseqf1olemqk  10581  iseqf1olemjpcl  10582  iseqf1olemfvp  10584  seq3f1olemqsumkj  10585  seq3f1olemqsumk  10586  seq3f1olemqsum  10587  seq3f1olemstep  10588  seq3f1olemp  10589  seq3f1oleml  10590  seq3f1o  10591  seqf1oglem1  10593  seqf1oglem2  10594  seqf1og  10595  hashfz1  10857  omgadd  10876  hashfacen  10910  leisorel  10911  zfz1isolemiso  10913  seq3coll  10916  cnrecnv  11057  sumeq2  11505  summodclem3  11526  summodclem2a  11527  fsumgcl  11532  fsum3  11533  fsumf1o  11536  fisumss  11538  fsumcl2lem  11544  fsumadd  11552  fsummulc2  11594  prodeq2  11703  prodmodclem3  11721  prodmodclem2a  11722  fprodseq  11729  fprodf1o  11734  fprodssdc  11736  fprodmul  11737  nninfctlemfo  12180  sqpweven  12316  2sqpwodd  12317  phimullem  12366  eulerthlem1  12368  eulerthlemrprm  12370  eulerthlema  12371  eulerthlemh  12372  eulerthlemth  12373  ennnfonelemjn  12562  ennnfonelemp1  12566  ennnfonelemhdmp1  12569  ennnfonelemss  12570  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemex  12574  ennnfonelemnn0  12582  ennnfonelemim  12584  ctinfomlemom  12587  ctiunctlemudc  12597  ctiunctlemfo  12599  ssnnctlemct  12606  idmhm  13044  mhmf1o  13045  idghm  13332  ghmf1o  13348  gsumfzreidx  13410  ssidcn  14389  txhmeo  14498  dvid  14874  dvidre  14876  dvexp  14890  dfrelog  15036  relogcl  15038  012of  15556  2o01f  15557  iswomninnlem  15609