Theorem f1of 5529

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

Syntax hints:   → wi 4  ⟶wf 5272  –1-1→wf1 5273  –1-1-onto→wf1o 5275

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 5281  df-f1o 5283

This theorem is referenced by:  f1ofn  5530  f1oabexg  5541  f1ompt  5738  f1oresrab  5752  fsn  5759  fsnunf  5791  f1ocnvfv1  5853  f1ocnvfv2  5854  f1ocnvdm  5857  fcof1o  5865  isocnv  5887  isores2  5889  isotr  5892  isopolem  5898  isosolem  5900  f1oiso2  5903  f1ofveu  5939  smoiso  6395  mapsn  6784  f1oen2g  6853  en1  6898  enm  6922  mapen  6950  fidceq  6973  dif1en  6983  fin0  6989  fin0or  6990  ac6sfi  7002  en2eqpr  7011  fiintim  7035  isotilem  7115  supisoex  7118  supisoti  7119  ordiso2  7144  caseinl  7200  caseinr  7201  omp1eomlem  7203  ctm  7218  enomnilem  7247  enmkvlem  7270  enwomnilem  7278  cc3  7387  frecuzrdgg  10568  fnn0nninf  10590  fxnn0nninf  10591  0tonninf  10592  1tonninf  10593  iseqf1olemkle  10649  iseqf1olemklt  10650  iseqf1olemqcl  10651  iseqf1olemnab  10653  iseqf1olemmo  10657  iseqf1olemqk  10659  iseqf1olemjpcl  10660  iseqf1olemfvp  10662  seq3f1olemqsumkj  10663  seq3f1olemqsumk  10664  seq3f1olemqsum  10665  seq3f1olemstep  10666  seq3f1olemp  10667  seq3f1oleml  10668  seq3f1o  10669  seqf1oglem1  10671  seqf1oglem2  10672  seqf1og  10673  hashfz1  10935  omgadd  10954  hashfacen  10988  leisorel  10989  zfz1isolemiso  10991  seq3coll  10994  cnrecnv  11265  sumeq2  11714  summodclem3  11735  summodclem2a  11736  fsumgcl  11741  fsum3  11742  fsumf1o  11745  fisumss  11747  fsumcl2lem  11753  fsumadd  11761  fsummulc2  11803  prodeq2  11912  prodmodclem3  11930  prodmodclem2a  11931  fprodseq  11938  fprodf1o  11943  fprodssdc  11945  fprodmul  11946  nninfctlemfo  12405  sqpweven  12541  2sqpwodd  12542  phimullem  12591  eulerthlem1  12593  eulerthlemrprm  12595  eulerthlema  12596  eulerthlemh  12597  eulerthlemth  12598  ennnfonelemjn  12817  ennnfonelemp1  12821  ennnfonelemhdmp1  12824  ennnfonelemss  12825  ennnfonelemkh  12827  ennnfonelemhf1o  12828  ennnfonelemex  12829  ennnfonelemnn0  12837  ennnfonelemim  12839  ctinfomlemom  12842  ctiunctlemudc  12852  ctiunctlemfo  12854  ssnnctlemct  12861  idmhm  13345  mhmf1o  13346  idghm  13639  ghmf1o  13655  gsumfzreidx  13717  psrnegcl  14489  psrlinv  14490  ssidcn  14726  txhmeo  14835  dvid  15211  dvidre  15213  dvexp  15227  dfrelog  15376  relogcl  15378  012of  16004  2o01f  16005  iswomninnlem  16062