Theorem f1of 5461

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

Syntax hints:   → wi 4  ⟶wf 5212  –1-1→wf1 5213  –1-1-onto→wf1o 5215

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 5221  df-f1o 5223

This theorem is referenced by:  f1ofn  5462  f1oabexg  5473  f1ompt  5667  f1oresrab  5681  fsn  5688  fsnunf  5716  f1ocnvfv1  5777  f1ocnvfv2  5778  f1ocnvdm  5781  fcof1o  5789  isocnv  5811  isores2  5813  isotr  5816  isopolem  5822  isosolem  5824  f1oiso2  5827  f1ofveu  5862  smoiso  6302  mapsn  6689  f1oen2g  6754  en1  6798  enm  6819  mapen  6845  fidceq  6868  dif1en  6878  fin0  6884  fin0or  6885  ac6sfi  6897  en2eqpr  6906  fiintim  6927  isotilem  7004  supisoex  7007  supisoti  7008  ordiso2  7033  caseinl  7089  caseinr  7090  omp1eomlem  7092  ctm  7107  enomnilem  7135  enmkvlem  7158  enwomnilem  7166  cc3  7266  frecuzrdgg  10415  fnn0nninf  10436  fxnn0nninf  10437  0tonninf  10438  1tonninf  10439  iseqf1olemkle  10483  iseqf1olemklt  10484  iseqf1olemqcl  10485  iseqf1olemnab  10487  iseqf1olemmo  10491  iseqf1olemqk  10493  iseqf1olemjpcl  10494  iseqf1olemfvp  10496  seq3f1olemqsumkj  10497  seq3f1olemqsumk  10498  seq3f1olemqsum  10499  seq3f1olemstep  10500  seq3f1olemp  10501  seq3f1oleml  10502  seq3f1o  10503  hashfz1  10762  omgadd  10781  hashfacen  10815  leisorel  10816  zfz1isolemiso  10818  seq3coll  10821  cnrecnv  10918  sumeq2  11366  summodclem3  11387  summodclem2a  11388  fsumgcl  11393  fsum3  11394  fsumf1o  11397  fisumss  11399  fsumcl2lem  11405  fsumadd  11413  fsummulc2  11455  prodeq2  11564  prodmodclem3  11582  prodmodclem2a  11583  fprodseq  11590  fprodf1o  11595  fprodssdc  11597  fprodmul  11598  sqpweven  12174  2sqpwodd  12175  phimullem  12224  eulerthlem1  12226  eulerthlemrprm  12228  eulerthlema  12229  eulerthlemh  12230  eulerthlemth  12231  ennnfonelemjn  12402  ennnfonelemp1  12406  ennnfonelemhdmp1  12409  ennnfonelemss  12410  ennnfonelemkh  12412  ennnfonelemhf1o  12413  ennnfonelemex  12414  ennnfonelemnn0  12422  ennnfonelemim  12424  ctinfomlemom  12427  ctiunctlemudc  12437  ctiunctlemfo  12439  ssnnctlemct  12446  idmhm  12859  mhmf1o  12860  ssidcn  13680  txhmeo  13789  dvid  14132  dvexp  14145  dfrelog  14251  relogcl  14253  012of  14715  2o01f  14716  iswomninnlem  14767