Theorem f1of 5504

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

Syntax hints:   → wi 4  ⟶wf 5254  –1-1→wf1 5255  –1-1-onto→wf1o 5257

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 5263  df-f1o 5265

This theorem is referenced by:  f1ofn  5505  f1oabexg  5516  f1ompt  5713  f1oresrab  5727  fsn  5734  fsnunf  5762  f1ocnvfv1  5824  f1ocnvfv2  5825  f1ocnvdm  5828  fcof1o  5836  isocnv  5858  isores2  5860  isotr  5863  isopolem  5869  isosolem  5871  f1oiso2  5874  f1ofveu  5910  smoiso  6360  mapsn  6749  f1oen2g  6814  en1  6858  enm  6879  mapen  6907  fidceq  6930  dif1en  6940  fin0  6946  fin0or  6947  ac6sfi  6959  en2eqpr  6968  fiintim  6992  isotilem  7072  supisoex  7075  supisoti  7076  ordiso2  7101  caseinl  7157  caseinr  7158  omp1eomlem  7160  ctm  7175  enomnilem  7204  enmkvlem  7227  enwomnilem  7235  cc3  7335  frecuzrdgg  10508  fnn0nninf  10530  fxnn0nninf  10531  0tonninf  10532  1tonninf  10533  iseqf1olemkle  10589  iseqf1olemklt  10590  iseqf1olemqcl  10591  iseqf1olemnab  10593  iseqf1olemmo  10597  iseqf1olemqk  10599  iseqf1olemjpcl  10600  iseqf1olemfvp  10602  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seq3f1olemqsum  10605  seq3f1olemstep  10606  seq3f1olemp  10607  seq3f1oleml  10608  seq3f1o  10609  seqf1oglem1  10611  seqf1oglem2  10612  seqf1og  10613  hashfz1  10875  omgadd  10894  hashfacen  10928  leisorel  10929  zfz1isolemiso  10931  seq3coll  10934  cnrecnv  11075  sumeq2  11524  summodclem3  11545  summodclem2a  11546  fsumgcl  11551  fsum3  11552  fsumf1o  11555  fisumss  11557  fsumcl2lem  11563  fsumadd  11571  fsummulc2  11613  prodeq2  11722  prodmodclem3  11740  prodmodclem2a  11741  fprodseq  11748  fprodf1o  11753  fprodssdc  11755  fprodmul  11756  nninfctlemfo  12207  sqpweven  12343  2sqpwodd  12344  phimullem  12393  eulerthlem1  12395  eulerthlemrprm  12397  eulerthlema  12398  eulerthlemh  12399  eulerthlemth  12400  ennnfonelemjn  12619  ennnfonelemp1  12623  ennnfonelemhdmp1  12626  ennnfonelemss  12627  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemex  12631  ennnfonelemnn0  12639  ennnfonelemim  12641  ctinfomlemom  12644  ctiunctlemudc  12654  ctiunctlemfo  12656  ssnnctlemct  12663  idmhm  13101  mhmf1o  13102  idghm  13389  ghmf1o  13405  gsumfzreidx  13467  ssidcn  14446  txhmeo  14555  dvid  14931  dvidre  14933  dvexp  14947  dfrelog  15096  relogcl  15098  012of  15640  2o01f  15641  iswomninnlem  15693