Theorem vex 2927

Description: All set variables are sets (see isset 2928). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
vex	|- x e. _V

Proof of Theorem vex

Step	Hyp	Ref	Expression
1		equid 1684	. 2 |- x = x
2		df-v 2926	. . 3 |- _V = { x | x = x }
3	2	abeq2i 2519	. 2 |- ( x e. _V <-> x = x )
4	1, 3	mpbir 201	1 |- x e. _V

Syntax hints:   e. wcel 1721   _Vcvv 2924

This theorem is referenced by:  isset  2928  ralv  2937  rexv  2938  reuv  2939  rmov  2940  rabab  2941  sbhypf  2969  ceqex  3034  ralab  3063  rexab  3065  moeq3  3079  mo2icl  3081  reu8  3098  sbc2or  3137  csbvarg  3246  csbiebg  3258  sbcnestgf  3266  sbnfc2  3277  ddif  3447  csbing  3516  dfun2  3544  dfin2  3545  vn0  3603  eqv  3611  abvor0  3613  sbss  3705  csbifg  3735  ifexg  3766  elpwg  3774  exsnrex  3816  dftp2  3822  prnzg  3892  snssg  3900  difprsnss  3902  sneqrg  3936  preq12bg  3945  pwpr  3979  pwtp  3980  pwv  3982  unipr  3997  uniprg  3998  unisng  4000  elintg  4026  elintrabg  4031  intss1  4033  ssint  4034  intmin  4038  intss  4039  intssuni  4040  intmin4  4047  intab  4048  intun  4050  intpr  4051  intprg  4052  uniintsn  4055  iinconst  4070  iuniin  4071  iinss1  4073  dfiin2g  4092  dfiunv2  4095  ssiinf  4108  iinss  4110  iinss2  4111  0iin  4117  iinab  4120  iinun2  4125  iundif2  4126  iindif2  4128  iinin2  4129  iinuni  4142  sspwuni  4144  iinpw  4147  iunpwss  4148  brab1  4225  csbopabg  4251  mptv  4269  trint  4285  trintss  4286  vprc  4309  inex1g  4314  ssexg  4317  intex  4324  inuni  4330  axpweq  4344  pwexg  4351  pwuni  4363  axpr  4370  zfpair2  4372  elALT  4375  rext  4380  sspwb  4381  unipw  4382  ssextss  4385  nnullss  4393  exss  4394  opth  4403  opthg  4404  copsexg  4410  copsex4g  4413  moop2  4419  euotd  4425  opelopabsbOLD  4431  opelopabsb  4433  pwin  4455  pwunss  4456  pwssun  4457  epelg  4463  epel  4465  dfid3  4467  pofun  4487  epse  4533  wefrc  4544  tron  4572  onfr  4588  sucel  4622  suctr  4632  uniexg  4673  unexb  4676  snnex  4680  uniuni  4683  eusvnf  4685  eusvnfb  4686  reusv6OLD  4701  iunpw  4726  onint  4742  ordpwsuc  4762  unon  4778  ordunisuc  4779  onuninsuci  4787  orduninsuc  4790  limsssuc  4797  limuni3  4799  tfinds  4806  tfindsg  4807  tfindsg2  4808  tfinds2  4810  dfom2  4814  peano5  4835  finds  4838  findsg  4839  finds2  4840  0nelxp  4873  opelxp  4875  opeliunxp  4896  elvv  4903  elvvv  4904  elvvuni  4905  xpsspw  4953  xpsspwOLD  4954  relopabi  4967  opabid2  4971  difopab  4973  xpiindi  4977  ralxpf  4986  relop  4990  cnvco  5023  dfrn2  5026  dfdm4  5030  dmss  5036  dmin  5044  dmiun  5045  dmuni  5046  dm0  5050  dmi  5051  reldm0  5054  elreldm  5061  elrnmpt1  5086  dmrnssfld  5096  dmcoss  5102  dmcosseq  5104  opelresg  5120  resieq  5123  dmres  5134  elres  5148  relssres  5150  resopab  5154  resiexg  5155  iss  5156  dfres2  5160  dfima2  5172  csbima12g  5180  imadmrn  5182  imai  5185  elimasng  5197  args  5199  epini  5201  iniseg  5202  dffr3  5203  dfse2  5204  exse2  5205  cotr  5213  issref  5214  cnvsym  5215  intasym  5216  asymref  5217  asymref2  5218  intirr  5219  brcodir  5220  codir  5221  qfto  5222  poirr2  5225  cnvopab  5241  cnv0  5242  cnvi  5243  cnvdif  5245  rniun  5249  dminss  5253  imainss  5254  inimasn  5256  ssrnres  5276  rninxp  5277  dminxp  5278  cnvcnv3  5287  dfrel2  5288  dmsnn0  5302  dmsnopg  5308  cnvcnvsn  5314  dmsnsnsn  5315  cnvsng  5322  elxp4  5324  elxp5  5325  cnvresima  5326  dfco2  5336  dfco2a  5337  cores  5340  resco  5341  imaco  5342  rnco  5343  coiun  5346  co02  5350  coi1  5352  coass  5355  relssdmrn  5357  unielrel  5361  unixp0  5370  ressn  5375  cnviin  5376  cnvpo  5377  cnvso  5378  uniabio  5395  iotaval  5396  sniota  5412  csbiotag  5414  dffun2  5431  dffun7  5446  dffun8  5447  dffun9  5448  funopg  5452  funssres  5460  funun  5462  funcnvsn  5463  funcnv2  5477  funcnv  5478  funcnv3  5479  fun2cnv  5480  funcnvuni  5485  imadif  5495  isarep1  5499  2elresin  5523  fnres  5528  fcnvres  5587  fabexg  5591  fconstg  5597  fun11iun  5662  f1osng  5683  dffv3  5691  fv3  5711  fvres  5712  nfunsn  5728  funimass4  5744  ssimaexg  5756  dffv2  5763  dmfco  5764  fvopab6  5793  fndmdif  5801  iinpreima  5827  fvelrn  5833  dff3  5849  dffo4  5852  exfo  5854  f1ompt  5858  fmptco  5868  fsng  5874  dfmpt  5878  fnressn  5885  fressnfv  5887  fvsng  5894  fnpr  5917  fnprOLD  5918  zfrep6  5935  funfvima3  5942  idref  5946  fvclss  5947  fvresex  5949  abrexco  5953  opabex3d  5956  opabex3  5957  imaiun  5959  dff13  5971  foeqcnvco  5994  f1eqcocnv  5995  fliftcnv  6000  isocnv2  6018  isomin  6024  isoini  6025  isofr  6029  isose  6030  f1oweALT  6041  wemoiso  6045  wemoiso2  6046  knatar  6047  oprabid  6072  csbovg  6079  0neqopab  6086  eloprabga  6127  mpt2v  6130  caovmo  6251  f1opw  6266  ofmres  6310  op1stg  6326  op2ndg  6327  1stval2  6331  2ndval2  6332  fo1st  6333  fo2nd  6334  f1stres  6335  f2ndres  6336  fo1stres  6337  fo2ndres  6338  1st2val  6339  2nd2val  6340  xp1st  6343  xp2nd  6344  sbcopeq1a  6366  csbopeq1a  6367  eloprabi  6380  mpt2mptsx  6381  dmmpt2ssx  6383  fmpt2x  6384  ovmptss  6395  fmpt2co  6397  df1st2  6400  df2nd2  6401  1stconst  6402  2ndconst  6403  curry1  6405  curry2  6408  fparlem1  6413  fparlem2  6414  fpar  6417  fsplit  6418  fo2ndf  6420  f1o2ndf1  6421  frxp  6423  xporderlem  6424  soxp  6426  fnwelem  6428  fnse  6430  reldmtpos  6454  dmtpos  6458  rntpos  6459  ovtpos  6461  dftpos3  6464  dftpos4  6465  tpostpos  6466  porpss  6493  sorpss  6494  sorpsscmpl  6500  opiota  6502  opabiotafun  6503  opabiota  6505  riotav  6521  csbriotag  6529  onovuni  6571  smogt  6596  tfrlem3  6605  tfrlem8  6612  tfrlem9a  6614  tfrlem16  6621  tz7.44lem1  6630  rdg0g  6652  rdglim2  6657  tz7.48-1  6667  seqomlem1  6674  seqomlem2  6675  abianfplem  6682  oacl  6746  omcl  6747  oecl  6748  oa0r  6749  om0r  6750  om1r  6753  oe1m  6755  oaordi  6756  oawordri  6760  oawordeulem  6764  oalimcl  6770  oaass  6771  oarec  6772  omordi  6776  omwordri  6782  omlimcl  6788  odi  6789  omass  6790  omeulem1  6792  oen0  6796  oeordi  6797  oewordri  6802  oeworde  6803  oeoalem  6806  oeoelem  6808  nnawordex  6847  omabs  6857  omsmolem  6863  ercnv  6893  iserd  6898  eqerlem  6904  eqer  6905  ecdmn0  6914  erth  6916  erdisj  6919  qsss  6932  ecid  6936  qsid  6937  iiner  6943  qsel  6950  erovlem  6967  ecopovsym  6973  ecopovtrn  6974  ecopover  6975  mapprc  6989  fnmap  6992  fnpm  6993  mapval2  7010  pmsspw  7015  mapsn  7022  mapsncnv  7027  ixpconstg  7038  ixpprc  7050  uniixp  7052  ixpin  7054  ixpiin  7055  resixpfo  7067  elixpsn  7068  ixpsnf1o  7069  boxriin  7071  boxcutc  7072  bren  7084  brdomg  7085  domen  7088  domeng  7089  idssen  7119  ener  7121  domtr  7127  ensn1g  7139  en1  7141  en1b  7142  fundmen  7147  fundmeng  7148  mapsnen  7151  unen  7156  domdifsn  7158  xpsnen  7159  xpsneng  7160  xpcomeng  7167  xpassen  7169  xpdom2  7170  xpdom2g  7171  domunsncan  7175  omxpenlem  7176  pw2f1o  7180  sbthlem10  7193  sbth  7194  sbthcl  7196  domunsn  7224  fodomr  7225  pwdom  7226  canth2  7227  canth2g  7228  domssex  7235  xpf1o  7236  mapen  7238  mapunen  7243  map2xp  7244  mapdom2  7245  mapdom3  7246  ssenen  7248  infensuc  7252  nneneq  7257  php  7258  php2  7259  php3  7260  sucdom2  7270  1sdom  7278  unxpdomlem2  7281  unxpdomlem3  7282  isinf  7289  fineqvlem  7290  fineqv  7291  pssnn  7294  ssfi  7296  dif1enOLD  7307  dif1en  7308  findcard  7314  findcard2  7315  findcard2s  7316  ac6sfi  7318  frfi  7319  fimax2g  7320  unbnn2  7331  isfinite2  7332  xpfi  7345  domunfican  7346  fiint  7350  fodomfi  7352  fodomfib  7353  iunfi  7361  pwfilem  7367  ixpfi2  7371  fissuni  7377  fipreima  7378  finsschain  7379  fival  7383  ssfii  7390  fi0  7391  fiin  7393  dffi2  7394  fipwuni  7397  fisn  7398  elfiun  7401  dffi3  7402  fifo  7403  marypha1lem  7404  dfsup2  7413  dfsup2OLD  7414  ordiso2  7448  oismo  7473  hartogslem1  7475  hartogs  7477  wofib  7478  wemappo  7482  wemapso2lem  7483  card2on  7486  brwdom  7499  brwdomn0  7501  brwdom2  7505  wdomtr  7507  wdompwdom  7510  canthwdom  7511  xpwdomg  7517  unxpwdom2  7520  ixpiunwdom  7523  elirrv  7529  zfregfr  7534  inf0  7540  inf3lema  7543  inf3lemd  7546  inf3lem1  7547  inf3lem2  7548  inf3lem3  7549  inf3lem5  7551  inf3lem6  7552  inf3lem7  7553  inf3  7554  infeq5  7556  omex  7562  dfom3  7566  dfom5  7569  infdifsn  7575  cantnfdm  7583  cantnfval  7587  cantnfval2  7588  cantnflt  7591  cantnff  7593  oemapso  7602  cantnflem1  7609  wemapwe  7618  cnfcom  7621  cnfcom3clem  7626  epfrs  7631  tcvalg  7641  tctr  7643  tcmin  7644  r1sdom  7664  r1val1  7676  tz9.12lem1  7677  tz9.12lem3  7679  tz9.13  7681  tz9.13g  7682  rankf  7684  unir1  7703  rankvalg  7707  rankonidlem  7718  r1val2  7727  bndrank  7731  ranklim  7734  r1pwOLD  7736  rankunb  7740  rankuni2b  7743  rankuni  7753  rankval4  7757  rankxplim  7767  rankxplim3  7769  rankxpsuc  7770  tcrank  7772  cp  7779  bnd2  7781  kardex  7782  karden  7783  cardf2  7794  tskwe  7801  cardlim  7823  harcard  7829  cardiun  7833  pm54.43  7851  r0weon  7858  infxpenlem  7859  infxpenc2lem2  7865  fseqenlem1  7869  fseqenlem2  7870  fseqen  7872  dfac8alem  7874  dfac8clem  7877  ac10ct  7879  ween  7880  acnlem  7893  finacn  7895  acndom  7896  acndom2  7899  wdomfil  7906  infpwfien  7907  alephon  7914  alephcard  7915  alephordi  7919  cardaleph  7934  alephval3  7955  iunfictbso  7959  aceq3lem  7965  dfac3  7966  dfac4  7967  dfac5lem1  7968  dfac5lem2  7969  dfac5lem3  7970  dfac5lem4  7971  dfac5lem5  7972  dfac5  7973  dfac2a  7974  dfac2  7975  dfac8  7979  dfac9  7980  dfac10b  7983  acacni  7984  dfacacn  7985  dfac13  7986  kmlem1  7994  kmlem2  7995  kmlem9  8002  kmlem10  8003  kmlem11  8004  kmlem12  8005  kmlem13  8006  cdafn  8013  pwsdompw  8048  infmap2  8062  ackbij1lem5  8068  ackbij1lem8  8071  ackbij2  8087  cflm  8094  cardcf  8096  cfeq0  8100  cfsuc  8101  cff1  8102  cfflb  8103  cfval2  8104  cflim2  8107  cfss  8109  cfslb2n  8112  cofsmo  8113  cfsmolem  8114  cfcoflem  8116  coftr  8117  sornom  8121  infpssr  8152  fin4en1  8153  enfin2i  8165  fin23lem26  8169  fin23lem14  8177  fin23lem16  8179  fin23lem17  8182  fin23lem21  8183  fin23lem32  8188  fin23lem34  8190  fin23lem39  8194  compsscnvlem  8214  compssiso  8218  isf34lem4  8221  enfin1ai  8228  isfin1-3  8230  fin67  8239  dffin7-2  8242  fin1a2lem7  8250  fin1a2lem10  8253  fin1a2lem12  8255  fin1a2lem13  8256  fin12  8257  itunitc1  8264  itunitc  8265  ituniiun  8266  hsmexlem2  8271  hsmexlem4  8273  hsmex  8276  axcc2lem  8280  axcc3  8282  acncc  8284  fin41  8288  dominf  8289  dcomex  8291  axdc2lem  8292  axdc3lem  8294  axdc3lem2  8295  axdc3lem4  8297  axdc4lem  8299  axcclem  8301  ac9  8327  ac6s  8328  ac6sg  8332  ac9s  8337  numthcor  8338  zorn2lem1  8340  zorn2lem4  8343  zorn2lem7  8346  zorng  8348  zornn0g  8349  ttukeylem5  8357  ttukeylem6  8358  ttukeylem7  8359  axdclem  8363  axdclem2  8364  fodomg  8367  fodomb  8368  brdom3  8370  brdom5  8371  brdom4  8372  brdom7disj  8373  brdom6disj  8374  iunfo  8378  ondomon  8402  cardmin  8403  alephval2  8411  dominfac  8412  fpwwe2lem1  8470  fpwwe2lem8  8476  fpwwe2lem11  8479  fpwwe2lem12  8480  fpwwe2lem13  8481  fpwwe2  8482  fpwwe  8485  canthwe  8490  canthp1lem1  8491  pwfseqlem1  8497  pwfseqlem2  8498  pwfseqlem3  8499  pwfseqlem4a  8500  pwfseqlem5  8502  pwxpndom2  8504  gchac  8512  gch2  8518  inawinalem  8528  winainflem  8532  winalim2  8535  winafp  8536  gchina  8538  wunfi  8560  intwun  8574  wunex2  8577  uniwun  8579  eltsk2g  8590  inttsk  8613  inar1  8614  rankcf  8616  tskcard  8620  tskuni  8622  gruun  8645  intgru  8653  ingru  8654  wfgru  8655  grudomon  8656  gruina  8657  grur1a  8658  grur1  8659  grutsk  8661  axgroth5  8663  axgroth2  8664  grothpw  8665  grothpwex  8666  axgroth6  8667  grothomex  8668  grothac  8669  axgroth3  8670  grothprim  8673  grothtsk  8674  inaprc  8675  nqereu  8770  nqerf  8771  dmrecnq  8809  ltaddnq  8815  genpnnp  8846  genpnmax  8848  genpcl  8849  nqpr  8855  addclprlem1  8857  mulclprlem  8860  distrlem4pr  8867  1idpr  8870  prlem934  8874  ltaddpr  8875  ltexprlem3  8879  ltexprlem4  8880  ltexprlem6  8882  ltexprlem7  8883  prlem936  8888  reclem2pr  8889  reclem3pr  8890  mulasssr  8929  ltsosr  8933  0idsr  8936  1idsr  8937  ltasr  8939  recexsrlem  8942  mulgt0sr  8944  supsrlem  8950  ltresr  8979  axmulass  8996  axrrecex  9002  axpre-lttri  9004  wuncn  9009  renfdisj  9102  wloglei  9523  lbinfm  9925  supmul1  9937  supmullem1  9938  supmullem2  9939  supmul  9940  dfinfmr  9949  infmsup  9950  infmrgelb  9952  infmrlb  9953  dfnn2  9977  dflt2  10705  xrinfmss2  10853  infmxrgelb  10877  xrinfm0  10879  fzpr  11065  uzrdgfni  11261  axdc4uzlem  11284  axdc4uz  11285  seqval  11297  seqfeq4  11335  serle  11341  seqof  11343  hash1snb  11644  hash2prde  11651  hash2prb  11652  hashxplem  11659  hashmap  11661  hashpw  11662  hashfun  11663  hashbclem  11664  hashfacen  11666  hashf1lem1  11667  hashf1lem2  11668  hashf1  11669  fz1isolem  11673  brfi1uzind  11678  ccatfn  11704  wrdexb  11726  wrdind  11754  shftfval  11848  shftfib  11850  shftfn  11851  2shfti  11858  sqrlem6  12016  rexfiuz  12114  rlimdm  12308  fclim  12310  climshft  12333  fsum2dlem  12517  fsumcom2  12521  fsum0diag2  12529  fsumabs  12543  fsumrlim  12553  fsumo1  12554  fsumiun  12563  incexclem  12579  isumltss  12591  supcvg  12598  xpnnenOLD  12772  rpnnen2lem11  12787  algrf  13027  isprm2lem  13049  isprm2  13050  prmind2  13053  iserodd  13172  4sqlem12  13287  vdwmc  13309  vdwlem10  13321  vdwlem13  13324  ramtlecl  13331  hashbc0  13336  ramval  13339  ramcl2lem  13340  ramub2  13345  0ram  13351  ram0  13353  ramub1lem1  13357  ramub1lem2  13358  ramub1  13359  restfn  13615  elrest  13618  restsspw  13622  prdsval  13641  prdsle  13647  prdsless  13648  prdsleval  13662  pwsle  13677  imasaddfnlem  13716  imasvscafn  13725  imasleval  13729  xpsc0  13748  xpsc1  13749  xpsfrnel2  13753  ismre  13778  fnmre  13779  ismred  13790  mremre  13792  fnmrc  13795  mrcfval  13796  mrisval  13818  mreexexlem4d  13835  isacs2  13841  mreacs  13846  acsfn  13847  acsfn1  13849  acsfn2  13851  cidffn  13866  comfeq  13895  invsym2  13951  oppcsect2  13963  brssc  13977  sscpwex  13978  isssc  13983  issubc  13998  isfuncd  14025  cofucl  14048  funcres2b  14057  funcpropd  14060  setcmon  14205  catcval  14214  fnxpc  14236  xpcval  14237  xpccatid  14248  curf2ndf  14307  drsdirfi  14358  isdrs2  14359  clatl  14506  odupos  14525  oduposb  14526  oduglb  14529  odulub  14531  posglbd  14539  ipoval  14543  ipolerval  14545  fpwipodrs  14553  ipodrsima  14554  isacs5lem  14558  psdmrn  14602  psssdm2  14610  submacs  14728  pwsdiagmhm  14731  gsumwspan  14754  mulgpropd  14886  subgacs  14938  nsgacs  14939  eqgfval  14951  eqgval  14952  gicsubgen  15028  gaid  15039  gaorb  15047  orbsta  15053  symgval  15057  symgbas  15058  symgplusg  15062  sylow1lem2  15196  sylow2alem1  15214  sylow2alem2  15215  sylow2a  15216  sylow2blem1  15217  sylow2blem2  15218  sylow2blem3  15219  sylow3lem1  15224  sylow3lem3  15226  sylow3lem6  15229  efgval  15312  efgval2  15319  efgrelexlemb  15345  efgcpbllema  15349  efgcpbllemb  15350  vrgpfval  15361  frgpuplem  15367  divsabl  15443  frgpnabllem1  15447  gsumval3  15477  gsumzaddlem  15489  gsumzadd  15490  gsum2d  15509  gsum2d2  15511  gsumcom2  15512  gsumxp  15513  dprdfadd  15541  dprdres  15549  subgdmdprd  15555  dprd2dlem1  15562  dprd2d2  15565  ablfac1eulem  15593  pgpfac1lem5  15600  opprsubg  15704  subrgmre  15855  subsubrg2  15858  subrgpropd  15865  lss1d  16002  lssintcl  16003  lssmre  16005  lssacs  16006  pwsdiaglmhm  16096  lbsextlem4  16196  drngnidl  16263  lidldvgen  16289  psrbaglefi  16400  mplcoe1  16491  mplcoe2  16493  ltbval  16495  ltbwe  16496  opsrle  16499  opsrtoslem1  16507  opsrtoslem2  16508  evlslem4  16527  coe1mul2  16625  coe1tm  16628  znleval  16798  cssmre  16883  thlle  16887  pjfval2  16899  istopon  16953  tgval2  16984  bastg  16994  tgdom  17006  distop  17023  indistopon  17028  fctop  17031  cctop  17033  ppttop  17034  epttop  17036  fncld  17049  cldss2  17057  ntreq0  17104  discld  17116  mretopd  17119  toponmre  17120  neisspw  17134  opnnei  17147  tgrest  17185  resttopon  17187  restco  17190  restdis  17204  neitr  17206  ordtbas2  17217  ordtcnv  17227  ordtrest2  17230  pnfnei  17246  mnfnei  17247  iscnp2  17265  subbascn  17280  cnntr  17301  cnrest2  17312  cnpresti  17314  cnprest  17315  cnprest2  17316  ist1-3  17375  hausnei2  17379  isnrm2  17384  dishaus  17408  cmpcovf  17416  fincmp  17418  cmpsublem  17424  cmpsub  17425  cmpcld  17427  uncmp  17428  fiuncmp  17429  hauscmplem  17431  cmpfi  17433  dfcon2  17443  consuba  17444  cnconn  17446  uncon  17453  t1conperf  17460  is1stc2  17466  1stcfb  17469  2ndcsb  17473  2ndc1stc  17475  1stcrest  17477  2ndcctbss  17479  2ndcdisj  17480  2ndcomap  17482  2ndcsep  17483  dis2ndc  17484  llyi  17498  nllyi  17499  nlly2i  17500  llynlly  17501  subislly  17505  restnlly  17506  restlly  17507  islly2  17508  llyrest  17509  llyidm  17512  nllyidm  17513  hausllycmp  17518  cldllycmp  17519  lly1stc  17520  dislly  17521  hausmapdom  17524  kgenf  17534  iskgen3  17542  llycmpkgen2  17543  1stckgenlem  17546  1stckgen  17547  kgencn2  17550  txuni2  17558  txbas  17560  eltx  17561  ptpjpre1  17564  ptuni2  17569  ptpjcn  17604  ptpjopn  17605  ptclsg  17608  dfac14  17611  xkoccn  17612  txcnp  17613  txcnmpt  17617  prdstopn  17621  txrest  17624  txdis  17625  txindis  17627  txdis1cn  17628  txlly  17629  txnlly  17630  pthaus  17631  txcmplem1  17634  txcmplem2  17635  hausdiag  17638  txlm  17641  tx1stc  17643  tx2ndc  17644  txkgen  17645  xkopt  17648  xkococnlem  17652  xkococn  17653  cnmpt1st  17661  cnmpt2nd  17662  xkofvcn  17677  xkoinjcn  17680  txcon  17682  imasnopn  17683  imasncld  17684  imasncls  17685  qtoptop2  17692  qtopuni  17695  basqtop  17704  tgqtop  17705  hmphdis  17789  indishmph  17791  txhmeo  17796  pt1hmeo  17799  ptuncnv  17800  ptunhmeo  17801  xpstopnlem1  17802  ptcmpfi  17806  xkohmeo  17808  isfbas  17822  isfbas2  17828  fbssfi  17830  trfbas2  17836  isfild  17851  snfil  17857  elfg  17864  fgcl  17871  filcon  17876  fbasrn  17877  filuni  17878  trfil2  17880  cfinfil  17886  csdfil  17887  supfil  17888  zfbas  17889  isufil2  17901  filssufilg  17904  acufl  17910  filufint  17913  uffix  17914  ufildr  17924  fin1aufil  17925  rnelfmlem  17945  rnelfm  17946  fmfnfmlem3  17949  fmfnfmlem4  17950  fmfnfm  17951  ufldom  17955  flimrest  17976  hauspwpwf1  17980  txflf  17999  fclsrest  18017  fclscmp  18023  alexsubb  18038  alexsubALTlem1  18039  alexsubALTlem2  18040  alexsubALTlem3  18041  alexsubALTlem4  18042  alexsubALT  18043  ptcmplem2  18045  ptcmplem3  18046  ptcmplem4  18047  ptcmplem5  18048  cnextf  18058  cnextcn  18059  tmdgsum  18086  symgtgp  18092  cldsubg  18101  tgpconcomp  18103  divstgplem  18111  divstgphaus  18113  prdstmdd  18114  tsmsval2  18120  tsmssubm  18133  ustfn  18192  ustfilxp  18203  ustn0  18211  restutopopn  18229  ustuqtop0  18231  ustuqtop1  18232  ustuqtop2  18233  ustuqtop3  18234  ustuqtop4  18235  utopsnneiplem  18238  utopreg  18243  ucnimalem  18271  ucnima  18272  fmucndlem  18282  neipcfilu  18287  imasdsf1olem  18364  xpsdsval  18372  xmetec  18425  prdsbl  18482  stdbdxmet  18506  met1stc  18512  prdsxmslem2  18520  metustidOLD  18550  metustid  18551  metustsymOLD  18552  metustsym  18553  metustexhalfOLD  18554  metustexhalf  18555  metustfbasOLD  18556  metustfbas  18557  blval2  18566  metuel2  18570  metustblOLD  18571  metustbl  18572  restmetu  18578  dscopn  18582  xrtgioo  18798  xrsblre  18803  icccmplem1  18814  icccmplem2  18815  fsumcn  18861  fsum2cn  18862  cnllycmp  18942  isphtpc  18980  pi1blem  19025  iscmet3  19207  metcld2  19220  bcthlem4  19241  minveclem3b  19290  ovolfiniun  19358  ovoliunlem1  19359  ovoliunlem2  19360  finiunmbl  19399  volfiniun  19402  iundisj2  19404  uniioombllem3  19438  vitalilem2  19462  vitalilem3  19463  vitali  19466  mbfimaopnlem  19508  itg1addlem4  19552  mbfi1fseqlem4  19571  mbfi1fseqlem6  19573  itgfsum  19679  ellimc2  19725  limcflf  19729  perfdvf  19751  dvres  19759  dvres2  19760  dvnff  19770  dvcj  19797  dvrec  19802  dvmptfsum  19820  dvef  19825  rolle  19835  dvivthlem1  19853  dvfsumle  19866  dvfsumabs  19868  dvfsumlem2  19872  dvfsumlem3  19873  ftc1cn  19888  mpfind  19926  pf1ind  19936  vieta1lem2  20189  elqaalem2  20198  ulmdv  20280  logfac  20456  xrlimcnp  20768  jensenlem1  20786  jensenlem2  20787  jensen  20788  wilthlem2  20813  prmorcht  20922  lgsquadlem1  21099  lgsquadlem2  21100  dchrisumlema  21143  dchrisumlem3  21146  umgraex  21319  isusgra0  21337  usgra2edg  21363  usgrarnedg  21365  usgraedg4  21367  usgraedgreu  21368  usgraexmpl  21381  usgrafis  21390  nbgraf1olem5  21416  nb3graprlem1  21421  cusgrarn  21429  cusgrares  21442  cusgrasize  21448  cusgrafilem1  21449  cusgrafilem2  21450  isuvtx  21458  uvtx01vtx  21462  trls  21497  wlkntrllem2  21521  wlkntrl  21523  constr1trl  21549  2pthon  21563  dfconngra1  21619  eupath  21664  ex-natded9.26  21688  nvss  22033  vsfval  22075  h2hlm  22444  axhcompl-zf  22462  hlim2  22655  hhcmpl  22663  hhcms  22666  shex  22675  isch2  22687  helch  22707  hhsscms  22740  occl  22767  chintcli  22794  dfch2  22870  spanuni  23007  spansni  23020  elnlfn  23392  nmopun  23478  nlelchi  23525  cnlnssadj  23544  adjbd1o  23549  branmfn  23569  pjnmopi  23612  hmopidmchi  23615  abrexss  23954  iuninc  23972  disjabrex  23985  disjabrexf  23986  disjpreima  23987  disjxpin  23989  iundisj2f  23991  suppss2f  24010  fmptdF  24030  fmptcof2  24037  ofpreima  24042  funcnvmptOLD  24043  funcnvmpt  24044  disjdsct  24051  1stpreima  24056  2ndpreima  24057  ctex  24061  iundisj2fi  24114  ishashinf  24120  tosglb  24153  pstmxmet  24253  tpr2rico  24271  esum0  24405  esumc  24407  gsumesum  24412  esumcst  24416  esumfsup  24421  esumpfinvalf  24427  hasheuni  24436  sigaex  24453  sigaval  24454  isrnsigaOLD  24456  pwsiga  24474  sigainb  24480  insiga  24481  dmsigagen  24488  measbase  24512  ismeas  24514  isrnmeas  24515  measiuns  24532  measdivcstOLD  24539  measdivcst  24540  cntmeas  24541  mbfmco2  24576  mbfmcnt  24579  br2base  24580  dya2iocrfn  24590  dya2iocct  24591  dya2iocnrect  24592  dya2iocucvr  24595  sxbrsigalem2  24597  ballotlem2  24707  ballotlemsf1o  24732  ballotlemirc  24750  derangenlem  24818  subfacp1lem1  24826  subfacp1lem3  24829  subfacp1lem4  24830  subfacp1lem5  24831  erdszelem7  24844  erdszelem8  24845  erdsze2lem2  24851  kur14lem9  24861  ptpcon  24881  indispcon  24882  conpcon  24883  cnllyscon  24893  rellyscon  24899  cvmsss2  24922  cvmcov2  24923  cvmliftlem15  24946  cvmlift2lem1  24950  cvmlift2lem12  24962  ghomgrplem  25061  relexpindlem  25100  rtrclreclem.trans  25107  dfrtrcl2  25109  untsucf  25120  dfid4  25144  shftvalg  25169  ntrivcvg  25186  fprodfac  25257  fprod2dlem  25265  fprodcom2  25269  dftr6  25329  coepr  25331  dffr5  25332  dfso2  25333  dfpo2  25334  br8  25335  br6  25336  br4  25337  dfres3  25338  cnvco1  25339  cnvco2  25340  eldm3  25341  fundmpss  25344  fprb  25351  dfdm5  25354  dfrn5  25355  setinds  25356  dfon2lem1  25361  dfon2lem3  25363  dfon2lem6  25366  dfon2lem7  25367  dfon2lem8  25368  dfon2  25370  rdgprc  25373  dfrdg2  25374  predreseq  25401  predpo  25406  predbrg  25408  setlikespec  25409  predep  25414  preddowncl  25418  preduz  25422  predfz  25425  tz6.26  25427  trpredrec  25463  poseq  25475  soseq  25476  wfrlem5  25482  wfrlem10  25487  wfrlem12  25489  wfrlem13  25490  wfrlem14  25491  wfrlem16  25493  tfrALTlem  25498  frrlem5  25507  frrlem11  25515  sltsolem1  25544  nofulllem5  25582  txpss3v  25640  brtxp  25642  brtxp2  25643  pprodss4v  25646  brpprod  25647  brpprod3a  25648  brpprod3b  25649  brsset  25651  idsset  25652  dfon3  25654  brtxpsd  25656  brbigcup  25660  dfbigcup2  25661  fobigcup  25662  elfix  25665  elfix2  25666  dffix2  25667  fixcnv  25670  limitssson  25673  dfom5b  25674  dffun10  25675  elfuns  25676  elfunsg  25677  elsingles  25679  fnsingle  25680  fvsingle  25681  dfiota3  25684  brimage  25687  brimageg  25688  funimage  25689  fnimage  25690  imageval  25691  brcart  25693  brdomaing  25696  brrangeg  25697  brimg  25698  brapply  25699  brcup  25700  brcap  25701  brsuccf  25702  funpartlem  25703  funpartfun  25704  funpartfv  25706  fullfunfv  25708  brrestrict  25710  dfrdg4  25711  tfrqfree  25712  altopelaltxp  25733  altxpsspw  25734  brsegle  25954  fvline  25990  liness  25991  ellines  25998  bpoly2  26015  bpoly3  26016  rankung  26019  ranksng  26020  rankelg  26021  rankpwg  26022  rankeq1o  26024  elhf2g  26029  hfext  26036  onsucconi  26099  supaddc  26145  supadd  26146  mblfinlem2  26152  mblfinlem3  26153  ismblfin  26154  mbfresfi  26160  ftc1cnnc  26186  areacirclem6  26194  trer  26217  finminlem  26219  gtinf  26220  fneer  26266  fnessref  26271  refssfne  26272  islocfin  26274  comppfsc  26285  neibastop1  26286  neibastop2lem  26287  neibastop3  26289  topmeet  26291  topjoin  26292  neifg  26298  tailfb  26304  filnetlem2  26306  filnetlem3  26307  filnetlem4  26308  cover2g  26314  f1opr  26324  inixp  26328  indexdom  26334  frinfm  26335  sdclem2  26344  sdclem1  26345  fdc  26347  isbndx  26389  prdstotbnd  26401  heibor1lem  26416  heiborlem1  26418  heiborlem3  26420  heiborlem4  26421  heiborlem5  26422  heiborlem6  26423  heiborlem8  26425  heiborlem10  26427  ismrer1  26445  riscer  26502  divrngidl  26536  intidl  26537  isfldidl  26576  ispridlc  26578  prtlem10  26612  prtlem13  26615  prtlem16  26616  prtlem19  26625  prter2  26628  prter3  26629  ralxpmap  26640  elrfi  26646  ismrcd1  26650  ismrcd2  26651  istopclsd  26652  ismrc  26653  mrefg2  26659  isnacs3  26662  mzpclall  26682  mzpincl  26689  mzpsubst  26703  mzpcompact2lem  26706  mzpcompact2  26707  eldioph2lem1  26716  eldioph2lem2  26717  eldiophss  26731  diophrex  26732  rexrabdioph  26752  2rexfrabdioph  26754  3rexfrabdioph  26755  4rexfrabdioph  26756  6rexfrabdioph  26757  7rexfrabdioph  26758  rabren3dioph  26774  fphpd  26775  rencldnfilem  26779  pellexlem5  26794  pellex  26796  rmxypairf1o  26872  monotuz  26902  monotoddzzfi  26903  oddcomabszz  26905  2nn0ind  26906  zindbi  26907  mzpcong  26935  rmydioph  26983  rmxdioph  26985  expdiophlem2  26991  setindtr  26993  setindtrs  26994  dford3lem2  26996  ttac  27005  pw2f1ocnv  27006  wepwsolem  27014  inisegn0  27016  dnnumch1  27017  fnwe2val  27022  fnwe2lem2  27024  aomclem1  27027  aomclem2  27028  aomclem6  27032  dfac11  27036  kelac2lem  27038  dfac21  27040  islssfg2  27045  lmhmlnmsplit  27061  pwssplit3  27066  filnm  27068  pwslnmlem1  27070  pwslnm  27072  dsmmval  27076  frlmlbs  27125  unxpwdom3  27132  enfixsn  27133  dfacbasgrp  27149  islindf4  27184  lmisfree  27188  lnr2i  27196  lnrfg  27199  hbtlem6  27209  rngunsnply  27254  pmtrfval  27269  symggen  27287  gsumcom3  27330  acsfn1p  27383  sdrgacs  27385  idomsubgmo  27390  fgraphxp  27406  expgrowth  27428  2sbc6g  27491  iotain  27493  compel  27516  ipo0  27527  ifr0  27528  fnchoice  27575  infrglb  27597  stoweidlem31  27655  stoweidlem57  27681  stirlinglem13  27710  funressnfv  27867  dfdfat2  27870  csbafv12g  27876  tz6.12-afv  27912  rlimdmafv  27916  csbaovg  27919  el2wlkonot  28074  el2spthonot  28075  el2spthonot0  28076  usg2wlkonot  28088  usg2wotspth  28089  2wot2wont  28091  2spontn0vne  28092  2spot2iun2spont  28096  frisusgranb  28109  frgra3vlem1  28112  frgra3vlem2  28113  3vfriswmgralem  28116  2pthfrgra  28123  frgrancvvdeqlem3  28143  frgrancvvdeqlem4  28144  frgrawopreg1  28161  frgrawopreg2  28162  frg2woteq  28171  2spotiundisj  28173  usg2spot2nb  28176  onfrALTlem5  28347  onfrALTlem4  28348  onfrALTlem3  28349  opelopab4  28357  a9e2nd  28364  trsspwALT  28649  trsspwALT2  28650  trsspwALT3  28651  pwtrVD  28655  unipwrVD  28662  unipwr  28663  onfrALTlem5VD  28715  onfrALTlem4VD  28716  onfrALTlem3VD  28717  relopabVD  28731  a9e2ndVD  28738  sspwimp  28748  sspwimpVD  28749  sspwimpcf  28750  sspwimpcfVD  28751  sspwimpALT  28755  sspwimpALT2  28759  a9e2ndALT  28761  bnj23  28801  bnj62  28803  bnj156  28813  bnj219  28818  bnj610  28833  bnj918  28853  bnj927  28857  bnj976  28866  bnj1098  28872  bnj1379  28920  bnj110  28947  bnj98  28956  bnj154  28967  bnj155  28968  bnj535  28979  bnj556  28989  bnj557  28990  bnj581  28997  bnj591  29000  bnj594  29001  bnj580  29002  bnj607  29005  bnj609  29006  bnj600  29008  bnj849  29014  bnj893  29017  bnj908  29020  bnj934  29024  bnj944  29027  bnj964  29032  bnj966  29033  bnj969  29035  bnj970  29036  bnj910  29037  bnj986  29043  bnj999  29046  bnj1018  29051  bnj907  29054  bnj1039  29058  bnj1040  29059  bnj1052  29062  bnj1123  29073  bnj1030  29074  bnj1133  29076  bnj1128  29077  bnj1145  29080  bnj1204  29099  bnj1373  29117  bnj1417  29128  bnj1421  29129  bnj1498  29148  eqlkr2  29595  glbconxN  29872  pmapglbx  30263  pmapglb  30264  pclclN  30385  pclfinN  30394  polval2N  30400  pclfinclN  30444  osumcllem10N  30459  pexmidlem7N  30470  cdleme31sdnN  30881  cdlemefr44  30919  cdleme48fv  30993  cdleme46fvaw  30995  cdleme48bw  30996  cdleme46fsvlpq  30999  cdlemeg46fvcl  31000  cdlemeg49le  31005  cdlemeg46fjgN  31015  cdlemeg46fjv  31017  cdleme48d  31029  cdlemeg49lebilem  31033  cdleme50eq  31035  cdleme50f  31036  cdlemg2jlemOLDN  31087  cdlemg2klem  31089  cdlemk40  31411  cdlemk56  31465  diaglbN  31550  dvhlveclem  31603  dib1dim  31660  dibglbN  31661  diblss  31665  diblsmopel  31666  dicelvalN  31673  diclspsn  31689  cdlemn7  31698  dihordlem7  31709  dihopelvalcpre  31743  xihopellsmN  31749  dihopellsm  31750  dih1  31781  dihmeetlem1N  31785  dihglblem5apreN  31786  dihmeetlem2N  31794  dihglbcpreN  31795  dihmeetlem4preN  31801  dihmeetlem13N  31814  dih1dimatlem  31824  dihatlat  31829  dihjatcclem4  31916  lcdlss  32114

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2393

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-v 2926