Theorem f1of 5583

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

Syntax hints:   → wi 4  ⟶wf 5322  –1-1→wf1 5323  –1-1-onto→wf1o 5325

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 5331  df-f1o 5333

This theorem is referenced by:  f1ofn  5584  f1oabexg  5595  f1ompt  5798  f1oresrab  5812  fsn  5819  fsnunf  5854  f1ocnvfv1  5918  f1ocnvfv2  5919  f1ocnvdm  5922  fcof1o  5930  isocnv  5952  isores2  5954  isotr  5957  isopolem  5963  isosolem  5965  f1oiso2  5968  f1ofveu  6006  smoiso  6468  mapsn  6859  f1oen2g  6928  en1  6973  enm  7004  mapen  7032  fidceq  7056  dif1en  7068  fin0  7074  fin0or  7075  ac6sfi  7087  en2eqpr  7099  fiintim  7123  isotilem  7205  supisoex  7208  supisoti  7209  ordiso2  7234  caseinl  7290  caseinr  7291  omp1eomlem  7293  ctm  7308  enomnilem  7337  enmkvlem  7360  enwomnilem  7368  pr2cv1  7400  cc3  7487  frecuzrdgg  10679  fnn0nninf  10701  fxnn0nninf  10702  0tonninf  10703  1tonninf  10704  iseqf1olemkle  10760  iseqf1olemklt  10761  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemmo  10768  iseqf1olemqk  10770  iseqf1olemjpcl  10771  iseqf1olemfvp  10773  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1olemstep  10777  seq3f1olemp  10778  seq3f1oleml  10779  seq3f1o  10780  seqf1oglem1  10782  seqf1oglem2  10783  seqf1og  10784  hashfz1  11046  omgadd  11066  hashfacen  11101  leisorel  11102  zfz1isolemiso  11104  seq3coll  11107  cnrecnv  11472  sumeq2  11921  summodclem3  11943  summodclem2a  11944  fsumgcl  11949  fsum3  11950  fsumf1o  11953  fisumss  11955  fsumcl2lem  11961  fsumadd  11969  fsummulc2  12011  prodeq2  12120  prodmodclem3  12138  prodmodclem2a  12139  fprodseq  12146  fprodf1o  12151  fprodssdc  12153  fprodmul  12154  nninfctlemfo  12613  sqpweven  12749  2sqpwodd  12750  phimullem  12799  eulerthlem1  12801  eulerthlemrprm  12803  eulerthlema  12804  eulerthlemh  12805  eulerthlemth  12806  ennnfonelemjn  13025  ennnfonelemp1  13029  ennnfonelemhdmp1  13032  ennnfonelemss  13033  ennnfonelemkh  13035  ennnfonelemhf1o  13036  ennnfonelemex  13037  ennnfonelemnn0  13045  ennnfonelemim  13047  ctinfomlemom  13050  ctiunctlemudc  13060  ctiunctlemfo  13062  ssnnctlemct  13069  idmhm  13554  mhmf1o  13555  idghm  13848  ghmf1o  13864  gsumfzreidx  13926  psrnegcl  14700  psrlinv  14701  ssidcn  14937  txhmeo  15046  dvid  15422  dvidre  15424  dvexp  15438  dfrelog  15587  relogcl  15589  uspgriedgedg  16033  012of  16613  2o01f  16614  iswomninnlem  16674  gfsumval  16701  gsumgfsumlem  16704  gfsump1  16707