Theorem f1of1 6838

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 6555	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2	1	simplbi 497	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)

Syntax hints:   → wi 4  –1-1→wf1 6545  –onto→wfo 6546  –1-1-onto→wf1o 6547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396  df-f1o 6555

This theorem is referenced by:  f1of  6839  f1un  6859  f1sng  6881  f1oresrab  7136  f1prex  7293  f1ocnvfvrneq  7295  isof1oidb  7332  isores3  7343  isoini2  7347  isosolem  7355  f1oiso  7359  weniso  7362  weisoeq  7363  f1opw2  7676  f1ovv  7961  mptcnfimad  7990  tposf12  8256  oacomf1olem  8584  enssdom  8997  sucdom2OLD  9106  domssex2  9161  mapen  9165  ssenen  9175  ssfiALT  9198  ssdomfi  9223  ssdomfi2  9224  sucdom2  9230  phplem2  9232  php3  9236  phplem4OLD  9244  php3OLD  9248  snnen2o  9261  1sdom2dom  9271  f1finf1o  9295  f1finf1oOLD  9296  domunfican  9344  fiint  9348  f1opwfi  9380  mapfienlem1  9428  mapfienlem2  9429  mapfien  9431  marypha1lem  9456  ordtypelem10  9550  oiexg  9558  unxpwdom2  9611  wemapwe  9720  inlresf1  9938  inrresf1  9940  isinffi  10015  infxpenlem  10036  fseqenlem1  10047  dfac12lem2  10167  dfac12r  10169  ackbij2  10266  cff1  10281  infpssrlem4  10329  fin4en1  10332  enfin2i  10344  fin23lem28  10363  isf32lem7  10382  isf34lem3  10398  enfin1ai  10407  canthnum  10672  canthwe  10674  canthp1lem2  10676  pwfseqlem4  10685  pwfseqlem5  10686  tskuni  10806  grothomex  10852  negfi  12193  seqf1olem1  14038  hashfacen  14445  hashfacenOLD  14446  hashf1lem1  14447  hashf1lem1OLD  14448  fsumss  15703  ackbijnn  15806  fprodss  15924  bitsinv2  16417  bitsf1  16420  sadasslem  16444  sadeq  16446  phimullem  16747  eulerthlem2  16750  unbenlem  16876  f1ocpbllem  17505  f1ovscpbl  17507  xpsff1o2  17550  xpsmnd  18733  injsubmefmnd  18848  xpsgrp  19014  eqgen  19135  conjsubgen  19204  subggim  19219  gim0to0  19222  gicsubgen  19232  symgfvne  19334  symgextf1  19375  symgfixelsi  19389  f1omvdmvd  19397  f1omvdconj  19400  pmtrfconj  19420  odngen  19531  sylow1lem2  19553  sylow2blem1  19574  gsumzres  19863  gsumzcl2  19864  gsumzf1o  19866  gsumzaddlem  19875  gsumconst  19888  gsumzmhm  19891  gsumzoppg  19898  dprdf1o  19988  xpsrngd  20118  xpsringd  20267  gsumfsum  21366  zntoslem  21489  znunithash  21497  iporthcom  21566  lindfres  21756  islindf3  21759  lindsmm  21761  lmimlbs  21769  lbslcic  21774  coe1sfi  22131  coe1mul2lem2  22186  resthauslem  23266  sshauslem  23275  basqtop  23614  tgqtop  23615  hmeoopn  23669  hmeocld  23670  hmeontr  23672  hmeoimaf1o  23673  haushmphlem  23690  tsmsf1o  24048  imasdsf1olem  24278  imasf1oxmet  24280  imasf1oxms  24397  ovoliunlem1  25430  dyadmbl  25528  vitalilem3  25538  dvcnvlem  25907  dvne0f1  25944  dvcnvrelem2  25950  logf1o2  26583  dvlog  26584  wilthlem3  27001  istrkg2ld  28263  f1otrg  28674  axcontlem10  28783  usgrf1  28984  usgrexmplef  29071  usgrres1  29127  edgusgrnbfin  29185  usgrexilem  29252  sizusglecusglem1  29274  uspgr2wlkeq  29459  trlres  29513  usgr2trlncl  29573  clwlkclwwlk  29811  adjbd1o  31894  padct  32501  s1f1  32666  s2f1  32668  cycpmconjv  32863  lmimdim  33297  madjusmdetlem4  33431  tpr2rico  33513  qqhre  33621  indf1ofs  33645  eulerpartgbij  33992  eulerpartlemgh  33998  ballotlemscr  34138  ballotlemro  34142  ballotlemfrc  34146  ballotlemrinv0  34152  reprpmtf1o  34258  derangenlem  34781  subfacp1lem3  34792  subfacp1lem5  34794  erdsze2lem1  34813  cvmliftmolem1  34891  cvmlift2lem9a  34913  phpreu  37077  poimirlem1  37094  poimirlem4  37097  poimirlem9  37102  poimirlem22  37115  mblfinlem2  37131  metf1o  37228  ismtyima  37276  ismtyres  37281  rngoisocnv  37454  laut11  39559  diaf1oN  40603  mapdcnvcl  41125  mapdcnvid2  41130  ricdrng1  41764  evlselv  41820  eldioph2lem2  42181  eldioph2  42182  pwfi2f1o  42520  gicabl  42523  sge0f1o  45770  nnfoctbdjlem  45843  f1ocof1ob2  46462  f1oresf1o  46670  fundcmpsurbijinjpreimafv  46747  fundcmpsurinjpreimafv  46748  fundcmpsurinjimaid  46751  isuspgrim0lem  47169  isuspgrim0  47170  uspgrimprop  47171  isuspgrimlem  47172  grimcnv  47177