MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1of Structured version   Visualization version   GIF version

Theorem f1of 6032
Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1of (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)

Proof of Theorem f1of
StepHypRef Expression
1 f1of1 6031 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
2 f1f 5996 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wf 5783  1-1wf1 5784  1-1-ontowf1o 5786
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 195  df-an 384  df-f1 5792  df-f1o 5794
This theorem is referenced by:  f1ofn  6033  f1ompt  6272  f1oresrab  6284  fsn  6290  fsnunf  6331  f1ocnvfv1  6407  f1ocnvfv2  6408  fsnex  6413  f1ocnvdm  6415  fcof1oinvd  6423  fveqf1o  6432  isocnv  6455  isocnv3  6457  isores2  6458  isotr  6461  isofr2  6469  isopolem  6470  isosolem  6472  f1oiso2  6477  weniso  6479  f1ofveu  6519  f1oexrnex  6982  f1oabexg  6992  wemoiso  7018  suppsnop  7170  smoiso  7320  mapsn  7759  ralxpmap  7767  f1oen2g  7832  en1  7883  enfixsn  7928  mapen  7983  ac6sfi  8063  domunfican  8092  fiint  8096  mapfienlem1  8167  mapfienlem2  8168  mapfienlem3  8169  mapfien  8170  supisoex  8237  supiso  8238  ordiso2  8277  ordtypelem10  8289  hartogslem1  8304  unxpwdom2  8350  cantnfle  8425  cantnfp1lem3  8434  cantnflem1b  8440  cantnflem1d  8442  cantnflem1  8443  cnfcomlem  8453  cnfcom  8454  cnfcom2lem  8455  cnfcom2  8456  cnfcom3lem  8457  cnfcom3  8458  cnfcom3clem  8459  infxpenlem  8693  infxpenc  8698  infxpenc2lem2  8700  fseqenlem1  8704  acndom  8731  acndom2  8734  infpwfien  8742  iunfictbso  8794  infmap2  8897  ackbij2lem2  8919  infpssrlem3  8984  infpssrlem4  8985  fin23lem30  9021  isf32lem6  9037  isf32lem7  9038  isf32lem8  9039  enfin1ai  9063  axcc3  9117  axcclem  9136  ttukeylem7  9194  fpwwe2lem6  9310  fpwwe2lem7  9311  fpwwe2lem9  9313  canthp1lem2  9328  canthp1  9329  pwfseqlem4a  9336  pwfseqlem5  9338  dfle2  11812  axdc4uzlem  12596  seqf1olem1  12654  seqf1olem2  12655  seqf1o  12656  hashkf  12933  hasheqf1oi  12951  hasheqf1oiOLD  12952  hasheqf1od  12955  hashcl  12958  hashgadd  12976  hashfacen  13044  hashf1lem1  13045  fz1isolem  13051  seqcoll  13054  seqcoll2  13055  cnrecnv  13696  sumeq2ii  14214  summolem3  14235  summolem2a  14236  fsum  14241  fsumf1o  14244  fsumss  14246  fsumcl2lem  14252  fsumadd  14260  fsummulc2  14301  fsumrelem  14323  ackbijnn  14342  prodeq2ii  14425  prodmolem3  14445  prodmolem2a  14446  fprod  14453  fprodf1o  14458  fprodss  14460  fprodser  14461  fprodcl2lem  14462  fprodmul  14472  fproddiv  14473  fprodn0  14491  fproddvdsd  14840  sadcaddlem  14960  sadadd2lem  14962  sadadd3  14964  sadaddlem  14969  sadasslem  14973  sadeq  14975  phimullem  15265  eulerthlem1  15267  eulerthlem2  15268  unbenlem  15393  vdwlem8  15473  0ram  15505  wunndx  15654  xpsaddlem  16001  xpsvsca  16005  xpsle  16007  idfucl  16307  setccatid  16500  setcinv  16506  catcisolem  16522  estrccatid  16538  funcestrcsetclem7  16552  funcestrcsetclem8  16553  funcsetcestrclem7  16567  funcsetcestrclem8  16568  yonffthlem  16688  gsumpropd2lem  17039  idmhm  17110  mhmf1o  17111  gsumws1  17142  idghm  17441  ghmf1o  17456  symgval  17565  symgbas  17566  elsymgbas  17568  symgbasf  17570  symgbasfi  17572  symg1bas  17582  symggrp  17586  symgid  17587  lactghmga  17590  symgfixf1  17623  f1omvdmvd  17629  f1omvdconj  17632  f1omvdco2  17634  pmtrfconj  17652  symggen  17656  pmtrdifellem1  17662  pmtrdifellem2  17663  psgnunilem1  17679  gsumval3eu  18071  gsumval3lem1  18072  gsumval3  18074  gsumzf1o  18079  gsumconst  18100  gsumsub  18114  gsumcom2  18140  dprdfsub  18186  dprdf1o  18197  dprdsn  18201  ablfaclem2  18251  srngcl  18621  lmhmf1o  18810  fidomndrnglem  19070  psrass1lem  19141  psrnegcl  19160  psrlinv  19161  coe1f2  19343  coe1add  19398  evls1rhmlem  19450  evl1sca  19462  pf1ind  19483  gsumfsum  19575  zntoslem  19666  islinds2  19910  lindsmm  19925  mat1dimelbas  20035  mat1f  20046  mdetleib2  20152  mdetrsca  20167  mdetralt  20172  mdetunilem7  20182  mdetunilem9  20184  ssidcn  20808  hausdiag  21197  hmphdis  21348  indishmph  21350  cmphaushmeo  21352  ordthmeolem  21353  txhmeo  21355  qtopf1  21368  ufldom  21515  symgtgp  21654  tsmsf1o  21697  iducn  21836  imasdsf1olem  21926  xpsdsval  21934  imasf1obl  22041  icchmeo  22476  iccpnfcnv  22479  xrhmeo  22481  cnheiborlem  22489  ovolctb  22979  ovoliunlem1  22991  ovoliunlem2  22992  iunmbl2  23046  dyadmbl  23088  vitalilem2  23098  vitalilem3  23099  vitalilem4  23100  vitalilem5  23101  mbfid  23123  dvid  23401  dvexp  23436  dvcnvlem  23457  dvcnv  23458  dvcnvrelem2  23499  dvcnvre  23500  efcvx  23921  reefgim  23922  efif1olem4  24009  eff1olem  24012  logrncl  24032  relogcl  24040  dvrelog  24097  relogcn  24098  logcn  24107  logf1o2  24110  dvlog  24111  dvlog2  24113  advlog  24114  advlogexp  24115  logtayl  24120  logccv  24123  dvcxp1  24195  loglesqrt  24213  asinrebnd  24342  dvatan  24376  efrlim  24410  amgmlem  24430  lgamcvg2  24495  wilthlem2  24509  wilthlem3  24510  sqff1o  24622  lgsqrlem4  24788  logdivsum  24936  log2sumbnd  24947  isismt  25144  motcl  25149  motco  25150  cnvmot  25151  motgrp  25153  motcgrg  25154  f1otrg  25466  f1otrge  25467  axlowdimlem10  25546  axcontlem5  25563  axcontlem10  25568  umgra1  25618  iseupa  26255  eupatrl  26258  eupa0  26264  eupares  26265  eupap1  26266  eupath2lem3  26269  dmadjrn  27941  unopnorm  27963  unopadj  27965  unoplin  27966  counop  27967  idcnop  28027  idhmop  28028  unopbd  28061  bracnln  28155  cnvbraval  28156  leopnmid  28184  nmopleid  28185  hmopidmch  28199  hmopidmpj  28200  disjrdx  28589  isoun  28665  padct  28688  fcobij  28691  fcobijfs  28692  abliso  28830  symgfcoeu  28979  tpr2rico  29089  xrge0iifmhm  29116  xrge0pluscn  29117  rrhre  29196  esumf1o  29242  volmeas  29424  eulerpartgbij  29564  eulerpartlemmf  29567  eulerpartlemgvv  29568  eulerpartlemgf  29571  eulerpartlemgs2  29572  eulerpartlemn  29573  ballotlemsima  29707  deranglem  30205  derangsn  30209  derangenlem  30210  subfacp1lem4  30222  subfacp1lem5  30223  subfacp1lem6  30224  cvmfolem  30318  cvmliftlem6  30329  poimirlem1  32380  poimirlem2  32381  poimirlem3  32382  poimirlem4  32383  poimirlem6  32385  poimirlem7  32386  poimirlem9  32388  poimirlem11  32390  poimirlem12  32391  poimirlem16  32395  poimirlem17  32396  poimirlem19  32398  poimirlem20  32399  poimirlem22  32401  poimirlem26  32405  poimirlem27  32406  poimirlem28  32407  poimirlem32  32411  mblfinlem2  32417  dvasin  32466  f1ocan1fv  32491  metf1o  32521  ismtyval  32569  isismty  32570  ismtyima  32572  ismtyhmeolem  32573  ismtybndlem  32575  ismrer1  32607  reheibor  32608  grposnOLD  32651  rngoisocnv  32750  lflnegl  33181  lautset  34186  islaut  34187  lautcl  34191  lautco  34201  pautsetN  34202  ispautN  34203  ldilco  34220  ltrncoidN  34232  ltrncoval  34249  trlcoabs2N  34828  trlcoat  34829  trlcone  34834  cdlemg47a  34840  cdlemg46  34841  cdlemg47  34842  trljco  34846  tgrpgrplem  34855  tendoidcl  34875  tendo0co2  34894  tendo0pl  34897  cdlemi2  34925  cdlemk2  34938  cdlemk4  34940  cdlemk8  34944  cdlemkid2  35030  cdlemk45  35053  cdlemk53b  35062  cdlemk53  35063  cdlemk55a  35065  erng1r  35101  tendocnv  35128  dvalveclem  35132  dva0g  35134  dvhgrp  35214  dvh0g  35218  dvhopN  35223  cdlemn3  35304  cdlemn8  35311  cdlemn9  35312  dihordlem7b  35322  dihopelvalcpre  35355  dihmeetlem1N  35397  dihglblem5apreN  35398  lcfrlem13  35662  hvmapclN  35871  hvmapcl2  35873  mapfzcons  36097  mzpresrename  36131  diophrw  36140  eldioph2  36143  diophren  36195  kelac1  36451  imasgim  36488  lnrfg  36508  brco2f1o  37150  brco3f1o  37151  clsneikex  37224  clsneinex  37225  clsneiel1  37226  neicvgmex  37235  neicvgel1  37237  dssmapntrcls  37246  mapsnd  38183  stoweidlem27  38721  stoweidlem31  38725  stoweidlem39  38733  fourierdlem20  38821  fourierdlem50  38850  fourierdlem52  38852  fourierdlem54  38854  fourierdlem64  38864  fourierdlem76  38876  fourierdlem102  38902  fourierdlem114  38914  sge0f1o  39076  nnfoctbdjlem  39149  isomenndlem  39221  ovnsubaddlem1  39261  upgrres1  40531  umgrres1  40532  1hegrlfgr  40721  upgriseupth  41374  mgmhmf1o  41576  idmgmhm  41577  funcringcsetcALTV2lem8  41834  funcringcsetclem8ALTV  41857  amgmwlem  42317
  Copyright terms: Public domain W3C validator