Theorem f1ofo 6400

Description: A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.)

Assertion

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

Proof of Theorem f1ofo

Step	Hyp	Ref	Expression
1		dff1o3 6399	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))
2	1	simplbi 493	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)

Syntax hints:   → wi 4  ^◡ccnv 5356  Fun wfun 6131  –onto→wfo 6135  –1-1-onto→wf1o 6136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-in 3799  df-ss 3806  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144

This theorem is referenced by:  f1imacnv  6409  resin  6414  f1ococnv2  6419  fo00  6428  isoini  6862  isofrlem  6864  isoselem  6865  ncanth  6883  f1opw2  7167  f1dmex  7417  f1ovv  7418  f1oweALT  7431  wemoiso2  7433  curry1  7552  curry2  7555  smoiso2  7751  bren  8252  f1oeng  8262  en1  8310  canth2  8403  domss2  8409  mapen  8414  ssenen  8424  phplem4  8432  php3  8436  ssfi  8470  domunfican  8523  fiint  8527  f1fi  8543  f1opwfi  8560  mapfien  8603  supisolem  8669  ordiso2  8711  ordtypelem10  8723  oismo  8736  wdomref  8768  brwdom2  8769  unxpwdom2  8784  cantnflt2  8869  cantnfp1lem3  8876  wemapwe  8893  infxpenc2lem1  9177  fseqen  9185  infpwfien  9220  infmap2  9377  ackbij2  9402  cff1  9417  cofsmo  9428  infpssr  9467  enfin2i  9480  fin23lem27  9487  enfin1ai  9543  fin1a2lem7  9565  axcclem  9616  ttukeylem1  9668  fpwwe2lem6  9794  fpwwe2lem9  9797  canthp1lem2  9812  tskuni  9942  gruen  9971  cnexALT  12137  fiinfnf1o  13459  hasheqf1oi  13461  hashfacen  13556  fsumf1o  14865  fsumss  14867  fprodf1o  15083  fprodss  15085  ruc  15380  unbenlem  16020  xpsfrn  16619  xpsbas  16624  xpsadd  16626  xpsmul  16627  xpssca  16628  xpsvsca  16629  xpsless  16630  xpsle  16631  imasmndf1  17719  imasgrpf1  17923  gicsubgen  18108  symgmov2  18200  symgextfo  18229  symgfixelsi  18242  giccyg  18691  gsumzres  18700  gsumzcl2  18701  gsumzf1o  18703  gsumzaddlem  18711  gsumconst  18724  gsumzmhm  18727  gsumzoppg  18734  dprdf1o  18822  coe1mul2lem2  20038  gsumfsum  20213  znleval  20302  lmimlbs  20583  lbslcic  20588  cmpfi  21624  idqtop  21922  basqtop  21927  tgqtop  21928  hmeontr  21985  hmeoimaf1o  21986  hmeoqtop  21991  cmphmph  22004  connhmph  22005  nrmhmph  22010  indishmph  22014  cmphaushmeo  22016  xpstps  22026  xpstopnlem2  22027  fmid  22176  tsmsf1o  22360  imasdsf1olem  22590  imasf1oxmet  22592  imasf1omet  22593  xpsdsfn  22594  imasf1oxms  22706  imasf1oms  22707  iccpnfhmeo  23156  cnheiborlem  23165  ovolctb  23698  ovolicc2lem4  23728  dyadmbl  23808  mbfimaopnlem  23863  itg1addlem4  23907  dvcnvrelem2  24222  dvcnvre  24223  deg1ldg  24293  deg1leb  24296  efifo  24735  logrn  24746  dvrelog  24824  efopnlem2  24844  fsumdvdsmul  25377  f1otrg  26224  axcontlem10  26326  edgusgrnbfin  26725  eupthvdres  27643  cnvunop  29353  counop  29356  idunop  29413  elunop2  29448  fmptco1f1o  30003  padct  30067  xrge0iifiso  30583  volmeas  30896  ballotlemro  31187  derangenlem  31756  subfacp1lem3  31767  subfacp1lem5  31769  erdsze2lem1  31788  cvmsss2  31859  poimirlem1  34041  poimirlem2  34042  poimirlem3  34043  poimirlem4  34044  poimirlem5  34045  poimirlem6  34046  poimirlem7  34047  poimirlem9  34049  poimirlem10  34050  poimirlem11  34051  poimirlem12  34052  poimirlem14  34054  poimirlem15  34055  poimirlem16  34056  poimirlem17  34057  poimirlem19  34059  poimirlem20  34060  poimirlem22  34062  poimirlem23  34063  poimirlem24  34064  poimirlem25  34065  poimirlem29  34069  poimirlem31  34071  mblfinlem2  34078  ismtybndlem  34234  ismtyres  34236  diaintclN  37217  dibintclN  37326  mapdrn  37808  dnnumch2  38584  kelac1  38602  lnmlmic  38627  pwslnmlem1  38631  pwfi2f1o  38635  gicabl  38638  imasgim  38639  isnumbasgrplem1  38640  ntrneifv2  39344  stoweidlem27  41181  fourierdlem20  41281  fourierdlem51  41311  fourierdlem52  41312  fourierdlem63  41323  fourierdlem64  41324  fourierdlem65  41325  fourierdlem102  41362  fourierdlem114  41374  sge0f1o  41533  nnfoctbdjlem  41606  isomenndlem  41681  ovnsubaddlem1  41721  f1oresf1o2  42342  isomuspgrlem2d  42754