Theorem f1of1 6049

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

Syntax hints:   → wi 4  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803

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 196  df-an 385  df-f1o 5811

This theorem is referenced by:  f1of  6050  f1sng  6090  f1oresrab  6302  f1prex  6439  f1ocnvfvrneq  6441  isof1oidb  6474  isores3  6485  isoini2  6489  isosolem  6497  f1oiso  6501  weniso  6504  weisoeq  6505  f1opw2  6786  f1ovv  7030  tposf12  7264  oacomf1olem  7531  enssdom  7866  domssex2  8005  mapen  8009  ssenen  8019  phplem4  8027  php3  8031  sucdom2  8041  ssfi  8065  f1finf1o  8072  domunfican  8118  fiint  8122  f1opwfi  8153  mapfienlem1  8193  mapfienlem2  8194  mapfien  8196  marypha1lem  8222  ordtypelem10  8315  oiexg  8323  unxpwdom2  8376  wemapwe  8477  isinffi  8701  infxpenlem  8719  fseqenlem1  8730  dfac12lem2  8849  dfac12r  8851  ackbij2  8948  cff1  8963  infpssrlem4  9011  fin4en1  9014  enfin2i  9026  fin23lem28  9045  isf32lem7  9064  isf34lem3  9080  enfin1ai  9089  canthnum  9350  canthwe  9352  canthp1lem2  9354  pwfseqlem4  9363  pwfseqlem5  9364  tskuni  9484  grothomex  9530  negfi  10850  seqf1olem1  12702  hashfacen  13095  hashf1lem1  13096  fsumss  14303  ackbijnn  14399  fprodss  14517  bitsinv2  15003  bitsf1  15006  sadasslem  15030  sadeq  15032  phimullem  15322  eulerthlem2  15325  unbenlem  15450  f1ocpbllem  16007  f1ovscpbl  16009  xpsff1o2  16054  xpsmnd  17153  xpsgrp  17357  eqgen  17470  conjsubgen  17516  subggim  17531  gicsubgen  17544  symgfvne  17631  symgextf1  17664  symgfixelsi  17678  f1omvdmvd  17686  f1omvdconj  17689  pmtrfconj  17709  odngen  17815  sylow1lem2  17837  sylow2blem1  17858  gsumzres  18133  gsumzcl2  18134  gsumzf1o  18136  gsumzaddlem  18144  gsumconst  18157  gsumzmhm  18160  gsumzoppg  18167  dprdf1o  18254  rim0to0  18565  coe1sfi  19404  coe1mul2lem2  19459  gsumfsum  19632  zntoslem  19724  znunithash  19732  iporthcom  19799  lindfres  19981  islindf3  19984  lindsmm  19986  lmimlbs  19994  lbslcic  19999  resthauslem  20977  sshauslem  20986  basqtop  21324  tgqtop  21325  hmeoopn  21379  hmeocld  21380  hmeontr  21382  hmeoimaf1o  21383  haushmphlem  21400  tsmsf1o  21758  imasdsf1olem  21988  imasf1oxmet  21990  imasf1oxms  22104  ovoliunlem1  23077  dyadmbl  23174  vitalilem3  23185  dvcnvlem  23543  dvne0f1  23579  dvcnvrelem2  23585  logf1o2  24196  dvlog  24197  wilthlem3  24596  istrkg2ld  25159  f1otrg  25551  axcontlem10  25653  usgraf1  25889  uslgra1  25901  usgra1  25902  usgraexmplef  25929  edgusgranbfin  25979  cusgraexilem2  25996  sizeusglecusglem1  26012  2trllemE  26083  constr1trl  26118  usgra2adedgspthlem2  26140  constr3trllem2  26179  eupatrl  26495  eupares  26502  eupath2lem3  26506  adjbd1o  28328  padct  28885  madjusmdetlem4  29224  tpr2rico  29286  qqhre  29392  indf1ofs  29415  eulerpartgbij  29761  eulerpartlemgh  29767  ballotlemscr  29907  ballotlemro  29911  ballotlemfrc  29915  ballotlemrinv0  29921  derangenlem  30407  subfacp1lem3  30418  subfacp1lem5  30420  erdsze2lem1  30439  cvmliftmolem1  30517  cvmlift2lem9a  30539  phpreu  32563  poimirlem1  32580  poimirlem4  32583  poimirlem9  32588  poimirlem22  32601  mblfinlem2  32617  metf1o  32721  ismtyima  32772  ismtyres  32777  rngoisocnv  32950  laut11  34390  diaf1oN  35437  mapdcnvcl  35959  mapdcnvid2  35964  eldioph2lem2  36342  eldioph2  36343  pwfi2f1o  36684  gicabl  36687  sge0f1o  39275  nnfoctbdjlem  39348  usgrf1  40402  usgrres1  40534  edgusgrnbfin  40601  usgrexi  40661  sizusglecusglem1  40677  uspgr2wlkeq  40854  trlres  40908  usgr2trlncl  40966  clwlkclwwlk  41211