Theorem f1of 5431

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

Syntax hints:   → wi 4  ⟶wf 5183  –1-1→wf1 5184  –1-1-onto→wf1o 5186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-f1 5192  df-f1o 5194

This theorem is referenced by:  f1ofn  5432  f1oabexg  5443  f1ompt  5635  f1oresrab  5649  fsn  5656  fsnunf  5684  f1ocnvfv1  5744  f1ocnvfv2  5745  f1ocnvdm  5748  fcof1o  5756  isocnv  5778  isores2  5780  isotr  5783  isopolem  5789  isosolem  5791  f1oiso2  5794  f1ofveu  5829  smoiso  6266  mapsn  6652  f1oen2g  6717  en1  6761  enm  6782  mapen  6808  fidceq  6831  dif1en  6841  fin0  6847  fin0or  6848  ac6sfi  6860  en2eqpr  6869  fiintim  6890  isotilem  6967  supisoex  6970  supisoti  6971  ordiso2  6996  caseinl  7052  caseinr  7053  omp1eomlem  7055  ctm  7070  enomnilem  7098  enmkvlem  7121  enwomnilem  7129  cc3  7205  frecuzrdgg  10347  fnn0nninf  10368  fxnn0nninf  10369  0tonninf  10370  1tonninf  10371  iseqf1olemkle  10415  iseqf1olemklt  10416  iseqf1olemqcl  10417  iseqf1olemnab  10419  iseqf1olemmo  10423  iseqf1olemqk  10425  iseqf1olemjpcl  10426  iseqf1olemfvp  10428  seq3f1olemqsumkj  10429  seq3f1olemqsumk  10430  seq3f1olemqsum  10431  seq3f1olemstep  10432  seq3f1olemp  10433  seq3f1oleml  10434  seq3f1o  10435  hashfz1  10692  omgadd  10711  hashfacen  10745  leisorel  10746  zfz1isolemiso  10748  seq3coll  10751  cnrecnv  10848  sumeq2  11296  summodclem3  11317  summodclem2a  11318  fsumgcl  11323  fsum3  11324  fsumf1o  11327  fisumss  11329  fsumcl2lem  11335  fsumadd  11343  fsummulc2  11385  prodeq2  11494  prodmodclem3  11512  prodmodclem2a  11513  fprodseq  11520  fprodf1o  11525  fprodssdc  11527  fprodmul  11528  sqpweven  12103  2sqpwodd  12104  phimullem  12153  eulerthlem1  12155  eulerthlemrprm  12157  eulerthlema  12158  eulerthlemh  12159  eulerthlemth  12160  ennnfonelemjn  12331  ennnfonelemp1  12335  ennnfonelemhdmp1  12338  ennnfonelemss  12339  ennnfonelemkh  12341  ennnfonelemhf1o  12342  ennnfonelemex  12343  ennnfonelemnn0  12351  ennnfonelemim  12353  ctinfomlemom  12356  ctiunctlemudc  12366  ctiunctlemfo  12368  ssnnctlemct  12375  ssidcn  12810  txhmeo  12919  dvid  13262  dvexp  13275  dfrelog  13381  relogcl  13383  012of  13835  2o01f  13836  iswomninnlem  13888