Theorem rexbidv 3185

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.)

Hypothesis

Ref	Expression
ralbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexbidv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rexbidv

Step	Hyp	Ref	Expression
1		ralbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	rexbidva 3183	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  2rexbidv  3228  rexralbidv  3229  cbvrex2vw  3248  cbvrex2v  3377  rspc2ev  3648  rspc3ev  3652  ceqsrex2v  3671  reuxfr1d  3772  uniiunlem  4110  n0snor2el  4858  eliun  5019  dfiun2g  5053  dfiin2g  5055  dfiunv2  5058  dmopab2rex  5942  elrnmpt  5981  elrnmptg  5984  elimag  6093  fvelrnb  6982  fvelimab  6994  foelrn  7141  foelrnf  7142  foco2  7143  elabrex  7279  elabrexg  7280  abrexco  7281  f1oiso  7387  f1oiso2  7388  orduninsuc  7880  funcnvuni  7972  fiunlem  7982  fiun  7983  f1iun  7984  abrexex2g  8005  f1oweALT  8013  el2xptp  8076  orderseqlem  8198  poseq  8199  soseq  8200  tfrlem12  8445  seqomlem2  8507  nneob  8712  eldifsucnn  8720  coflton  8727  cofon1  8728  cofon2  8729  naddunif  8749  qseq2  8820  elqsg  8826  elqsecl  8829  elixpsn  8995  ixpsnf1o  8996  isfi  9036  pssnn  9234  enfiALT  9254  frfi  9349  unblem1  9356  unblem2  9357  unbnn2  9361  fofinf1o  9400  finsschain  9429  indexfi  9430  elfi  9482  marypha1lem  9502  supeq3  9518  supmo  9521  suplub  9529  supisolem  9542  eqinf  9553  infval  9555  infglb  9559  infglbb  9560  infmo  9564  oieq1  9581  ordtypelem2  9588  ordtypelem3  9589  ordtypelem9  9595  wemaplem1  9615  brwdom2  9642  brwdom3  9651  unwdomg  9653  oemapval  9752  cantnf  9762  wemapwe  9766  cnfcom3clem  9774  ttrcleq  9778  brttrcl  9782  ttrcltr  9785  tz9.13  9860  tz9.13g  9861  cardf2  10012  isnum2  10014  ennum  10016  cardiun  10051  infxpenc2  10091  aceq1  10186  aceq2  10188  dfac5lem3  10194  dfac5lem4  10195  dfac5lem4OLD  10197  dfac2a  10199  dfac2b  10200  kmlem9  10228  kmlem12  10231  kmlem14  10233  ackbij1  10306  cflm  10319  cfss  10334  cofsmo  10338  cfsmolem  10339  cfcoflem  10341  coftr  10342  isfin7  10370  fin23lem26  10394  isf32lem5  10426  fin1a2lem11  10479  hsmexlem2  10496  axdc3lem3  10521  axdc3  10523  numthcor  10563  zorn2lem7  10571  brdom3  10597  brdom7disj  10600  brdom6disj  10601  iundom2g  10609  fpwwe2  10712  winainflem  10762  winalim2  10765  inar1  10844  tskuni  10852  nqereu  10998  prnmax  11064  genpv  11068  genpnmax  11076  genpass  11078  prlem936  11116  recexsrlem  11172  map2psrpr  11179  supsrlem  11180  axrrecex  11232  axpre-sup  11238  dedekind  11453  cnegex  11471  recex  11922  fimaxre3  12241  infm3  12254  supaddc  12262  supadd  12263  supmul1  12264  supmullem1  12265  supmullem2  12266  supmul  12267  creur  12287  creui  12288  cju  12289  nnunb  12549  arch  12550  xrsupsslem  13369  xrinfmsslem  13370  xrsupss  13371  xrinfmss  13372  xrub  13374  supxrunb1  13381  supxrunb2  13382  infmremnf  13405  infmrp1  13406  modmuladd  13964  fsequb2  14027  hashge2el2difr  14530  tpfo  14549  iswrd  14564  wrdval  14565  csbwrdg  14592  cshword  14839  0csh0  14841  2cshwcshw  14874  scshwfzeqfzo  14875  cshimadifsn  14878  shftfval  15119  abs1m  15384  rexfiuz  15396  reusq0  15511  limsupbnd2  15529  clim  15540  rlim  15541  rlim2  15542  rlim0  15554  rlim0lt  15555  ello1mpt2  15568  o1lo1  15583  o1compt  15633  rlimdiv  15694  climsup  15718  sumeq1  15737  sumeq2w  15740  sumeq2sdv  15751  summo  15765  fsum  15768  fsumcvg3  15777  infcvgaux2i  15906  mertenslem1  15932  mertenslem2  15933  mertens  15934  prodeq1f  15954  prodeq1  15955  prodeq2w  15958  prodeq2sdv  15971  prodmo  15984  fprod  15989  divides  16304  odd2np1lem  16388  opeo  16413  omeo  16414  divalglem4  16444  divalglem10  16450  divalg  16451  gcdcllem3  16547  zeqzmulgcd  16556  bezoutlem1  16586  exprmfct  16751  nnnn0modprm0  16853  pythagtriplem2  16864  pythagtrip  16881  pceu  16893  pcprmpw2  16929  unbenlem  16955  4sqlem12  17003  vdwapval  17020  vdwapun  17021  vdwmc2  17026  vdwpc  17027  vdwlem2  17029  vdwlem10  17037  vdwlem13  17040  vdwnnlem1  17042  rami  17062  cshwsiun  17147  cshwrepswhash1  17150  brssc  17875  cat1  18164  isdrs  18371  drsdir  18372  drsdirfi  18375  isdrs2  18376  ipodrsima  18611  grpinvalem  18711  gsumvalx  18714  gsumpropd  18716  gsumress  18720  isnsgrp  18761  smndex2dnrinv  18950  sgrp2nmndlem5  18964  grpinvex  18983  dfgrp2  19002  grpidinv2  19037  grpidinv  19038  dfgrp3lem  19078  grp1  19087  imasgrp2  19095  cyccom  19243  conjnmzb  19293  gaorb  19347  orbsta  19353  symgfix2  19458  symgextfo  19464  pmtrprfvalrn  19530  psgnunilem3  19538  psgneu  19548  psgnval  19549  psgnvali  19550  psgnvalii  19551  ispgp  19634  subgpgp  19639  sylow1  19645  pgpfi  19647  sylow2blem3  19664  fislw  19667  sylow3lem2  19670  lsmelvalm  19693  lsmass  19711  pj1fval  19736  pj1val  19737  pj1eu  19738  pj1id  19741  efgrelexlema  19791  efgrelexlemb  19792  efgredeu  19794  cyggeninv  19925  pgpfac1lem2  20119  pgpfac1lem3  20121  pgpfac1lem4  20122  pgpfac1  20124  pgpfaclem2  20126  pgpfac  20128  dvdsrval  20387  dvdsr  20388  subrgdvds  20614  lss1d  20984  lspsn  21023  ellspsn  21024  lspsolvlem  21167  rspsn  21366  pzriprnglem10  21524  znf1o  21593  cygznlem3  21611  psgndiflemA  21642  ellspd  21845  opsrval  22087  mat1dimelbas  22498  mat1dimbas  22499  scmatval  22531  scmatel  22532  scmateALT  22539  mat0scmat  22565  decpmataa0  22795  decpmatmulsumfsupp  22800  pmatcollpw2lem  22804  pm2mpmhmlem1  22845  chpscmat  22869  basis2  22979  eltg2  22986  tg2  22993  isclo  23116  neival  23131  isnei  23132  isneip  23134  restbas  23187  neitr  23209  cnpval  23265  iscnp  23266  cnpimaex  23285  lmbr  23287  lmbr2  23288  cnprest2  23319  lmff  23330  regsep  23363  pnrmopn  23372  nrmsep3  23384  isnrm2  23387  iscmp  23417  cmpsublem  23428  cmpsub  23429  tgcmp  23430  sscmp  23434  hauscmplem  23435  1stcclb  23473  1stcfb  23474  is2ndc  23475  2ndc1stc  23480  1stcrest  23482  2ndcctbss  23484  1stcelcls  23490  llyeq  23499  nllyeq  23500  hausllycmp  23523  lly1stc  23525  refssex  23540  refun0  23544  islocfin  23546  locfinnei  23552  comppfsc  23561  txbas  23596  ptval  23599  ptpjopn  23641  ptclsg  23644  txcnp  23649  ptcnp  23651  txrest  23660  ptrescn  23668  txcmp  23672  tx1stc  23679  xkococn  23689  kqreglem1  23770  fbasssin  23865  fbssfi  23866  fbssint  23867  fbun  23869  fgss2  23903  fgcl  23907  ufli  23943  fmfnfmlem3  23985  fbflim2  24006  hauspwpwf1  24016  flfneii  24021  flftg  24025  txflf  24035  fclscf  24054  alexsubb  24075  alexsubALT  24080  tsmssubm  24172  ustincl  24237  ustdiag  24238  ustinvel  24239  ustexhalf  24240  ust0  24249  trust  24259  elutop  24263  ucnval  24307  ucncn  24315  cfiluexsm  24320  cfiluweak  24325  blssps  24455  blss  24456  imasf1oxms  24523  mopni  24526  metss  24542  metrest  24558  metcnp3  24574  cfilucfil  24593  metuel2  24599  nlmvscn  24729  nrginvrcn  24734  icccmplem1  24863  icccmplem2  24864  icccmp  24866  divcnOLD  24909  divcn  24911  cncfval  24933  elcncf2  24935  cncfmet  24954  cnheibor  25006  evth  25010  lebnumlem3  25014  lebnum  25015  xlebnum  25016  lebnumii  25017  ipcn  25299  lmmbr  25311  lmmbr2  25312  cfilfval  25317  cfili  25321  iscfil3  25326  caufval  25328  iscau  25329  iscau2  25330  equivcfil  25352  equivcau  25353  lmcau  25366  ovolval  25527  elovolm  25529  ovolgelb  25534  ovoliunlem1  25556  ovoliun2  25560  ovolshftlem1  25563  ovolscalem1  25567  ovolicc  25577  ioombl1lem4  25615  uniioombllem2  25637  mbfaddlem  25714  mbfsup  25718  mbfinf  25719  mbflimsup  25720  i1fmulc  25758  itg1climres  25769  itg2val  25783  itg2l  25784  itg2leub  25789  itg2seq  25797  itg2monolem1  25805  itg2mono  25808  itg2i1fseq2  25811  cniccibl  25896  cnicciblnc  25898  ellimc3  25934  limciun  25949  dvferm1  26043  dvferm2  26045  lhop1lem  26072  ply1divex  26196  ig1peu  26234  plyval  26252  elply2  26255  coeval  26282  coeeu  26284  coelem  26285  coeeq  26286  plydivlem4  26356  plydivex  26357  aannenlem2  26389  aalioulem2  26393  aaliou2  26400  ulmval  26441  ulm2  26446  ulmcau  26456  ulmdvlem3  26463  abelthlem9  26502  abelth  26503  efif1olem4  26605  eflogeq  26662  efopn  26718  cxpcn3  26809  cxpeq  26818  rlimcnp  27026  lgamgulmlem6  27095  muval  27193  dchrptlem1  27326  dchrptlem2  27327  lgsdchrval  27416  2lgslem1b  27454  addsq2nreurex  27506  pntpbnd  27650  pntibndlem3  27654  pntibnd  27655  pntlemi  27666  pntleme  27670  pntlemp  27672  pnt3  27674  elno  27708  elnoOLD  27709  sltval  27710  nosupprefixmo  27763  noinfprefixmo  27764  nosupcbv  27765  nosupno  27766  nosupdm  27767  nosupfv  27769  nosupres  27770  nosupbnd1lem1  27771  nosupbnd1lem3  27773  nosupbnd1lem4  27774  nosupbnd1lem5  27775  noinfcbv  27780  noinfno  27781  noinfdm  27782  noinffv  27784  noinfres  27785  noinfbnd1lem3  27788  noinfbnd1lem4  27789  noinfbnd1lem5  27790  madef  27913  cofsslt  27970  coinitsslt  27971  cofss  27982  coiniss  27983  addsval  28013  addsval2  28014  addsproplem2  28021  addsproplem4  28023  addsproplem5  28024  addsproplem6  28025  addscut  28029  sleadd1  28040  addsuniflem  28052  addsunif  28053  addsasslem1  28054  addsasslem2  28055  addsbdaylem  28067  negsid  28091  negsunif  28105  mulsval  28153  mulsuniflem  28193  addsdilem1  28195  mulsasslem1  28207  precsexlemcbv  28248  precsexlem3  28251  precsexlem8  28256  precsexlem9  28257  precsexlem11  28259  precsex  28260  n0s0suc  28363  dfnns2  28380  zscut  28411  n0seo  28423  zseo  28424  elreno  28445  recut  28446  0reno  28447  renegscl  28448  readdscl  28449  remulscllem1  28450  remulscl  28452  istrkgld  28485  istrkg3ld  28487  axtgsegcon  28490  axtgpasch  28493  axtgcont1  28494  axtgupdim2  28497  legov  28611  islnopp  28765  ishpg  28785  hpgbr  28786  hpgcom  28793  iscgra1  28836  isinag  28864  isleag  28873  ttgval  28901  ttgvalOLD  28902  ttgitvval  28914  ttgelitv  28915  brbtwn  28932  brcgr  28933  axpasch  28974  axlowdim2  28993  axlowdim  28994  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  axcontlem8  29004  upgredg2vtx  29176  edglnl  29178  usgredg4  29252  ushgredgedg  29264  ushgredgedgloop  29266  dfnbgr2  29372  nbgrel  29375  nbumgrvtx  29381  nbgrnself  29394  uvtxel1  29431  cusgrfilem2  29492  cusgrfi  29494  vtxd0nedgb  29524  fusgrn0degnn0  29535  wlkonl1iedg  29701  wspniunwspnon  29956  elwwlks2on  29992  clwwlknscsh  30094  erclwwlkneq  30099  eleclclwwlkn  30108  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  3cyclfrgrrn1  30317  friendshipgt3  30430  isgrpo  30529  isgrpoi  30530  grpoidinvlem3  30538  grpoideu  30541  grpoidinv2  30547  nmoofval  30794  nmooval  30795  nmosetn0  30797  nmoolb  30803  nmoubi  30804  nmlno0lem  30825  chcompl  31274  pjhthmo  31334  pjhval  31429  pjpreeq  31430  h1de2ci  31588  elspansn  31598  nmopval  31888  nmopsetn0  31897  nmfnval  31908  nmfnsetn0  31910  eigvecval  31928  hhcno  31936  hhcnf  31937  nmoplb  31939  nmopub  31940  nmfnlb  31956  nmfnleub  31957  eleigvec  31989  nmlnop0iALT  32027  nmopun  32046  nmcexi  32058  branmfn  32137  pjnmopi  32180  cvbr  32314  hatomic  32392  chrelat2  32402  cdjreui  32464  cdj3lem2  32467  elabreximd  32538  br8d  32632  unipreima  32662  abfmpunirn  32670  curry2ima  32720  toslublem  32945  tosglblem  32947  cyc3genpm  33145  archirng  33168  archiexdiv  33170  archiabllem2a  33174  archiabl  33178  erlcl1  33232  erlcl2  33233  erldi  33234  erlbrd  33235  erler  33237  fracerl  33273  isarchiofld  33312  elgrplsmsn  33383  lsmssass  33395  grplsm0l  33396  grplsmid  33397  mxidlprm  33463  1arithidomlem1  33528  1arithidom  33530  1arithufdlem1  33537  1arithufdlem2  33538  1arithufdlem3  33539  1arithufdlem4  33540  1arithufd  33541  dfufd2  33543  fedgmul  33644  ccfldextdgrr  33682  fldext2chn  33719  constrsslem  33731  constrconj  33735  crefi  33793  pcmplfin  33806  rspectopn  33813  pstmfval  33842  tpr2rico  33858  rge0scvg  33895  ismntop  33972  esumc  34015  esumpcvgval  34042  esum2dlem  34056  inelsros  34142  diffiunisros  34143  dya2icoseg2  34243  dya2iocuni  34248  eulerpartlemgvv  34341  eulerpartlemgh  34343  hgt749d  34626  tgoldbachgt  34640  bnj66  34836  bnj873  34900  bnj18eq1  34903  bnj1234  34989  bnj1318  35001  cplgredgex  35088  subfacp1lem3  35150  pconncn  35192  cnpconn  35198  txpconn  35200  connpconn  35203  iscvm  35227  cvmcov  35231  cvmopnlem  35246  cvmliftlem15  35266  cvmlift3lem2  35288  cvmlift3lem4  35290  cvmlift3  35296  satf  35321  satfv1  35331  satfvsucsuc  35333  satfbrsuc  35334  satfrnmapom  35338  satf0op  35345  sat1el2xp  35347  fmlafvel  35353  fmlasuc  35354  fmla1  35355  isfmlasuc  35356  fmlaomn0  35358  fmlasucdisj  35367  satffunlem1lem1  35370  satffunlem1lem2  35371  satffunlem2lem1  35372  dmopab3rexdif  35373  satffunlem2lem2  35374  sategoelfvb  35387  satfv1fvfmla1  35391  2goelgoanfmla1  35392  rexxfr3dALT  35607  r1peuqusdeg1  35611  br8  35718  br6  35719  br4  35720  dfrdg2  35759  dfrdg3  35760  altxpeq2  35938  funtransport  35995  fvtransport  35996  brcolinear2  36022  colineardim1  36025  segcon2  36069  brsegle  36072  funray  36104  fvray  36105  funline  36106  linedegen  36107  fvline  36108  ellines  36116  prodeq12sdv  36184  cbvsumdavw  36245  cbvproddavw  36246  cbvsumdavw2  36261  cbvproddavw2  36262  nn0prpwlem  36288  fnessref  36323  neibastop2lem  36326  neibastop2  36327  tailfb  36343  unblimceq0lem  36472  unblimceq0  36473  unbdqndv2  36477  bj-finsumval0  37251  relowlssretop  37329  nlpineqsn  37374  pibp19  37380  phpreu  37564  matunitlindflem2  37577  ptrest  37579  poimirlem4  37584  poimirlem17  37597  poimirlem20  37600  poimirlem24  37604  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  poimirlem31  37611  poimirlem32  37612  poimir  37613  heicant  37615  mblfinlem1  37617  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  itg2gt0cn  37635  ftc1anclem6  37658  unirep  37674  indexa  37693  sdclem2  37702  sdclem1  37703  sdc  37704  fdc  37705  fdc1  37706  incsequz  37708  istotbnd  37729  sstotbnd2  37734  equivtotbnd  37738  isbnd  37740  bndss  37746  ssbnd  37748  totbndbnd  37749  ismtybndlem  37766  heibor1lem  37769  heiborlem1  37771  heiborlem6  37776  heiborlem8  37778  heiborlem10  37780  heibor  37781  rngoid  37862  isgrpda  37915  isdrngo2  37918  divrngidl  37988  prnc  38027  isfldidl  38028  exanres3  38252  brcoels  38391  br1cossxrnres  38404  eldm1cossres2  38417  prtlem5  38816  prtlem13  38824  prtlem16  38825  islshp  38935  lsmsat  38964  lcvbr  38977  lsatcv0  38987  lshpsmreu  39065  lshpkrlem1  39066  lshpkrlem2  39067  lshpkrlem3  39068  lshpkrcl  39072  lshpset2N  39075  islshpkrN  39076  cvrval  39225  atlex  39272  glbconxN  39335  hlsuprexch  39338  islln  39463  islpln  39487  islpln5  39492  lvolex3N  39495  islvol  39530  islvol5  39536  ispointN  39699  pmapglbx  39726  paddval  39755  elpaddn0  39757  elpaddat  39761  elpadd0  39766  4atex  40033  4atex2  40034  cdlemefrs29bpre1  40354  cdlemefrs32fva  40357  cdlemg33b  40664  dvhb1dimN  40943  dvhopellsm  41074  dib1dim  41122  diclspsn  41151  dihglblem2aN  41250  dihglblem2N  41251  dih1dimatlem  41286  dvh3dimatN  41396  dvh2dim  41402  dvh3dim  41403  dvh4dimN  41404  dvh3dim3N  41406  dochfl1  41433  lcfl7N  41458  lcf1o  41508  lcfrlem39  41538  mapdpglem3  41632  hvmapvalvalN  41718  hdmap14lem2a  41824  hdmapglem7a  41884  3factsumint1  41978  primrootsunit1  42054  primrootscoprmpow  42056  primrootscoprbij  42059  remexz  42061  aks6d1c2p2  42076  aks6d1c6lem5  42134  aks5lem8  42158  exfinfldd  42160  3rspcedvd  42208  nnn1suc  42255  sn-negex12  42392  fimgmcyclem  42488  prjspeclsp  42567  elrfi  42650  isnacs  42660  nacsfg  42661  nacsfix  42668  mzpcompact2lem  42707  eldiophb  42713  eldioph  42714  eldioph2  42718  eldioph2b  42719  eldioph3  42722  eldiophss  42730  diophrex  42731  sbcrexgOLD  42741  sbc2rexgOLD  42744  rexrabdioph  42750  rexfrabdioph  42751  elnn0rabdioph  42759  dvdsrabdioph  42766  eldioph4b  42767  eldioph4i  42768  diophren  42769  rencldnfilem  42776  pell1234qrdich  42817  jm2.27  42965  expdiophlem1  42978  wepwsolem  42999  aomclem8  43018  islnr3  43072  lnr2i  43073  lpirlnr  43074  hbtlem1  43080  hbtlem2  43081  hbtlem7  43082  hbtlem4  43083  hbtlem5  43085  hbtlem6  43086  dgraaval  43101  dgraalem  43102  dgraaub  43105  rngunsnply  43130  onsupmaxb  43200  onexoegt  43205  onsucelab  43225  limnsuc  43227  oaordnr  43258  omnord1  43267  oenord1  43278  oaomoencom  43279  oenass  43281  cantnfresb  43286  tfsconcatfv2  43302  tfsconcatb0  43306  tfsconcat0i  43307  ofoafo  43318  naddcnffo  43326  oaun3lem1  43336  oadif1lem  43341  oadif1  43342  minregex2  43497  brtrclfv2  43689  clsk1indlem1  44007  extoimad  44126  mnuop123d  44231  mnuop23d  44235  mnuprdlem1  44241  mnuprdlem2  44242  ismnushort  44270  disjrnmpt2  45095  upbdrech  45220  ssfiunibd  45224  supxrgere  45248  supxrgelem  45252  supxrge  45253  suplesup  45254  infxr  45282  infleinf  45287  supxrunb3  45314  unb2ltle  45330  uzub  45346  supminfxr  45379  iccshift  45436  iooshift  45440  climinf  45527  climinff  45532  ellimcabssub0  45538  climf  45543  limcperiod  45549  limclner  45572  climf2  45587  clim2d  45594  limsuppnfd  45623  limsuppnf  45632  climinfmpt  45636  limsupubuzmpt  45640  limsupmnf  45642  limsupre2lem  45645  limsupre2  45646  limsupmnfuz  45648  limsupre2mpt  45651  limsupre3lem  45653  limsupre3  45654  limsupre3mpt  45655  limsupre3uzlem  45656  limsupre3uz  45657  limsupreuz  45658  limsupreuzmpt  45660  climuz  45665  liminfreuzlem  45723  liminfreuz  45724  xlimmnfvlem1  45753  xlimmnfv  45755  xlimpnfvlem1  45757  xlimpnfv  45759  cncfshiftioo  45813  fperdvper  45840  itgiccshift  45901  itgperiod  45902  stoweidlem27  45948  stoweidlem31  45952  stoweidlem43  45964  stoweidlem46  45967  stoweidlem52  45973  stoweidlem60  45981  fourierdlem42  46070  fourierdlem48  46075  fourierdlem51  46078  fourierdlem54  46081  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem68  46095  fourierdlem70  46097  fourierdlem71  46098  fourierdlem73  46100  fourierdlem80  46107  fourierdlem81  46108  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem92  46119  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem100  46127  fourierdlem103  46130  fourierdlem104  46131  fourierdlem105  46132  fourierdlem108  46135  fourierdlem109  46136  fourierdlem110  46137  fourierdlem112  46139  fourierdlem113  46140  sge0pnffigt  46317  sge0resplit  46327  ovnval2  46466  ovnval2b  46473  ovnlecvr  46479  ovnpnfelsup  46480  ovn0lem  46486  ovnsubaddlem1  46491  hoidmvlelem1  46516  ovnhoilem1  46522  ovnhoi  46524  ovnlecvr2  46531  hoiqssbl  46546  ovolval5lem2  46574  ovolval5lem3  46575  ovolval5  46576  ovnovol  46580  smfsuplem2  46733  smfsup  46735  smfinflem  46738  smfinf  46739  fsetsnf  46966  fsetsnfo  46968  cfsetsnfsetf  46973  cfsetsnfsetfo  46975  cbvrex2  47019  2reu8i  47028  2reuimp0  47029  afvelrnb  47078  afvelrnb0  47079  elsetpreimafvb  47258  imasetpreimafvbijlemfo  47279  iccelpart  47307  iccpartiun  47308  icceuelpart  47310  sprsymrelf1lem  47365  sprsymrelf  47369  fmtnofac2lem  47442  fmtnofac2  47443  fmtnofac1  47444  m1expevenALTV  47521  odd2np1ALTV  47548  opoeALTV  47557  opeoALTV  47558  mogoldbblem  47594  nfermltlrev  47618  isgbow  47626  isgbo  47627  7gbow  47646  9gbo  47648  11gbo  47649  sbgoldbwt  47651  mogoldbb  47659  sbgoldbo  47661  nnsum3primesgbe  47666  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  bgoldbtbnd  47683  dfclnbgr2  47697  clnbgrel  47701  dfsclnbgr2  47718  sclnbgrel  47719  sclnbgrelself  47720  vopnbgrel  47726  vopnbgrelself  47727  dfclnbgr6  47728  dfnbgr6  47729  dfsclnbgr6  47730  clnbgrgrim  47786  grlimgrtri  47820  uspgrsprf1  47870  uspgrsprfo  47871  0nodd  47893  1odd  47894  2nodd  47895  0even  47960  1neven  47961  2even  47962  2zlidl  47963  2zrngamgm  47968  2zrngagrp  47972  2zrngmmgm  47975  2zrngnmrid  47979  lcoval  48141  el0ldep  48195  ldepspr  48202  zlmodzxzldep  48233  line  48466  rrxline  48468  sepnsepo  48603