Theorem f1of 5578

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

Syntax hints:   → wi 4  ⟶wf 5318  –1-1→wf1 5319  –1-1-onto→wf1o 5321

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 5327  df-f1o 5329

This theorem is referenced by:  f1ofn  5579  f1oabexg  5590  f1ompt  5792  f1oresrab  5806  fsn  5813  fsnunf  5847  f1ocnvfv1  5911  f1ocnvfv2  5912  f1ocnvdm  5915  fcof1o  5923  isocnv  5945  isores2  5947  isotr  5950  isopolem  5956  isosolem  5958  f1oiso2  5961  f1ofveu  5999  smoiso  6461  mapsn  6852  f1oen2g  6921  en1  6966  enm  6997  mapen  7025  fidceq  7049  dif1en  7059  fin0  7065  fin0or  7066  ac6sfi  7078  en2eqpr  7090  fiintim  7114  isotilem  7194  supisoex  7197  supisoti  7198  ordiso2  7223  caseinl  7279  caseinr  7280  omp1eomlem  7282  ctm  7297  enomnilem  7326  enmkvlem  7349  enwomnilem  7357  pr2cv1  7389  cc3  7475  frecuzrdgg  10666  fnn0nninf  10688  fxnn0nninf  10689  0tonninf  10690  1tonninf  10691  iseqf1olemkle  10747  iseqf1olemklt  10748  iseqf1olemqcl  10749  iseqf1olemnab  10751  iseqf1olemmo  10755  iseqf1olemqk  10757  iseqf1olemjpcl  10758  iseqf1olemfvp  10760  seq3f1olemqsumkj  10761  seq3f1olemqsumk  10762  seq3f1olemqsum  10763  seq3f1olemstep  10764  seq3f1olemp  10765  seq3f1oleml  10766  seq3f1o  10767  seqf1oglem1  10769  seqf1oglem2  10770  seqf1og  10771  hashfz1  11033  omgadd  11052  hashfacen  11087  leisorel  11088  zfz1isolemiso  11090  seq3coll  11093  cnrecnv  11458  sumeq2  11907  summodclem3  11928  summodclem2a  11929  fsumgcl  11934  fsum3  11935  fsumf1o  11938  fisumss  11940  fsumcl2lem  11946  fsumadd  11954  fsummulc2  11996  prodeq2  12105  prodmodclem3  12123  prodmodclem2a  12124  fprodseq  12131  fprodf1o  12136  fprodssdc  12138  fprodmul  12139  nninfctlemfo  12598  sqpweven  12734  2sqpwodd  12735  phimullem  12784  eulerthlem1  12786  eulerthlemrprm  12788  eulerthlema  12789  eulerthlemh  12790  eulerthlemth  12791  ennnfonelemjn  13010  ennnfonelemp1  13014  ennnfonelemhdmp1  13017  ennnfonelemss  13018  ennnfonelemkh  13020  ennnfonelemhf1o  13021  ennnfonelemex  13022  ennnfonelemnn0  13030  ennnfonelemim  13032  ctinfomlemom  13035  ctiunctlemudc  13045  ctiunctlemfo  13047  ssnnctlemct  13054  idmhm  13539  mhmf1o  13540  idghm  13833  ghmf1o  13849  gsumfzreidx  13911  psrnegcl  14684  psrlinv  14685  ssidcn  14921  txhmeo  15030  dvid  15406  dvidre  15408  dvexp  15422  dfrelog  15571  relogcl  15573  uspgriedgedg  16014  012of  16502  2o01f  16503  iswomninnlem  16563