Theorem f1of 5473

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

Syntax hints:   → wi 4  ⟶wf 5224  –1-1→wf1 5225  –1-1-onto→wf1o 5227

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 5233  df-f1o 5235

This theorem is referenced by:  f1ofn  5474  f1oabexg  5485  f1ompt  5680  f1oresrab  5694  fsn  5701  fsnunf  5729  f1ocnvfv1  5791  f1ocnvfv2  5792  f1ocnvdm  5795  fcof1o  5803  isocnv  5825  isores2  5827  isotr  5830  isopolem  5836  isosolem  5838  f1oiso2  5841  f1ofveu  5876  smoiso  6317  mapsn  6704  f1oen2g  6769  en1  6813  enm  6834  mapen  6860  fidceq  6883  dif1en  6893  fin0  6899  fin0or  6900  ac6sfi  6912  en2eqpr  6921  fiintim  6942  isotilem  7019  supisoex  7022  supisoti  7023  ordiso2  7048  caseinl  7104  caseinr  7105  omp1eomlem  7107  ctm  7122  enomnilem  7150  enmkvlem  7173  enwomnilem  7181  cc3  7281  frecuzrdgg  10430  fnn0nninf  10451  fxnn0nninf  10452  0tonninf  10453  1tonninf  10454  iseqf1olemkle  10498  iseqf1olemklt  10499  iseqf1olemqcl  10500  iseqf1olemnab  10502  iseqf1olemmo  10506  iseqf1olemqk  10508  iseqf1olemjpcl  10509  iseqf1olemfvp  10511  seq3f1olemqsumkj  10512  seq3f1olemqsumk  10513  seq3f1olemqsum  10514  seq3f1olemstep  10515  seq3f1olemp  10516  seq3f1oleml  10517  seq3f1o  10518  hashfz1  10777  omgadd  10796  hashfacen  10830  leisorel  10831  zfz1isolemiso  10833  seq3coll  10836  cnrecnv  10933  sumeq2  11381  summodclem3  11402  summodclem2a  11403  fsumgcl  11408  fsum3  11409  fsumf1o  11412  fisumss  11414  fsumcl2lem  11420  fsumadd  11428  fsummulc2  11470  prodeq2  11579  prodmodclem3  11597  prodmodclem2a  11598  fprodseq  11605  fprodf1o  11610  fprodssdc  11612  fprodmul  11613  sqpweven  12189  2sqpwodd  12190  phimullem  12239  eulerthlem1  12241  eulerthlemrprm  12243  eulerthlema  12244  eulerthlemh  12245  eulerthlemth  12246  ennnfonelemjn  12417  ennnfonelemp1  12421  ennnfonelemhdmp1  12424  ennnfonelemss  12425  ennnfonelemkh  12427  ennnfonelemhf1o  12428  ennnfonelemex  12429  ennnfonelemnn0  12437  ennnfonelemim  12439  ctinfomlemom  12442  ctiunctlemudc  12452  ctiunctlemfo  12454  ssnnctlemct  12461  idmhm  12882  mhmf1o  12883  ssidcn  14006  txhmeo  14115  dvid  14458  dvexp  14471  dfrelog  14577  relogcl  14579  012of  15042  2o01f  15043  iswomninnlem  15094