Theorem f1of 5375

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

Syntax hints:   → wi 4  ⟶wf 5127  –1-1→wf1 5128  –1-1-onto→wf1o 5130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-f1 5136  df-f1o 5138

This theorem is referenced by:  f1ofn  5376  f1oabexg  5387  f1ompt  5579  f1oresrab  5593  fsn  5600  fsnunf  5628  f1ocnvfv1  5686  f1ocnvfv2  5687  f1ocnvdm  5690  fcof1o  5698  isocnv  5720  isores2  5722  isotr  5725  isopolem  5731  isosolem  5733  f1oiso2  5736  f1ofveu  5770  smoiso  6207  mapsn  6592  f1oen2g  6657  en1  6701  enm  6722  mapen  6748  fidceq  6771  dif1en  6781  fin0  6787  fin0or  6788  ac6sfi  6800  en2eqpr  6809  fiintim  6825  isotilem  6901  supisoex  6904  supisoti  6905  ordiso2  6928  caseinl  6984  caseinr  6985  omp1eomlem  6987  ctm  7002  enomnilem  7018  enmkvlem  7043  enwomnilem  7050  cc3  7100  frecuzrdgg  10220  fnn0nninf  10241  fxnn0nninf  10242  0tonninf  10243  1tonninf  10244  iseqf1olemkle  10288  iseqf1olemklt  10289  iseqf1olemqcl  10290  iseqf1olemnab  10292  iseqf1olemmo  10296  iseqf1olemqk  10298  iseqf1olemjpcl  10299  iseqf1olemfvp  10301  seq3f1olemqsumkj  10302  seq3f1olemqsumk  10303  seq3f1olemqsum  10304  seq3f1olemstep  10305  seq3f1olemp  10306  seq3f1oleml  10307  seq3f1o  10308  hashfz1  10561  omgadd  10580  hashfacen  10611  leisorel  10612  zfz1isolemiso  10614  seq3coll  10617  cnrecnv  10714  sumeq2  11160  summodclem3  11181  summodclem2a  11182  fsumgcl  11187  fsum3  11188  fsumf1o  11191  fisumss  11193  fsumcl2lem  11199  fsumadd  11207  fsummulc2  11249  prodeq2  11358  prodmodclem3  11376  prodmodclem2a  11377  fprodseq  11384  sqpweven  11889  2sqpwodd  11890  phimullem  11937  ennnfonelemjn  11951  ennnfonelemp1  11955  ennnfonelemhdmp1  11958  ennnfonelemss  11959  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemex  11963  ennnfonelemnn0  11971  ennnfonelemim  11973  ctinfomlemom  11976  ctiunctlemudc  11986  ctiunctlemfo  11988  ssidcn  12418  txhmeo  12527  dvid  12870  dvexp  12883  dfrelog  12989  relogcl  12991  012of  13363  2o01f  13364  iswomninnlem  13417