Theorem f1of1 6817

Description: A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1of1	⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)

Proof of Theorem f1of1

Step	Hyp	Ref	Expression
1		df-f1o 6540	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2	1	simplbi 502	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)

This proof depends on syntax axioms:   → wi 4  –1-1→wf1 6530  –onto→wfo 6531  –1-1-onto→wf1o 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f1o 6540

This theorem is used by:  f1of  6818  f1un  6839  f1sng  6862  f1oresrab  7122  f1ounsn  7274  f1prex  7286  f1ocnvfvrneq  7288  f1ocoima  7305  isof1oidb  7326  isores3  7337  isoini2  7341  isosolem  7349  f1oiso  7353  weniso  7358  weisoeq  7359  f1opw2  7670  f1ovv  7956  mptcnfimad  7984  tposf12  8250  oacomf1olem  8552  enssdom  8983  enssdomOLD  8984  domssex2  9136  mapen  9140  ssenen  9150  ssfiALT  9169  ssdomfi  9191  ssdomfi2  9192  sucdom2  9198  phplem2  9200  php3  9204  snnen2o  9216  1sdom2dom  9225  f1finf1o  9244  domunfican  9292  fiint  9297  f1opwfi  9324  mapfienlem1  9376  mapfienlem2  9377  mapfien  9379  marypha1lem  9404  ordtypelem10  9500  oiexg  9508  unxpwdom2  9561  wemapwe  9677  inlresf1  9921  inrresf1  9923  isinffi  9998  infxpenlem  10017  fseqenlem1  10028  dfac12lem2  10148  dfac12r  10150  ackbij2  10245  cff1  10261  infpssrlem4  10309  fin4en1  10312  enfin2i  10324  fin23lem28  10343  isf32lem7  10362  isf34lem3  10378  enfin1ai  10387  canthnum  10659  canthwe  10661  canthp1lem2  10663  pwfseqlem4  10672  pwfseqlem5  10673  tskuni  10793  grothomex  10839  negfi  12189  seqf1olem1  14106  hashfacen  14520  hashf1lem1  14521  s1f1  14677  fsumss  15812  ackbijnn  15918  fprodss  16036  bitsinv2  16534  bitsf1  16537  sadasslem  16561  sadeq  16563  phimullem  16871  eulerthlem2  16874  unbenlem  17001  f1ocpbllem  17611  f1ovscpbl  17613  xpsff1o2  17656  xpsmnd  18885  injsubmefmnd  19007  xpsgrp  19183  eqgen  19307  conjsubgen  19379  subggim  19394  gim0to0  19397  gicsubgen  19407  symgfvne  19509  symgextf1  19549  symgfixelsi  19563  f1omvdmvd  19571  f1omvdconj  19574  pmtrfconj  19594  odngen  19705  sylow1lem2  19727  sylow2blem1  19748  gsumzres  20037  gsumzcl2  20038  gsumzf1o  20040  gsumzaddlem  20049  gsumconst  20062  gsumzmhm  20065  gsumzoppg  20072  dprdf1o  20162  xpsrngd  20315  xpsringd  20474  gsumfsum  21648  zntoslem  21770  znunithash  21778  iporthcom  21849  lindfres  22037  islindf3  22040  lindsmm  22042  lmimlbs  22050  lbslcic  22055  coe1sfi  22439  coe1mul2lem2  22495  resthauslem  23589  sshauslem  23598  basqtop  23938  tgqtop  23939  hmeoopn  23993  hmeocld  23994  hmeontr  23996  hmeoimaf1o  23997  haushmphlem  24014  tsmsf1o  24372  imasdsf1olem  24600  imasf1oxmet  24602  imasf1oxms  24716  ovoliunlem1  25731  dyadmbl  25829  vitalilem3  25839  dvcnvlem  26204  dvne0f1  26240  dvcnvrelem2  26246  logf1o2  26888  dvlog  26889  wilthlem3  27307  oldfib  28643  istrkg2ld  28802  f1otrg  29328  axcontlem10  29431  usgrf1  29633  usgrexmplef  29720  usgrres1  29776  edgusgrnbfin  29834  usgrexilem  29901  sizusglecusglem1  29922  uspgr2wlkeq  30106  trlres  30163  usgr2trlncl  30226  clwlkclwwlk  30473  adjbd1o  32567  padct  33190  indf1ofs  33313  s2f1  33390  mndlactf1o  33471  mndractf1o  33472  gsumwrd2dccat  33519  cycpmconjv  33583  1arithidomlem2  33947  mplvrpmlem  34054  mplvrpmfgalem  34055  mplvrpmga  34056  mplvrpmmhm  34057  mplvrpmrhm  34058  esplysply  34082  lmimdim  34115  madjusmdetlem4  34341  tpr2rico  34423  qqhre  34531  eulerpartgbij  34884  eulerpartlemgh  34890  ballotlemscr  35031  ballotlemro  35035  ballotlemfrc  35039  ballotlemrinv0  35045  reprpmtf1o  35135  onvf1od  35705  vonf1owev  35707  vonf1owevOLD  35708  vonf1oonf1  35712  derangenlem  35751  subfacp1lem3  35762  subfacp1lem5  35764  erdsze2lem1  35783  cvmliftmolem1  35861  cvmlift2lem9a  35883  phpreu  38359  poimirlem1  38371  poimirlem4  38374  poimirlem9  38379  poimirlem22  38392  mblfinlem2  38408  metf1o  38506  ismtyima  38554  ismtyres  38559  rngoisocnv  38732  laut11  40960  diaf1oN  42004  mapdcnvcl  42526  mapdcnvid2  42531  ricdrng1  43411  evlselv  43436  eldioph2lem2  43607  eldioph2  43608  pwfi2f1o  43938  gicabl  43941  permaxext  45829  permac8prim  45838  sge0f1o  47211  nnfoctbdjlem  47284  3f1oss1  47964  f1ocof1ob2  47971  f1oresf1o  48179  fundcmpsurbijinjpreimafv  48308  fundcmpsurinjpreimafv  48309  fundcmpsurinjimaid  48312  grimcnv  48805  uhgrimedg  48808  isuspgrim0lem  48810  isuspgrim0  48811  isuspgrimlem  48812  upgrimtrlslem2  48822  upgrimpthslem2  48825  uhgrimisgrgriclem  48847  uhgrimisgrgric  48848  clnbgrgrimlem  48850  grimedg  48852  grtriproplem  48856  grtrif1o  48859  grimgrtri  48866  stgrusgra  48876  isubgr3stgrlem4  48886  isubgr3stgrlem7  48889  isubgr3stgrlem8  48890  grlimgrtri  48920  usgrexmpl1lem  48938  usgrexmpl2lem  48943  gpgusgra  48974  imaidfu  50037  uptrlem1  50137