Theorem f1of 5619

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

Syntax hints:   → wi 4  ⟶wf 5353  –1-1→wf1 5354  –1-1-onto→wf1o 5356

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 5362  df-f1o 5364

This theorem is referenced by:  f1ofn  5620  f1oabexg  5631  f1ompt  5833  f1oresrab  5847  fsn  5854  fsnunf  5889  f1ocnvfv1  5956  f1ocnvfv2  5957  f1ocnvdm  5960  fcof1o  5968  isocnv  5990  isores2  5992  isotr  5995  isopolem  6001  isosolem  6003  f1oiso2  6006  f1ofveu  6046  suppsnopdc  6463  smoiso  6546  mapsnd  6936  mapsn  6938  f1oen2g  7007  en1  7052  enm  7084  mapen  7112  fidceq  7137  dif1en  7149  fin0  7155  fin0or  7156  ac6sfi  7168  en2eqpr  7180  fiintim  7204  isotilem  7310  supisoex  7313  supisoti  7314  ordiso2  7339  caseinl  7395  caseinr  7396  omp1eomlem  7398  ctm  7413  enomnilem  7442  enmkvlem  7465  enwomnilem  7473  pr2cv1  7505  cc3  7598  frecuzrdgg  10805  fnn0nninf  10827  fxnn0nninf  10828  0tonninf  10829  1tonninf  10830  iseqf1olemkle  10886  iseqf1olemklt  10887  iseqf1olemqcl  10888  iseqf1olemnab  10890  iseqf1olemmo  10894  iseqf1olemqk  10896  iseqf1olemjpcl  10897  iseqf1olemfvp  10899  seq3f1olemqsumkj  10900  seq3f1olemqsumk  10901  seq3f1olemqsum  10902  seq3f1olemstep  10903  seq3f1olemp  10904  seq3f1oleml  10905  seq3f1o  10906  seqf1oglem1  10908  seqf1oglem2  10909  seqf1og  10910  hashfz1  11174  omgadd  11194  hashfacen  11236  leisorel  11237  zfz1isolemiso  11239  seq3coll  11242  cnrecnv  11623  sumeq2  12072  summodclem3  12094  summodclem2a  12095  fsumgcl  12100  fsum3  12101  fsumf1o  12104  fisumss  12106  fsumcl2lem  12112  fsumadd  12120  fsummulc2  12162  prodeq2  12271  prodmodclem3  12289  prodmodclem2a  12290  fprodseq  12297  fprodf1o  12302  fprodssdc  12304  fprodmul  12305  nninfctlemfo  12764  sqpweven  12900  2sqpwodd  12901  phimullem  12950  eulerthlem1  12952  eulerthlemrprm  12954  eulerthlema  12955  eulerthlemh  12956  eulerthlemth  12957  ballotfilemsima  13206  ennnfonelemjn  13240  ennnfonelemp1  13244  ennnfonelemhdmp1  13247  ennnfonelemss  13248  ennnfonelemkh  13250  ennnfonelemhf1o  13251  ennnfonelemex  13252  ennnfonelemnn0  13260  ennnfonelemim  13262  ctinfomlemom  13265  ctiunctlemudc  13275  ctiunctlemfo  13277  ssnnctlemct  13284  idmhm  13727  mhmf1o  13728  idghm  14015  ghmf1o  14031  gsumfzreidx  14093  gfsumval  14105  gsumshift  14108  gfsump1  14111  psrnegcl  14967  psrlinv  14968  ssidcn  15204  txhmeo  15313  dvid  15689  dvidre  15691  dvexp  15705  dfrelog  15854  relogcl  15856  uspgriedgedg  16303  012of  16906  2o01f  16907  iswomninnlem  16973