MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vex Unicode version

Theorem vex 2791
Description: All set variables are sets (see isset 2792). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
vex  |-  x  e. 
_V

Proof of Theorem vex
StepHypRef Expression
1 eqid 2283 . 2  |-  x  =  x
2 df-v 2790 . . 3  |-  _V  =  { x  |  x  =  x }
32abeq2i 2390 . 2  |-  ( x  e.  _V  <->  x  =  x )
41, 3mpbir 200 1  |-  x  e. 
_V
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684   _Vcvv 2788
This theorem is referenced by:  isset  2792  ralv  2801  rexv  2802  reuv  2803  rmov  2804  rabab  2805  sbhypf  2833  ceqex  2898  ralab  2926  rexab  2928  moeq3  2942  mo2icl  2944  reu8  2961  sbc2or  2999  csbvarg  3108  csbiebg  3120  sbcnestgf  3128  sbnfc2  3141  ddif  3308  csbing  3376  dfun2  3404  dfin2  3405  vn0  3462  eqv  3470  abvor0  3472  sbss  3563  csbifg  3593  ifexg  3624  elpwg  3632  dftp2  3679  prnzg  3746  snssg  3754  difprsn  3756  sneqrg  3782  preq12bg  3791  pwpr  3823  pwtp  3824  pwv  3826  unipr  3841  uniprg  3842  unisng  3844  elintg  3870  elintrabg  3875  intss1  3877  ssint  3878  intmin  3882  intss  3883  intssuni  3884  intmin4  3891  intab  3892  intun  3894  intpr  3895  intprg  3896  uniintsn  3899  iinconst  3914  iuniin  3915  iinss1  3917  dfiin2g  3936  ssiinf  3951  iinss  3953  iinss2  3954  0iin  3960  iinab  3963  iinun2  3968  iundif2  3969  iindif2  3971  iinin2  3972  iinuni  3985  sspwuni  3987  iinpw  3990  iunpwss  3991  brab1  4068  csbopabg  4094  mptv  4112  trint  4128  trintss  4129  vprc  4152  inex1g  4157  ssexg  4160  intex  4167  inuni  4173  axpweq  4187  pwexg  4194  pwuni  4206  axpr  4213  zfpair2  4215  elALT  4218  rext  4222  sspwb  4223  unipw  4224  ssextss  4227  nnullss  4235  exss  4236  opth  4245  opthg  4246  copsexg  4252  copsex4g  4255  moop2  4261  euotd  4267  opelopabsbOLD  4273  opelopabsb  4275  pwin  4297  pwunss  4298  pwssun  4299  pwundifOLD  4301  epelg  4306  epel  4308  dfid3  4310  pofun  4330  epse  4376  wefrc  4387  tron  4415  onfr  4431  sucel  4465  suctr  4475  uniexg  4517  unexb  4520  snnex  4524  uniuni  4527  eusvnf  4529  eusvnfb  4530  reusv6OLD  4545  iunpw  4570  onint  4586  ordpwsuc  4606  unon  4622  ordunisuc  4623  onuninsuci  4631  orduninsuc  4634  limsssuc  4641  limuni3  4643  tfinds  4650  tfindsg  4651  tfindsg2  4652  tfinds2  4654  dfom2  4658  peano5  4679  finds  4682  findsg  4683  finds2  4684  0nelxp  4717  opelxp  4719  opeliunxp  4740  elvv  4748  elvvv  4749  elvvuni  4750  xpsspw  4797  xpsspwOLD  4798  relopabi  4811  opabid2  4815  difopab  4817  xpiindi  4821  ralxpf  4830  relop  4834  cnvco  4865  dfrn2  4868  dfdm4  4872  dmss  4878  dmin  4886  dmiun  4887  dmuni  4888  dm0  4892  dmi  4893  reldm0  4896  elreldm  4903  elrnmpt1  4928  dmrnssfld  4938  dmcoss  4944  dmcosseq  4946  opelresg  4962  resieq  4965  dmres  4976  elres  4990  relssres  4992  resopab  4996  resiexg  4997  iss  4998  dfres2  5002  dfima2  5014  csbima12g  5022  imadmrn  5024  imai  5027  elimasng  5039  args  5041  epini  5043  iniseg  5044  dffr3  5045  dfse2  5046  exse2  5047  cotr  5055  issref  5056  cnvsym  5057  intasym  5058  asymref  5059  asymref2  5060  intirr  5061  brcodir  5062  codir  5063  qfto  5064  poirr2  5067  cnvopab  5083  cnv0  5084  cnvi  5085  cnvdif  5087  rniun  5091  dminss  5095  imainss  5096  ssrnres  5116  rninxp  5117  dminxp  5118  cnvcnv3  5123  dfrel2  5124  dmsnn0  5138  dmsnopg  5144  cnvcnvsn  5150  dmsnsnsn  5151  cnvsng  5158  elxp4  5160  elxp5  5161  cnvresima  5162  dfco2  5172  dfco2a  5173  cores  5176  resco  5177  imaco  5178  rnco  5179  coiun  5182  co02  5186  coi1  5188  coass  5191  relssdmrn  5193  unielrel  5197  unixp0  5206  ressn  5211  cnviin  5212  cnvpo  5213  cnvso  5214  uniabio  5229  iotaval  5230  sniota  5246  csbiotag  5248  dffun2  5265  dffun7  5280  dffun8  5281  dffun9  5282  funopg  5286  funssres  5294  funun  5296  funcnvsn  5297  funcnv2  5309  funcnv  5310  funcnv3  5311  fun2cnv  5312  funcnvuni  5317  imadif  5327  isarep1  5331  2elresin  5355  fnres  5360  fcnvres  5418  fabexg  5422  fconstg  5428  fun11iun  5493  f1osng  5514  dffv3  5521  fv3  5541  fvres  5542  nfunsn  5558  funimass4  5573  ssimaexg  5585  dffv2  5592  dmfco  5593  fvopab6  5621  fndmdif  5629  iinpreima  5655  fvelrn  5661  dff3  5673  dffo4  5676  exfo  5678  f1ompt  5682  fmptco  5691  fsng  5697  dfmpt  5701  fnressn  5705  fressnfv  5707  fvsng  5714  zfrep6  5748  funfvima3  5755  idref  5759  fvclss  5760  fvresex  5762  abrexco  5766  opabex3  5769  imaiun  5771  dff13  5783  foeqcnvco  5804  f1eqcocnv  5805  fliftcnv  5810  isocnv2  5828  isomin  5834  isoini  5835  isofr  5839  isose  5840  f1oweALT  5851  wemoiso  5855  wemoiso2  5856  knatar  5857  oprabid  5882  csbovg  5889  eloprabga  5934  mpt2v  5937  caovmo  6057  f1opw  6072  ofmres  6116  op1stg  6132  op2ndg  6133  1stval2  6137  2ndval2  6138  fo1st  6139  fo2nd  6140  f1stres  6141  f2ndres  6142  fo1stres  6143  fo2ndres  6144  1st2val  6145  2nd2val  6146  xp1st  6149  xp2nd  6150  sbcopeq1a  6172  csbopeq1a  6173  eloprabi  6186  mpt2mptsx  6187  dmmpt2ssx  6189  fmpt2x  6190  ovmptss  6200  fmpt2co  6202  df1st2  6205  df2nd2  6206  1stconst  6207  2ndconst  6208  curry1  6210  curry2  6213  fparlem1  6218  fparlem2  6219  fpar  6222  fsplit  6223  frxp  6225  xporderlem  6226  soxp  6228  fnwelem  6230  fnse  6232  reldmtpos  6242  dmtpos  6246  rntpos  6247  ovtpos  6249  dftpos3  6252  dftpos4  6253  tpostpos  6254  porpss  6281  sorpss  6282  sorpsscmpl  6288  opiota  6290  opabiotafun  6291  opabiota  6293  riotav  6309  csbriotag  6317  onovuni  6359  smogt  6384  tfrlem3  6393  tfrlem8  6400  tfrlem9a  6402  tfrlem16  6409  tz7.44lem1  6418  rdg0g  6440  rdglim2  6445  tz7.48-1  6455  seqomlem1  6462  seqomlem2  6463  abianfplem  6470  oacl  6534  omcl  6535  oecl  6536  oa0r  6537  om0r  6538  om1r  6541  oe1m  6543  oaordi  6544  oawordri  6548  oawordeulem  6552  oalimcl  6558  oaass  6559  oarec  6560  omordi  6564  omwordri  6570  omlimcl  6576  odi  6577  omass  6578  omeulem1  6580  oen0  6584  oeordi  6585  oewordri  6590  oeworde  6591  oeoalem  6594  oeoelem  6596  nnawordex  6635  omabs  6645  omsmolem  6651  ercnv  6681  iserd  6686  eqerlem  6692  eqer  6693  ecdmn0  6702  erth  6704  erdisj  6707  qsss  6720  ecid  6724  qsid  6725  iiner  6731  qsel  6738  erovlem  6754  ecopovsym  6760  ecopovtrn  6761  ecopover  6762  mapprc  6776  fnmap  6779  fnpm  6780  mapval2  6797  pmsspw  6802  mapsn  6809  mapsncnv  6814  ixpconstg  6825  ixpprc  6837  uniixp  6839  ixpin  6841  ixpiin  6842  resixpfo  6854  elixpsn  6855  ixpsnf1o  6856  boxriin  6858  boxcutc  6859  bren  6871  brdomg  6872  domen  6875  domeng  6876  idssen  6906  ener  6908  domtr  6914  ensn1g  6926  en1  6928  en1b  6929  fundmen  6934  fundmeng  6935  mapsnen  6938  unen  6943  domdifsn  6945  xpsnen  6946  xpsneng  6947  xpcomeng  6954  xpassen  6956  xpdom2  6957  xpdom2g  6958  domunsncan  6962  omxpenlem  6963  pw2f1o  6967  fopwdom  6970  sbthlem10  6980  sbth  6981  sbthcl  6983  domunsn  7011  fodomr  7012  pwdom  7013  canth2  7014  canth2g  7015  domssex  7022  xpf1o  7023  mapen  7025  mapunen  7030  map2xp  7031  mapdom2  7032  mapdom3  7033  ssenen  7035  infensuc  7039  nneneq  7044  php  7045  php2  7046  php3  7047  sucdom2  7057  1sdom  7065  unxpdomlem2  7068  unxpdomlem3  7069  isinf  7076  fineqvlem  7077  fineqv  7078  pssnn  7081  ssfi  7083  dif1enOLD  7090  dif1en  7091  findcard  7097  findcard2  7098  findcard2s  7099  ac6sfi  7101  frfi  7102  fimax2g  7103  unbnn2  7114  isfinite2  7115  xpfi  7128  domunfican  7129  fiint  7133  fodomfi  7135  fodomfib  7136  iunfi  7144  pwfilem  7150  ixpfi2  7154  fissuni  7160  fipreima  7161  finsschain  7162  fival  7166  ssfii  7172  fi0  7173  fiin  7175  dffi2  7176  fipwuni  7179  fisn  7180  elfiun  7183  dffi3  7184  fifo  7185  marypha1lem  7186  dfsup2  7195  dfsup2OLD  7196  ordiso2  7230  oismo  7255  hartogslem1  7257  hartogs  7259  wofib  7260  wemappo  7264  wemapso2lem  7265  card2on  7268  brwdom  7281  brwdomn0  7283  brwdom2  7287  wdomtr  7289  wdompwdom  7292  canthwdom  7293  xpwdomg  7299  unxpwdom2  7302  ixpiunwdom  7305  elirrv  7311  zfregfr  7316  inf0  7322  inf3lema  7325  inf3lemd  7328  inf3lem1  7329  inf3lem2  7330  inf3lem3  7331  inf3lem5  7333  inf3lem6  7334  inf3lem7  7335  inf3  7336  infeq5  7338  omex  7344  dfom3  7348  dfom5  7351  infdifsn  7357  cantnfdm  7365  cantnfval  7369  cantnfval2  7370  cantnflt  7373  cantnff  7375  oemapso  7384  cantnflem1  7391  wemapwe  7400  cnfcom  7403  cnfcom3clem  7408  epfrs  7413  tcvalg  7423  tctr  7425  tcmin  7426  r1sdom  7446  r1val1  7458  tz9.12lem1  7459  tz9.12lem3  7461  tz9.13  7463  tz9.13g  7464  rankf  7466  unir1  7485  rankvalg  7489  rankonidlem  7500  r1val2  7509  bndrank  7513  ranklim  7516  r1pwOLD  7518  rankunb  7522  rankuni2b  7525  rankuni  7535  rankval4  7539  rankxplim  7549  rankxplim3  7551  rankxpsuc  7552  tcrank  7554  cp  7561  bnd2  7563  kardex  7564  karden  7565  cardf2  7576  tskwe  7583  cardlim  7605  harcard  7611  cardiun  7615  pm54.43  7633  r0weon  7640  infxpenlem  7641  infxpenc2lem2  7647  fseqenlem1  7651  fseqenlem2  7652  fseqen  7654  dfac8alem  7656  dfac8clem  7659  ac10ct  7661  ween  7662  acnlem  7675  finacn  7677  acndom  7678  acndom2  7681  wdomfil  7688  infpwfien  7689  alephon  7696  alephcard  7697  alephordi  7701  cardaleph  7716  alephval3  7737  iunfictbso  7741  aceq3lem  7747  dfac3  7748  dfac4  7749  dfac5lem1  7750  dfac5lem2  7751  dfac5lem3  7752  dfac5lem4  7753  dfac5lem5  7754  dfac5  7755  dfac2a  7756  dfac2  7757  dfac8  7761  dfac9  7762  dfac10b  7765  acacni  7766  dfacacn  7767  dfac13  7768  kmlem1  7776  kmlem2  7777  kmlem9  7784  kmlem10  7785  kmlem11  7786  kmlem12  7787  kmlem13  7788  cdafn  7795  pwsdompw  7830  infmap2  7844  ackbij1lem5  7850  ackbij1lem8  7853  ackbij2lem3  7867  ackbij2  7869  cflm  7876  cardcf  7878  cfeq0  7882  cfsuc  7883  cff1  7884  cfflb  7885  cfval2  7886  cflim2  7889  cfss  7891  cfslb2n  7894  cofsmo  7895  cfsmolem  7896  cfcoflem  7898  coftr  7899  sornom  7903  infpssr  7934  fin4en1  7935  fin23lem11  7943  enfin2i  7947  fin23lem26  7951  fin23lem14  7959  fin23lem16  7961  fin23lem17  7964  fin23lem21  7965  fin23lem32  7970  fin23lem34  7972  fin23lem39  7976  compsscnvlem  7996  compssiso  8000  isf34lem4  8003  enfin1ai  8010  isfin1-3  8012  fin67  8021  dffin7-2  8024  fin1a2lem7  8032  fin1a2lem10  8035  fin1a2lem12  8037  fin1a2lem13  8038  fin12  8039  itunitc1  8046  itunitc  8047  ituniiun  8048  hsmexlem2  8053  hsmexlem4  8055  hsmex  8058  axcc2lem  8062  axcc3  8064  acncc  8066  fin41  8070  dominf  8071  dcomex  8073  axdc2lem  8074  axdc3lem  8076  axdc3lem2  8077  axdc3lem4  8079  axdc4lem  8081  axcclem  8083  ac9  8110  ac6s  8111  ac6sg  8115  ac9s  8120  numthcor  8121  zorn2lem1  8123  zorn2lem4  8126  zorn2lem7  8129  zorng  8131  zornn0g  8132  ttukeylem5  8140  ttukeylem6  8141  ttukeylem7  8142  axdclem  8146  axdclem2  8147  fodomg  8150  fodomb  8151  brdom3  8153  brdom5  8154  brdom4  8155  brdom7disj  8156  brdom6disj  8157  iunfo  8161  ondomon  8185  cardmin  8186  alephval2  8194  dominfac  8195  fpwwe2lem1  8253  fpwwe2lem8  8259  fpwwe2lem11  8262  fpwwe2lem12  8263  fpwwe2lem13  8264  fpwwe2  8265  fpwwe  8268  canthwe  8273  canthp1lem1  8274  pwfseqlem1  8280  pwfseqlem2  8281  pwfseqlem3  8282  pwfseqlem4a  8283  pwfseqlem5  8285  pwxpndom2  8287  gchac  8295  gch2  8301  inawinalem  8311  winainflem  8315  winalim2  8318  winafp  8319  gchina  8321  wunfi  8343  intwun  8357  wunex2  8360  uniwun  8362  eltsk2g  8373  inttsk  8396  inar1  8397  rankcf  8399  tskcard  8403  tskuni  8405  gruun  8428  intgru  8436  ingru  8437  wfgru  8438  grudomon  8439  gruina  8440  grur1a  8441  grur1  8442  grutsk  8444  axgroth5  8446  axgroth2  8447  grothpw  8448  grothpwex  8449  axgroth6  8450  grothomex  8451  grothac  8452  axgroth3  8453  grothprim  8456  grothtsk  8457  inaprc  8458  nqereu  8553  nqerf  8554  dmrecnq  8592  ltaddnq  8598  genpnnp  8629  genpnmax  8631  genpcl  8632  nqpr  8638  addclprlem1  8640  mulclprlem  8643  distrlem4pr  8650  1idpr  8653  prlem934  8657  ltaddpr  8658  ltexprlem3  8662  ltexprlem4  8663  ltexprlem6  8665  ltexprlem7  8666  prlem936  8671  reclem2pr  8672  reclem3pr  8673  mulasssr  8712  ltsosr  8716  0idsr  8719  1idsr  8720  ltasr  8722  recexsrlem  8725  mulgt0sr  8727  supsrlem  8733  ltresr  8762  axmulass  8779  axrrecex  8785  axpre-lttri  8787  wuncn  8792  renfdisj  8885  wloglei  9305  lbinfm  9707  supmul1  9719  supmullem1  9720  supmullem2  9721  supmul  9722  dfinfmr  9731  infmsup  9732  infmrgelb  9734  infmrlb  9735  dfnn2  9759  dflt2  10482  xrinfmss2  10629  infmxrgelb  10653  xrinfm0  10655  fzpr  10840  uzrdgfni  11021  axdc4uzlem  11044  axdc4uz  11045  seqval  11057  seqfeq4  11095  serle  11101  seqof  11103  hashxplem  11385  hashmap  11387  hashpw  11388  hashfun  11389  hashbclem  11390  hashfacen  11392  hashf1lem1  11393  hashf1lem2  11394  hashf1  11395  fz1isolem  11399  ccatfn  11427  wrdexb  11449  wrdind  11477  shftfval  11565  shftfib  11567  shftfn  11568  2shfti  11575  sqrlem6  11733  rexfiuz  11831  rlimdm  12025  fclim  12027  climshft  12050  fsum2dlem  12233  fsumcom2  12237  fsum0diag2  12245  fsumabs  12259  fsumrlim  12269  fsumo1  12270  fsumiun  12279  incexclem  12295  isumltss  12307  supcvg  12314  xpnnenOLD  12488  rpnnen2lem11  12503  algrf  12743  isprm2lem  12765  isprm2  12766  prmind2  12769  iserodd  12888  4sqlem12  13003  vdwmc  13025  vdwlem10  13037  vdwlem13  13040  ramtlecl  13047  hashbc0  13052  ramval  13055  ramcl2lem  13056  ramub2  13061  0ram  13067  ram0  13069  ramub1lem1  13073  ramub1lem2  13074  ramub1  13075  restfn  13329  elrest  13332  restsspw  13336  prdsval  13355  prdsle  13361  prdsless  13362  prdsleval  13376  pwsle  13391  imasaddfnlem  13430  imasvscafn  13439  imasleval  13443  xpsc0  13462  xpsc1  13463  xpsfrnel2  13467  ismre  13492  fnmre  13493  ismred  13504  mremre  13506  fnmrc  13509  mrcfval  13510  mrisval  13532  mreexexlem4d  13549  isacs2  13555  mreacs  13560  acsfn  13561  acsfn1  13563  acsfn2  13565  cidffn  13580  comfeq  13609  invsym2  13665  oppcsect2  13677  brssc  13691  sscpwex  13692  isssc  13697  issubc  13712  isfuncd  13739  cofucl  13762  funcres2b  13771  funcpropd  13774  setcmon  13919  catcval  13928  fnxpc  13950  xpcval  13951  xpccatid  13962  curf2ndf  14021  drsdirfi  14072  isdrs2  14073  clatl  14220  odupos  14239  oduposb  14240  oduglb  14243  odulub  14245  posglbd  14253  ipoval  14257  ipolerval  14259  fpwipodrs  14267  ipodrsima  14268  isacs5lem  14272  psdmrn  14316  psssdm2  14324  submacs  14442  pwsdiagmhm  14445  gsumwspan  14468  mulgpropd  14600  subgacs  14652  nsgacs  14653  eqgfval  14665  eqgval  14666  gicsubgen  14742  gaid  14753  gaorb  14761  orbsta  14767  symgval  14771  symgbas  14772  symgplusg  14776  sylow1lem2  14910  sylow2alem1  14928  sylow2alem2  14929  sylow2a  14930  sylow2blem1  14931  sylow2blem2  14932  sylow2blem3  14933  sylow3lem1  14938  sylow3lem3  14940  sylow3lem6  14943  efgval  15026  efgval2  15033  efgrelexlemb  15059  efgcpbllema  15063  efgcpbllemb  15064  vrgpfval  15075  frgpuplem  15081  divsabl  15157  frgpnabllem1  15161  gsumval3  15191  gsumzaddlem  15203  gsumzadd  15204  gsum2d  15223  gsum2d2  15225  gsumcom2  15226  gsumxp  15227  dprdfadd  15255  dprdres  15263  subgdmdprd  15269  dprd2dlem1  15276  dprd2d2  15279  ablfac1eulem  15307  pgpfac1lem5  15314  opprsubg  15418  subrgmre  15569  subsubrg2  15572  subrgpropd  15579  lss1d  15720  lssintcl  15721  lssmre  15723  lssacs  15724  pwsdiaglmhm  15814  islbs3  15908  lbsextlem4  15914  drngnidl  15981  lidldvgen  16007  psrbaglefi  16118  mplcoe1  16209  mplcoe2  16211  ltbval  16213  ltbwe  16214  opsrle  16217  opsrtoslem1  16225  opsrtoslem2  16226  evlslem4  16245  coe1mul2  16346  coe1tm  16349  znleval  16508  cssmre  16593  thlle  16597  pjfval2  16609  istopon  16663  tgval2  16694  bastg  16704  tgdom  16716  distop  16733  indistopon  16738  fctop  16741  cctop  16743  ppttop  16744  epttop  16746  fncld  16759  cldss2  16767  ntreq0  16814  discld  16826  mretopd  16829  toponmre  16830  neisspw  16844  opnnei  16857  tgrest  16890  resttopon  16892  restco  16895  restdis  16909  ordtbas2  16921  ordtcnv  16931  ordtrest2  16934  pnfnei  16950  mnfnei  16951  iscnp2  16969  subbascn  16984  cnntr  17004  cnrest2  17014  cnpresti  17016  cnprest  17017  cnprest2  17018  ist1-3  17077  hausnei2  17081  isnrm2  17086  dishaus  17110  cmpcovf  17118  fincmp  17120  cmpsublem  17126  cmpsub  17127  cmpcld  17129  uncmp  17130  fiuncmp  17131  hauscmplem  17133  cmpfi  17135  dfcon2  17145  consuba  17146  cnconn  17148  uncon  17155  t1conperf  17162  is1stc2  17168  1stcfb  17171  2ndcsb  17175  2ndc1stc  17177  1stcrest  17179  2ndcctbss  17181  2ndcdisj  17182  2ndcomap  17184  2ndcsep  17185  dis2ndc  17186  llyi  17200  nllyi  17201  nlly2i  17202  llynlly  17203  subislly  17207  restnlly  17208  restlly  17209  islly2  17210  llyrest  17211  llyidm  17214  nllyidm  17215  hausllycmp  17220  cldllycmp  17221  lly1stc  17222  dislly  17223  hausmapdom  17226  kgenf  17236  iskgen3  17244  llycmpkgen2  17245  1stckgenlem  17248  1stckgen  17249  kgencn2  17252  txuni2  17260  txbas  17262  eltx  17263  ptpjpre1  17266  ptuni2  17271  ptpjcn  17305  ptpjopn  17306  ptclsg  17309  dfac14  17312  xkoccn  17313  txcnp  17314  txcnmpt  17318  prdstopn  17322  txrest  17325  txdis  17326  txindis  17328  txdis1cn  17329  txlly  17330  txnlly  17331  pthaus  17332  txcmplem1  17335  txcmplem2  17336  hausdiag  17339  txlm  17342  tx1stc  17344  tx2ndc  17345  txkgen  17346  xkopt  17349  xkococnlem  17353  xkococn  17354  cnmpt1st  17362  cnmpt2nd  17363  xkofvcn  17378  xkoinjcn  17381  txcon  17383  qtoptop2  17390  qtopuni  17393  basqtop  17402  tgqtop  17403  hmphdis  17487  indishmph  17489  txhmeo  17494  pt1hmeo  17497  ptuncnv  17498  ptunhmeo  17499  xpstopnlem1  17500  ptcmpfi  17504  xkohmeo  17506  isfbas  17524  isfbas2  17530  fbssfi  17532  trfbas2  17538  isfild  17553  snfil  17559  elfg  17566  fgcl  17573  filcon  17578  fbasrn  17579  filuni  17580  trfil2  17582  cfinfil  17588  csdfil  17589  supfil  17590  zfbas  17591  isufil2  17603  filssufilg  17606  acufl  17612  filufint  17615  uffix  17616  ufinffr  17624  ufildr  17626  fin1aufil  17627  rnelfmlem  17647  rnelfm  17648  fmfnfmlem3  17651  fmfnfmlem4  17652  fmfnfm  17653  ufldom  17657  flimrest  17678  hauspwpwf1  17682  txflf  17701  fclsrest  17719  fclscmp  17725  alexsubb  17740  alexsubALTlem1  17741  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  ptcmplem2  17747  ptcmplem3  17748  ptcmplem4  17749  ptcmplem5  17750  tmdgsum  17778  symgtgp  17784  cldsubg  17793  tgpconcomp  17795  divstgplem  17803  divstgphaus  17805  prdstmdd  17806  tsmsval2  17812  tsmssubm  17825  imasdsf1olem  17937  xpsdsval  17945  xmetec  17980  prdsbl  18037  stdbdxmet  18061  met1stc  18067  prdsxmslem2  18075  dscopn  18096  xrtgioo  18312  xrsblre  18317  icccmplem1  18327  icccmplem2  18328  fsumcn  18374  fsum2cn  18375  cnllycmp  18454  isphtpc  18492  pi1blem  18537  iscmet3  18719  metcld2  18732  bcthlem4  18749  minveclem3b  18792  ovolfiniun  18860  ovoliunlem1  18861  ovoliunlem2  18862  finiunmbl  18901  volfiniun  18904  iundisj2  18906  uniioombllem3  18940  vitalilem2  18964  vitalilem3  18965  vitali  18968  mbfimaopnlem  19010  itg1addlem4  19054  mbfi1fseqlem4  19073  mbfi1fseqlem6  19075  itgfsum  19181  ellimc2  19227  limcflf  19231  perfdvf  19253  dvres  19261  dvres2  19262  dvnff  19272  dvcj  19299  dvrec  19304  dvmptfsum  19322  dvef  19327  rolle  19337  dvivthlem1  19355  dvfsumle  19368  dvfsumabs  19370  dvfsumlem2  19374  dvfsumlem3  19375  ftc1cn  19390  mpfind  19428  pf1ind  19438  vieta1lem2  19691  elqaalem2  19700  ulmdv  19780  logfac  19954  xrlimcnp  20263  jensenlem1  20281  jensenlem2  20282  jensen  20283  wilthlem2  20307  prmorcht  20416  lgsquadlem1  20593  lgsquadlem2  20594  dchrisumlema  20637  dchrisumlem3  20640  ex-natded9.26  20806  nvss  21149  vsfval  21191  h2hlm  21560  axhcompl-zf  21578  hlim2  21771  hhcmpl  21779  hhcms  21782  shex  21791  isch2  21803  helch  21823  hhsscms  21856  occl  21883  chintcli  21910  dfch2  21986  spanuni  22123  spansni  22136  elnlfn  22508  nmopun  22594  nlelchi  22641  cnlnssadj  22660  adjbd1o  22665  branmfn  22685  pjnmopi  22728  hmopidmchi  22731  abrexss  23040  ballotlem2  23047  ballotlemsf1o  23072  ballotlemirc  23090  iuninc  23158  suppss2f  23201  fmptdF  23221  fmptcof2  23229  funcnvmptOLD  23234  funcnvmpt  23235  tpr2rico  23296  ctex  23336  disjabrex  23359  disjabrexf  23360  disjpreima  23361  iundisj2fi  23364  iundisj2f  23366  disjdsct  23369  ishashinf  23389  esumel  23426  esum0  23428  esumc  23430  esumcst  23436  esumpfinvalf  23444  hasheuni  23453  sigaex  23470  sigaval  23471  isrnsigaOLD  23473  pwsiga  23491  sigainb  23497  insiga  23498  dmsigagen  23505  measbase  23528  ismeas  23530  isrnmeas  23531  measiuns  23544  measdivcstOLD  23551  measdivcst  23552  cntmeas  23553  mbfmco2  23570  mbfmcnt  23573  br2base  23574  coinfliplem  23679  dmgmseqn0  23696  derangenlem  23702  subfacp1lem1  23710  subfacp1lem3  23713  subfacp1lem4  23714  subfacp1lem5  23715  erdszelem7  23728  erdszelem8  23729  erdsze2lem2  23735  kur14lem9  23745  ptpcon  23764  indispcon  23765  conpcon  23766  cnllyscon  23776  rellyscon  23782  cvmsss2  23805  cvmcov2  23806  cvmliftlem15  23829  cvmlift2lem1  23833  cvmlift2lem12  23845  umgraex  23875  eupath  23905  ghomgrplem  23996  relexpindlem  24036  rtrclreclem.trans  24043  dfrtrcl2  24045  untsucf  24056  dftr6  24107  coepr  24109  dffr5  24110  dfso2  24111  dfpo2  24112  br8  24113  br6  24114  br4  24115  dfres3  24116  cnvco1  24117  cnvco2  24118  eldm3  24119  fundmpss  24122  fprb  24129  dfdm5  24132  dfrn5  24133  setinds  24134  dfon2lem1  24139  dfon2lem3  24141  dfon2lem6  24144  dfon2lem7  24145  dfon2lem8  24146  dfon2  24148  rdgprc  24151  dfrdg2  24152  predreseq  24179  predpo  24184  predbrg  24186  setlikespec  24187  predep  24192  preddowncl  24196  preduz  24200  predfz  24203  tz6.26  24205  trpredrec  24241  poseq  24253  soseq  24254  wfrlem5  24260  wfrlem10  24265  wfrlem12  24267  wfrlem13  24268  wfrlem14  24269  wfrlem16  24271  tfrALTlem  24276  frrlem5  24285  frrlem11  24293  sltsolem1  24322  nofulllem5  24360  txpss3v  24418  brtxp  24420  brtxp2  24421  pprodss4v  24424  brpprod  24425  brpprod3a  24426  brpprod3b  24427  brsset  24429  idsset  24430  dfon3  24432  brtxpsd  24434  brbigcup  24438  dfbigcup2  24439  fobigcup  24440  elfix  24443  elfix2  24444  dffix2  24445  fixcnv  24448  limitssson  24451  dfom5b  24452  dffun10  24453  elfuns  24454  elfunsg  24455  elsingles  24457  fnsingle  24458  fvsingle  24459  dfiota3  24462  brimage  24465  brimageg  24466  funimage  24467  fnimage  24468  imageval  24469  brcart  24471  brdomaing  24474  brrangeg  24475  brimg  24476  brapply  24477  brcup  24478  brcap  24479  brsuccf  24480  funpartfun  24481  funpartfv  24483  fullfunfv  24485  brrestrict  24487  dfrdg4  24488  tfrqfree  24489  altopelaltxp  24510  altxpsspw  24511  brsegle  24731  fvline  24767  liness  24768  ellines  24775  bpoly2  24792  bpoly3  24793  rankung  24796  ranksng  24797  rankelg  24798  rankpwg  24799  rankeq1o  24801  elhf2g  24806  hfext  24813  onsucconi  24876  areacirclem6  24930  tpssg  24932  fatesg  24956  eqvinopb  24965  copsexgb  24966  elo  25041  stcat  25044  splint  25048  domfldrefc  25057  ranfldrefc  25058  domrngref  25060  domintrefb  25063  restidsing  25076  prj1b  25079  prj3  25080  eloi  25086  elintabg  25090  domintrefc  25125  inttpemp  25139  mapmapmap  25148  injsurinj  25149  npincppr  25159  repfuntw  25160  repcpwti  25161  cbcpcp  25162  cbicp  25166  prjmapcp2  25170  dstr  25171  iscst4  25177  islatalg  25183  domrancur1c  25202  mnlmxl2  25269  defse3  25272  inpc  25277  inposet  25278  tolat  25286  toplat  25290  dfdir2  25291  prodeq3ii  25308  fprodser  25320  symgfo  25368  svs2  25487  inttop2  25515  sallnei  25529  nsn  25530  dmhmph  25533  rnhmph  25534  intopcoaconlem3b  25538  intopcoaconlem3  25539  qusp  25542  efilcp  25552  fgsb2  25555  bwt2  25592  dmrngcmp  25751  dualded  25783  ishomd  25790  vtarsuelt  25895  fnctartar  25907  fnctartar2  25908  dfiunv2  25916  prismorcset2  25918  domcatfun  25925  codcatfun  25934  idcatfun  25941  empklst  26009  fnckle  26045  pfsubkl  26047  pgapspf2  26053  isconcl5a  26101  isconcl5ab  26102  bosser  26167  pdiveql  26168  abhp2  26175  bhp2a  26176  cnvresimaOLD  26226  trer  26227  finminlem  26231  gtinf  26234  fneer  26288  fnessref  26293  refssfne  26294  islocfin  26296  comppfsc  26307  neibastop1  26308  neibastop2lem  26309  neibastop3  26311  topmeet  26313  topjoin  26314  neifg  26320  tailfb  26326  filnetlem2  26328  filnetlem3  26329  filnetlem4  26330  cover2g  26359  f1opr  26391  inixp  26399  indexdom  26413  frinfm  26416  sdclem2  26452  sdclem1  26453  fdc  26455  isbndx  26506  prdstotbnd  26518  heibor1lem  26533  heiborlem1  26535  heiborlem3  26537  heiborlem4  26538  heiborlem5  26539  heiborlem6  26540  heiborlem8  26542  heiborlem10  26544  ismrer1  26562  riscer  26619  divrngidl  26653  intidl  26654  isfldidl  26693  ispridlc  26695  prtlem10  26733  prtlem13  26736  prtlem16  26737  prtlem19  26746  prter2  26749  prter3  26750  ralxpmap  26761  elrfi  26769  ismrcd1  26773  ismrcd2  26774  istopclsd  26775  ismrc  26776  mrefg2  26782  isnacs3  26785  mzpclall  26805  mzpincl  26812  mzpsubst  26826  mzpcompact2lem  26829  mzpcompact2  26830  eldioph2lem1  26839  eldioph2lem2  26840  eldiophss  26854  diophrex  26855  rexrabdioph  26875  2rexfrabdioph  26877  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  rabren3dioph  26898  fphpd  26899  rencldnfilem  26903  pellexlem5  26918  pellex  26920  rmxypairf1o  26996  monotuz  27026  monotoddzzfi  27027  oddcomabszz  27029  2nn0ind  27030  zindbi  27031  mzpcong  27059  rmydioph  27107  rmxdioph  27109  expdiophlem2  27115  setindtr  27117  setindtrs  27118  dford3lem2  27120  ttac  27129  pw2f1ocnv  27130  wepwsolem  27138  inisegn0  27140  dnnumch1  27141  fnwe2val  27146  fnwe2lem2  27148  aomclem1  27151  aomclem2  27152  aomclem6  27156  dfac11  27160  kelac2lem  27162  dfac21  27164  islssfg2  27169  lmhmlnmsplit  27185  pwssplit3  27190  filnm  27192  pwslnmlem1  27194  pwslnm  27196  dsmmval  27200  frlmlbs  27249  unxpwdom3  27256  enfixsn  27257  dfacbasgrp  27273  islindf4  27308  lmisfree  27312  lnr2i  27320  lnrfg  27323  hbtlem6  27333  rngunsnply  27378  pmtrfval  27393  symggen  27411  gsumcom3  27454  acsfn1p  27507  sdrgacs  27509  idomsubgmo  27514  fgraphxp  27530  expgrowth  27552  2sbc6g  27615  iotain  27617  compel  27640  ipo0  27652  ifr0  27653  fnchoice  27700  infrglb  27722  stoweidlem31  27780  stoweidlem57  27806  stoweidlem62  27811  stirlinglem13  27835  funressnfv  27991  dfdfat2  27994  csbafv12g  28000  tz6.12-afv  28035  csbaovg  28040  isusgra0  28106  usgraexmpl  28133  isuvtx  28160  uvtx01vtx  28164  frgra3vlem1  28178  frgra3vlem2  28179  3vfriswmgralem  28182  onfrALTlem5  28307  onfrALTlem4  28308  onfrALTlem3  28309  opelopab4  28317  a9e2nd  28324  trsspwALT  28592  trsspwALT2  28593  trsspwALT3  28594  pwtrVD  28598  pwtrOLD  28599  unipwrVD  28608  unipwr  28609  onfrALTlem5VD  28661  onfrALTlem4VD  28662  onfrALTlem3VD  28663  relopabVD  28677  a9e2ndVD  28684  sspwimp  28694  sspwimpVD  28695  sspwimpcf  28696  sspwimpcfVD  28697  sspwimpALT  28701  sspwimpALT2  28705  a9e2ndALT  28707  bnj23  28744  bnj62  28746  bnj156  28756  bnj219  28761  bnj610  28776  bnj918  28796  bnj927  28800  bnj976  28809  bnj1098  28815  bnj1379  28863  bnj110  28890  bnj98  28899  bnj154  28910  bnj155  28911  bnj535  28922  bnj556  28932  bnj557  28933  bnj581  28940  bnj591  28943  bnj594  28944  bnj580  28945  bnj607  28948  bnj609  28949  bnj600  28951  bnj849  28957  bnj893  28960  bnj908  28963  bnj934  28967  bnj944  28970  bnj964  28975  bnj966  28976  bnj969  28978  bnj970  28979  bnj910  28980  bnj986  28986  bnj999  28989  bnj1018  28994  bnj907  28997  bnj1039  29001  bnj1040  29002  bnj1052  29005  bnj1123  29016  bnj1030  29017  bnj1133  29019  bnj1128  29020  bnj1145  29023  bnj1204  29042  bnj1373  29060  bnj1417  29071  bnj1421  29072  bnj1498  29091  eqlkr2  29290  glbconxN  29567  pmapglbx  29958  pmapglb  29959  pclclN  30080  pclfinN  30089  polval2N  30095  pclfinclN  30139  osumcllem10N  30154  pexmidlem7N  30165  cdleme31sdnN  30576  cdlemefr44  30614  cdleme48fv  30688  cdleme46fvaw  30690  cdleme48bw  30691  cdleme46fsvlpq  30694  cdlemeg46fvcl  30695  cdlemeg49le  30700  cdlemeg46fjgN  30710  cdlemeg46fjv  30712  cdleme48d  30724  cdlemeg49lebilem  30728  cdleme50eq  30730  cdleme50f  30731  cdlemg2jlemOLDN  30782  cdlemg2klem  30784  cdlemk40  31106  cdlemk56  31160  diaglbN  31245  dvhlveclem  31298  dib1dim  31355  dibglbN  31356  diblss  31360  diblsmopel  31361  dicelvalN  31368  diclspsn  31384  cdlemn7  31393  dihordlem7  31404  dihopelvalcpre  31438  xihopellsmN  31444  dihopellsm  31445  dih1  31476  dihmeetlem1N  31480  dihglblem5apreN  31481  dihmeetlem2N  31489  dihglbcpreN  31490  dihmeetlem4preN  31496  dihmeetlem13N  31509  dih1dimatlem  31519  dihatlat  31524  dihjatcclem4  31611  lcdlss  31809
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790
  Copyright terms: Public domain W3C validator