Theorem f1of 5574

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

Syntax hints:   → wi 4  ⟶wf 5314  –1-1→wf1 5315  –1-1-onto→wf1o 5317

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 5323  df-f1o 5325

This theorem is referenced by:  f1ofn  5575  f1oabexg  5586  f1ompt  5788  f1oresrab  5802  fsn  5809  fsnunf  5843  f1ocnvfv1  5907  f1ocnvfv2  5908  f1ocnvdm  5911  fcof1o  5919  isocnv  5941  isores2  5943  isotr  5946  isopolem  5952  isosolem  5954  f1oiso2  5957  f1ofveu  5995  smoiso  6454  mapsn  6845  f1oen2g  6914  en1  6959  enm  6987  mapen  7015  fidceq  7039  dif1en  7049  fin0  7055  fin0or  7056  ac6sfi  7068  en2eqpr  7077  fiintim  7101  isotilem  7181  supisoex  7184  supisoti  7185  ordiso2  7210  caseinl  7266  caseinr  7267  omp1eomlem  7269  ctm  7284  enomnilem  7313  enmkvlem  7336  enwomnilem  7344  pr2cv1  7376  cc3  7462  frecuzrdgg  10646  fnn0nninf  10668  fxnn0nninf  10669  0tonninf  10670  1tonninf  10671  iseqf1olemkle  10727  iseqf1olemklt  10728  iseqf1olemqcl  10729  iseqf1olemnab  10731  iseqf1olemmo  10735  iseqf1olemqk  10737  iseqf1olemjpcl  10738  iseqf1olemfvp  10740  seq3f1olemqsumkj  10741  seq3f1olemqsumk  10742  seq3f1olemqsum  10743  seq3f1olemstep  10744  seq3f1olemp  10745  seq3f1oleml  10746  seq3f1o  10747  seqf1oglem1  10749  seqf1oglem2  10750  seqf1og  10751  hashfz1  11013  omgadd  11032  hashfacen  11066  leisorel  11067  zfz1isolemiso  11069  seq3coll  11072  cnrecnv  11429  sumeq2  11878  summodclem3  11899  summodclem2a  11900  fsumgcl  11905  fsum3  11906  fsumf1o  11909  fisumss  11911  fsumcl2lem  11917  fsumadd  11925  fsummulc2  11967  prodeq2  12076  prodmodclem3  12094  prodmodclem2a  12095  fprodseq  12102  fprodf1o  12107  fprodssdc  12109  fprodmul  12110  nninfctlemfo  12569  sqpweven  12705  2sqpwodd  12706  phimullem  12755  eulerthlem1  12757  eulerthlemrprm  12759  eulerthlema  12760  eulerthlemh  12761  eulerthlemth  12762  ennnfonelemjn  12981  ennnfonelemp1  12985  ennnfonelemhdmp1  12988  ennnfonelemss  12989  ennnfonelemkh  12991  ennnfonelemhf1o  12992  ennnfonelemex  12993  ennnfonelemnn0  13001  ennnfonelemim  13003  ctinfomlemom  13006  ctiunctlemudc  13016  ctiunctlemfo  13018  ssnnctlemct  13025  idmhm  13510  mhmf1o  13511  idghm  13804  ghmf1o  13820  gsumfzreidx  13882  psrnegcl  14655  psrlinv  14656  ssidcn  14892  txhmeo  15001  dvid  15377  dvidre  15379  dvexp  15393  dfrelog  15542  relogcl  15544  uspgriedgedg  15985  012of  16386  2o01f  16387  iswomninnlem  16447