Theorem f1of 5616

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

Syntax hints:   → wi 4  ⟶wf 5350  –1-1→wf1 5351  –1-1-onto→wf1o 5353

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 5359  df-f1o 5361

This theorem is referenced by:  f1ofn  5617  f1oabexg  5628  f1ompt  5830  f1oresrab  5844  fsn  5851  fsnunf  5886  f1ocnvfv1  5952  f1ocnvfv2  5953  f1ocnvdm  5956  fcof1o  5964  isocnv  5986  isores2  5988  isotr  5991  isopolem  5997  isosolem  5999  f1oiso2  6002  f1ofveu  6040  suppsnopdc  6452  smoiso  6535  mapsnd  6925  mapsn  6927  f1oen2g  6996  en1  7041  enm  7073  mapen  7101  fidceq  7126  dif1en  7138  fin0  7144  fin0or  7145  ac6sfi  7157  en2eqpr  7169  fiintim  7193  isotilem  7299  supisoex  7302  supisoti  7303  ordiso2  7328  caseinl  7384  caseinr  7385  omp1eomlem  7387  ctm  7402  enomnilem  7431  enmkvlem  7454  enwomnilem  7462  pr2cv1  7494  cc3  7587  frecuzrdgg  10785  fnn0nninf  10807  fxnn0nninf  10808  0tonninf  10809  1tonninf  10810  iseqf1olemkle  10866  iseqf1olemklt  10867  iseqf1olemqcl  10868  iseqf1olemnab  10870  iseqf1olemmo  10874  iseqf1olemqk  10876  iseqf1olemjpcl  10877  iseqf1olemfvp  10879  seq3f1olemqsumkj  10880  seq3f1olemqsumk  10881  seq3f1olemqsum  10882  seq3f1olemstep  10883  seq3f1olemp  10884  seq3f1oleml  10885  seq3f1o  10886  seqf1oglem1  10888  seqf1oglem2  10889  seqf1og  10890  hashfz1  11154  omgadd  11174  hashfacen  11216  leisorel  11217  zfz1isolemiso  11219  seq3coll  11222  cnrecnv  11603  sumeq2  12052  summodclem3  12074  summodclem2a  12075  fsumgcl  12080  fsum3  12081  fsumf1o  12084  fisumss  12086  fsumcl2lem  12092  fsumadd  12100  fsummulc2  12142  prodeq2  12251  prodmodclem3  12269  prodmodclem2a  12270  fprodseq  12277  fprodf1o  12282  fprodssdc  12284  fprodmul  12285  nninfctlemfo  12744  sqpweven  12880  2sqpwodd  12881  phimullem  12930  eulerthlem1  12932  eulerthlemrprm  12934  eulerthlema  12935  eulerthlemh  12936  eulerthlemth  12937  ennnfonelemjn  13174  ennnfonelemp1  13178  ennnfonelemhdmp1  13181  ennnfonelemss  13182  ennnfonelemkh  13184  ennnfonelemhf1o  13185  ennnfonelemex  13186  ennnfonelemnn0  13194  ennnfonelemim  13196  ctinfomlemom  13199  ctiunctlemudc  13209  ctiunctlemfo  13211  ssnnctlemct  13218  idmhm  13703  mhmf1o  13704  idghm  13997  ghmf1o  14013  gsumfzreidx  14075  psrnegcl  14887  psrlinv  14888  ssidcn  15124  txhmeo  15233  dvid  15609  dvidre  15611  dvexp  15625  dfrelog  15774  relogcl  15776  uspgriedgedg  16223  012of  16816  2o01f  16817  iswomninnlem  16883  gfsumval  16911  gsumgfsumlem  16914  gfsump1  16917