Theorem f1of 5462

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

Syntax hints:   → wi 4  ⟶wf 5213  –1-1→wf1 5214  –1-1-onto→wf1o 5216

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 5222  df-f1o 5224

This theorem is referenced by:  f1ofn  5463  f1oabexg  5474  f1ompt  5668  f1oresrab  5682  fsn  5689  fsnunf  5717  f1ocnvfv1  5778  f1ocnvfv2  5779  f1ocnvdm  5782  fcof1o  5790  isocnv  5812  isores2  5814  isotr  5817  isopolem  5823  isosolem  5825  f1oiso2  5828  f1ofveu  5863  smoiso  6303  mapsn  6690  f1oen2g  6755  en1  6799  enm  6820  mapen  6846  fidceq  6869  dif1en  6879  fin0  6885  fin0or  6886  ac6sfi  6898  en2eqpr  6907  fiintim  6928  isotilem  7005  supisoex  7008  supisoti  7009  ordiso2  7034  caseinl  7090  caseinr  7091  omp1eomlem  7093  ctm  7108  enomnilem  7136  enmkvlem  7159  enwomnilem  7167  cc3  7267  frecuzrdgg  10416  fnn0nninf  10437  fxnn0nninf  10438  0tonninf  10439  1tonninf  10440  iseqf1olemkle  10484  iseqf1olemklt  10485  iseqf1olemqcl  10486  iseqf1olemnab  10488  iseqf1olemmo  10492  iseqf1olemqk  10494  iseqf1olemjpcl  10495  iseqf1olemfvp  10497  seq3f1olemqsumkj  10498  seq3f1olemqsumk  10499  seq3f1olemqsum  10500  seq3f1olemstep  10501  seq3f1olemp  10502  seq3f1oleml  10503  seq3f1o  10504  hashfz1  10763  omgadd  10782  hashfacen  10816  leisorel  10817  zfz1isolemiso  10819  seq3coll  10822  cnrecnv  10919  sumeq2  11367  summodclem3  11388  summodclem2a  11389  fsumgcl  11394  fsum3  11395  fsumf1o  11398  fisumss  11400  fsumcl2lem  11406  fsumadd  11414  fsummulc2  11456  prodeq2  11565  prodmodclem3  11583  prodmodclem2a  11584  fprodseq  11591  fprodf1o  11596  fprodssdc  11598  fprodmul  11599  sqpweven  12175  2sqpwodd  12176  phimullem  12225  eulerthlem1  12227  eulerthlemrprm  12229  eulerthlema  12230  eulerthlemh  12231  eulerthlemth  12232  ennnfonelemjn  12403  ennnfonelemp1  12407  ennnfonelemhdmp1  12410  ennnfonelemss  12411  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemex  12415  ennnfonelemnn0  12423  ennnfonelemim  12425  ctinfomlemom  12428  ctiunctlemudc  12438  ctiunctlemfo  12440  ssnnctlemct  12447  idmhm  12860  mhmf1o  12861  ssidcn  13713  txhmeo  13822  dvid  14165  dvexp  14178  dfrelog  14284  relogcl  14286  012of  14748  2o01f  14749  iswomninnlem  14800