Theorem f1of1 6823

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 6545	. 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 6535  –onto→wfo 6536  –1-1-onto→wf1o 6537

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 6545

This theorem is used by:  f1of  6824  f1un  6845  f1sng  6868  f1oresrab  7128  f1ounsn  7280  f1prex  7292  f1ocnvfvrneq  7294  f1ocoima  7311  isof1oidb  7332  isores3  7343  isoini2  7347  isosolem  7355  f1oiso  7359  weniso  7364  weisoeq  7365  f1opw2  7676  f1ovv  7970  mptcnfimad  7998  tposf12  8268  oacomf1olem  8572  enssdom  9003  enssdomOLD  9004  domssex2  9156  mapen  9160  ssenen  9170  ssfiALT  9189  ssdomfi  9211  ssdomfi2  9212  sucdom2  9218  phplem2  9220  php3  9224  snnen2o  9236  1sdom2dom  9245  f1finf1o  9264  domunfican  9313  fiint  9318  f1opwfi  9345  mapfienlem1  9397  mapfienlem2  9398  mapfien  9400  marypha1lem  9425  ordtypelem10  9521  oiexg  9529  unxpwdom2  9582  wemapwe  9698  inlresf1  9996  inrresf1  9998  isinffi  10073  infxpenlem  10092  fseqenlem1  10103  dfac12lem2  10223  dfac12r  10225  ackbij2  10320  cff1  10336  infpssrlem4  10384  fin4en1  10387  enfin2i  10399  fin23lem28  10418  isf32lem7  10437  isf34lem3  10453  enfin1ai  10462  canthnum  10734  canthwe  10736  canthp1lem2  10738  pwfseqlem4  10747  pwfseqlem5  10748  tskuni  10868  grothomex  10914  negfi  12266  seqf1olem1  14184  hashfacen  14599  hashf1lem1  14600  s1f1  14756  fsumss  15891  ackbijnn  15997  fprodss  16115  bitsinv2  16613  bitsf1  16616  sadasslem  16640  sadeq  16642  phimullem  16956  eulerthlem2  16959  unbenlem  17086  f1ocpbllem  17696  f1ovscpbl  17698  xpsff1o2  17741  xpsmnd  18971  injsubmefmnd  19093  xpsgrp  19269  eqgen  19393  conjsubgen  19465  subggim  19480  gim0to0  19483  gicsubgen  19493  symgfvne  19595  symgextf1  19635  symgfixelsi  19649  f1omvdmvd  19657  f1omvdconj  19660  pmtrfconj  19680  odngen  19791  sylow1lem2  19813  sylow2blem1  19834  gsumzres  20123  gsumzcl2  20124  gsumzf1o  20126  gsumzaddlem  20135  gsumconst  20148  gsumzmhm  20151  gsumzoppg  20158  dprdf1o  20248  xpsrngd  20401  xpsringd  20562  gsumfsum  21740  zntoslem  21862  znunithash  21870  iporthcom  21941  lindfres  22129  islindf3  22132  lindsmm  22134  lmimlbs  22142  lbslcic  22147  coe1sfi  22531  coe1mul2lem2  22587  resthauslem  23681  sshauslem  23690  basqtop  24030  tgqtop  24031  hmeoopn  24085  hmeocld  24086  hmeontr  24088  hmeoimaf1o  24089  haushmphlem  24106  tsmsf1o  24464  imasdsf1olem  24692  imasf1oxmet  24694  imasf1oxms  24808  ovoliunlem1  25823  dyadmbl  25921  vitalilem3  25931  dvcnvlem  26296  dvne0f1  26332  dvcnvrelem2  26338  logf1o2  26978  dvlog  26979  wilthlem3  27397  oldfib  28763  istrkg2ld  28922  f1otrg  29448  axcontlem10  29551  usgrf1  29753  usgrexmplef  29840  usgrres1  29896  edgusgrnbfin  29954  usgrexilem  30021  sizusglecusglem1  30042  uspgr2wlkeq  30226  trlres  30283  usgr2trlncl  30346  clwlkclwwlk  30593  adjbd1o  32687  padct  33310  indf1ofs  33433  s2f1  33510  mndlactf1o  33591  mndractf1o  33592  gsumwrd2dccat  33639  cycpmconjv  33703  1arithidomlem2  34068  mplvrpmlem  34175  mplvrpmfgalem  34176  mplvrpmga  34177  mplvrpmmhm  34178  mplvrpmrhm  34179  esplysply  34203  lmimdim  34236  madjusmdetlem4  34462  tpr2rico  34544  qqhre  34652  eulerpartgbij  35004  eulerpartlemgh  35010  ballotlemscr  35151  ballotlemro  35155  ballotlemfrc  35159  ballotlemrinv0  35165  reprpmtf1o  35255  onvf1od  35886  vonf1owev  35888  vonf1owevOLD  35889  vonf1oonf1  35893  vonf1onprcf1ac  35894  onprcf1acwevd  35897  derangenlem  35936  subfacp1lem3  35947  subfacp1lem5  35949  erdsze2lem1  35968  cvmliftmolem1  36046  cvmlift2lem9a  36068  phpreu  38527  poimirlem1  38539  poimirlem4  38542  poimirlem9  38547  poimirlem22  38560  mblfinlem2  38576  metf1o  38689  ismtyima  38737  ismtyres  38742  rngoisocnv  38915  laut11  41143  diaf1oN  42187  mapdcnvcl  42709  mapdcnvid2  42714  ricdrng1  43592  evlselv  43617  eldioph2lem2  43771  eldioph2  43772  pwfi2f1o  44097  gicabl  44100  permaxext  45994  permac8prim  46003  sge0f1o  47391  nnfoctbdjlem  47464  3f1oss1  48144  f1ocof1ob2  48151  f1oresf1o  48359  fundcmpsurbijinjpreimafv  48488  fundcmpsurinjpreimafv  48489  fundcmpsurinjimaid  48492  grimcnv  48985  uhgrimedg  48988  isuspgrim0lem  48990  isuspgrim0  48991  isuspgrimlem  48992  upgrimtrlslem2  49002  upgrimpthslem2  49005  uhgrimisgrgriclem  49027  uhgrimisgrgric  49028  clnbgrgrimlem  49030  grimedg  49032  grtriproplem  49036  grtrif1o  49039  grimgrtri  49046  stgrusgra  49056  isubgr3stgrlem4  49066  isubgr3stgrlem7  49069  isubgr3stgrlem8  49070  grlimgrtri  49100  usgrexmpl1lem  49118  usgrexmpl2lem  49123  gpgusgra  49154  imaidfu  50217  uptrlem1  50317