Theorem f1of1 6828

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 6550	. 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 6540  –onto→wfo 6541  –1-1-onto→wf1o 6542

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 6550

This theorem is used by:  f1of  6829  f1un  6850  f1sng  6873  f1oresrab  7133  f1ounsn  7284  f1prex  7296  f1ocnvfvrneq  7298  f1ocoima  7315  isof1oidb  7336  isores3  7347  isoini2  7351  isosolem  7359  f1oiso  7363  weniso  7368  weisoeq  7369  f1opw2  7680  f1ovv  7974  mptcnfimad  8002  tposf12  8276  oacomf1olem  8580  enssdom  9011  enssdomOLD  9012  domssex2  9164  mapen  9168  ssenen  9178  ssfiALT  9197  ssdomfi  9219  ssdomfi2  9220  sucdom2  9226  phplem2  9228  php3  9232  snnen2o  9244  1sdom2dom  9253  f1finf1o  9272  domunfican  9321  fiint  9326  f1opwfi  9353  mapfienlem1  9404  mapfienlem2  9405  mapfien  9407  marypha1lem  9432  ordtypelem10  9528  oiexg  9536  unxpwdom2  9589  wemapwe  9705  inlresf1  10003  inrresf1  10005  isinffi  10080  infxpenlem  10099  fseqenlem1  10110  dfac12lem2  10230  dfac12r  10232  ackbij2  10327  cff1  10343  infpssrlem4  10391  fin4en1  10394  enfin2i  10406  fin23lem28  10425  isf32lem7  10444  isf34lem3  10460  enfin1ai  10469  canthnum  10741  canthwe  10743  canthp1lem2  10745  pwfseqlem4  10754  pwfseqlem5  10755  tskuni  10875  grothomex  10921  negfi  12273  seqf1olem1  14191  hashfacen  14606  hashf1lem1  14607  s1f1  14764  fsumss  15900  ackbijnn  16006  fprodss  16124  bitsinv2  16622  bitsf1  16625  sadasslem  16649  sadeq  16651  phimullem  16965  eulerthlem2  16968  unbenlem  17095  f1ocpbllem  17705  f1ovscpbl  17707  xpsff1o2  17750  xpsmnd  18980  injsubmefmnd  19102  xpsgrp  19278  eqgen  19402  conjsubgen  19474  subggim  19489  gim0to0  19492  gicsubgen  19502  symgfvne  19604  symgextf1  19644  symgfixelsi  19658  f1omvdmvd  19666  f1omvdconj  19669  pmtrfconj  19689  odngen  19800  sylow1lem2  19822  sylow2blem1  19843  gsumzres  20132  gsumzcl2  20133  gsumzf1o  20135  gsumzaddlem  20144  gsumconst  20157  gsumzmhm  20160  gsumzoppg  20167  dprdf1o  20257  xpsrngd  20410  xpsringd  20571  gsumfsum  21749  zntoslem  21871  znunithash  21879  iporthcom  21950  lindfres  22138  islindf3  22141  lindsmm  22143  lmimlbs  22151  lbslcic  22156  coe1sfi  22540  coe1mul2lem2  22596  resthauslem  23690  sshauslem  23699  basqtop  24039  tgqtop  24040  hmeoopn  24094  hmeocld  24095  hmeontr  24097  hmeoimaf1o  24098  haushmphlem  24115  tsmsf1o  24473  imasdsf1olem  24701  imasf1oxmet  24703  imasf1oxms  24817  ovoliunlem1  25832  dyadmbl  25930  vitalilem3  25940  dvcnvlem  26305  dvne0f1  26341  dvcnvrelem2  26347  logf1o2  26987  dvlog  26988  wilthlem3  27406  oldfib  28772  istrkg2ld  28931  f1otrg  29457  axcontlem10  29560  usgrf1  29762  usgrexmplef  29849  usgrres1  29905  edgusgrnbfin  29963  usgrexilem  30030  sizusglecusglem1  30051  uspgr2wlkeq  30235  trlres  30292  usgr2trlncl  30355  clwlkclwwlk  30602  adjbd1o  32696  padct  33361  indf1ofs  33483  s2f1  33560  mndlactf1o  33641  mndractf1o  33642  gsumwrd2dccat  33689  cycpmconjv  33753  1arithidomlem2  34118  mplvrpmlem  34225  mplvrpmfgalem  34226  mplvrpmga  34227  mplvrpmmhm  34228  mplvrpmrhm  34229  esplysply  34253  lmimdim  34286  madjusmdetlem4  34512  tpr2rico  34594  qqhre  34702  eulerpartgbij  35054  eulerpartlemgh  35060  ballotlemscr  35201  ballotlemro  35205  ballotlemfrc  35209  ballotlemrinv0  35215  reprpmtf1o  35305  dfac15  35821  jf1  35961  onvf1od  35986  vonf1owev  35988  vonf1owevOLD  35989  vonf1oonf1  35994  vonf1onprcf1ac  35995  onprcf1acwevd  35998  onprcf1of1orad  36004  onprcf1of1orbd  36005  derangenlem  36054  subfacp1lem3  36065  subfacp1lem5  36067  erdsze2lem1  36086  cvmliftmolem1  36164  cvmlift2lem9a  36186  phpreu  38664  poimirlem1  38676  poimirlem4  38679  poimirlem9  38684  poimirlem22  38697  mblfinlem2  38713  metf1o  38826  ismtyima  38874  ismtyres  38879  rngoisocnv  39052  laut11  41280  diaf1oN  42324  mapdcnvcl  42846  mapdcnvid2  42851  ricdrng1  43729  evlselv  43754  eldioph2lem2  43909  eldioph2  43910  pwfi2f1o  44235  gicabl  44238  permaxext  46131  permac8prim  46140  sge0f1o  47528  nnfoctbdjlem  47601  3f1oss1  48281  f1ocof1ob2  48288  f1oresf1o  48496  fundcmpsurbijinjpreimafv  48625  fundcmpsurinjpreimafv  48626  fundcmpsurinjimaid  48629  grimcnv  49122  uhgrimedg  49125  isuspgrim0lem  49127  isuspgrim0  49128  isuspgrimlem  49129  upgrimtrlslem2  49139  upgrimpthslem2  49142  uhgrimisgrgriclem  49164  uhgrimisgrgric  49165  clnbgrgrimlem  49167  grimedg  49169  grtriproplem  49173  grtrif1o  49176  grimgrtri  49183  stgrusgra  49193  isubgr3stgrlem4  49203  isubgr3stgrlem7  49206  isubgr3stgrlem8  49207  grlimgrtri  49237  usgrexmpl1lem  49255  usgrexmpl2lem  49260  gpgusgra  49291  imaidfu  50362  uptrlem1  50462