Theorem rexbidv 3158

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 3156	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2113  ∃wrex 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3059

This theorem is referenced by:  2rexbidv  3199  rexralbidv  3200  cbvrex2vw  3217  cbvrex2v  3337  rspc2ev  3587  rspc3ev  3591  ceqsrex2v  3610  reuxfr1d  3706  uniiunlem  4037  n0snor2el  4787  eliun  4948  dfiun2g  4983  dfiin2g  4984  dfiunv2  4987  dmopab2rex  5864  elrnmpt  5905  elrnmptg  5908  elimag  6021  fvelrnb  6892  fvelimab  6904  foelrn  7050  foelrnf  7051  foco2  7052  elabrex  7186  elabrexg  7187  abrexco  7188  f1oiso  7295  f1oiso2  7296  orduninsuc  7783  funcnvuni  7872  fiunlem  7884  fiun  7885  f1iun  7886  abrexex2g  7906  f1oweALT  7914  el2xptp  7977  orderseqlem  8097  poseq  8098  soseq  8099  tfrlem12  8318  seqomlem2  8380  nneob  8582  eldifsucnn  8590  coflton  8597  cofon1  8598  cofon2  8599  naddunif  8619  qseq2  8693  elqsg  8699  elqsecl  8702  elixpsn  8873  ixpsnf1o  8874  isfi  8910  pssnn  9091  enfiALT  9110  frfi  9183  unblem1  9190  unblem2  9191  unbnn2  9195  fofinf1o  9230  finsschain  9257  indexfi  9258  elfi  9314  marypha1lem  9334  supeq3  9350  supmo  9353  suplub  9361  supisolem  9375  eqinf  9386  infval  9388  infglb  9392  infglbb  9393  infmo  9398  oieq1  9415  ordtypelem2  9422  ordtypelem3  9423  ordtypelem9  9429  wemaplem1  9449  brwdom2  9476  brwdom3  9485  unwdomg  9487  oemapval  9590  cantnf  9600  wemapwe  9604  cnfcom3clem  9612  ttrcleq  9616  brttrcl  9620  ttrcltr  9623  tz9.13  9701  tz9.13g  9702  cardf2  9853  isnum2  9855  ennum  9857  cardiun  9892  infxpenc2  9930  aceq1  10025  aceq2  10027  dfac5lem3  10033  dfac5lem4  10034  dfac5lem4OLD  10036  dfac2a  10038  dfac2b  10039  kmlem9  10067  kmlem12  10070  kmlem14  10072  ackbij1  10145  cflm  10158  cfss  10173  cofsmo  10177  cfsmolem  10178  cfcoflem  10180  coftr  10181  isfin7  10209  fin23lem26  10233  isf32lem5  10265  fin1a2lem11  10318  hsmexlem2  10335  axdc3lem3  10360  axdc3  10362  numthcor  10402  zorn2lem7  10410  brdom3  10436  brdom7disj  10439  brdom6disj  10440  iundom2g  10448  fpwwe2  10552  winainflem  10602  winalim2  10605  inar1  10684  tskuni  10692  nqereu  10838  prnmax  10904  genpv  10908  genpnmax  10916  genpass  10918  prlem936  10956  recexsrlem  11012  map2psrpr  11019  supsrlem  11020  axrrecex  11072  axpre-sup  11078  dedekind  11294  cnegex  11312  recex  11767  fimaxre3  12086  infm3  12099  supaddc  12107  supadd  12108  supmul1  12109  supmullem1  12110  supmullem2  12111  supmul  12112  creur  12137  creui  12138  cju  12139  nnunb  12395  arch  12396  xrsupsslem  13220  xrinfmsslem  13221  xrsupss  13222  xrinfmss  13223  xrub  13225  supxrunb1  13232  supxrunb2  13233  infmremnf  13257  infmrp1  13258  modmuladd  13834  fsequb2  13897  hashge2el2difr  14402  tpfo  14421  iswrd  14436  wrdval  14437  csbwrdg  14465  cshword  14712  0csh0  14714  2cshwcshw  14746  scshwfzeqfzo  14747  cshimadifsn  14750  shftfval  14991  abs1m  15257  rexfiuz  15269  reusq0  15386  limsupbnd2  15404  clim  15415  rlim  15416  rlim2  15417  rlim0  15429  rlim0lt  15430  ello1mpt2  15443  o1lo1  15458  o1compt  15508  rlimdiv  15567  climsup  15591  sumeq1  15610  sumeq2w  15613  sumeq2sdv  15624  summo  15638  fsum  15641  fsumcvg3  15650  infcvgaux2i  15779  mertenslem1  15805  mertenslem2  15806  mertens  15807  prodeq1f  15827  prodeq1  15828  prodeq2w  15831  prodeq2sdv  15844  prodmo  15857  fprod  15862  divides  16179  odd2np1lem  16265  opeo  16290  omeo  16291  divalglem4  16321  divalglem10  16327  divalg  16328  gcdcllem3  16426  zeqzmulgcd  16435  bezoutlem1  16464  exprmfct  16629  nnnn0modprm0  16732  pythagtriplem2  16743  pythagtrip  16760  pceu  16772  pcprmpw2  16808  unbenlem  16834  4sqlem12  16882  vdwapval  16899  vdwapun  16900  vdwmc2  16905  vdwpc  16906  vdwlem2  16908  vdwlem10  16916  vdwlem13  16919  vdwnnlem1  16921  rami  16941  cshwsiun  17025  cshwrepswhash1  17028  brssc  17736  cat1  18019  isdrs  18222  drsdir  18223  drsdirfi  18226  isdrs2  18227  ipodrsima  18462  grpinvalem  18596  gsumvalx  18599  gsumpropd  18601  gsumress  18605  isnsgrp  18646  smndex2dnrinv  18838  sgrp2nmndlem5  18852  grpinvex  18871  dfgrp2  18890  grpidinv2  18925  grpidinv  18926  dfgrp3lem  18966  grp1  18975  imasgrp2  18983  cyccom  19130  conjnmzb  19180  gaorb  19234  orbsta  19240  symgfix2  19343  symgextfo  19349  pmtrprfvalrn  19415  psgnunilem3  19423  psgneu  19433  psgnval  19434  psgnvali  19435  psgnvalii  19436  ispgp  19519  subgpgp  19524  sylow1  19530  pgpfi  19532  sylow2blem3  19549  fislw  19552  sylow3lem2  19555  lsmelvalm  19578  lsmass  19596  pj1fval  19621  pj1val  19622  pj1eu  19623  pj1id  19626  efgrelexlema  19676  efgrelexlemb  19677  efgredeu  19679  cyggeninv  19810  pgpfac1lem2  20004  pgpfac1lem3  20006  pgpfac1lem4  20007  pgpfac1  20009  pgpfaclem2  20011  pgpfac  20013  dvdsrval  20295  dvdsr  20296  subrgdvds  20517  lss1d  20912  lspsn  20951  ellspsn  20952  lspsolvlem  21095  rspsn  21286  pzriprnglem10  21443  znf1o  21504  cygznlem3  21522  psgndiflemA  21554  ellspd  21755  opsrval  21999  mat1dimelbas  22413  mat1dimbas  22414  scmatval  22446  scmatel  22447  scmateALT  22454  mat0scmat  22480  decpmataa0  22710  decpmatmulsumfsupp  22715  pmatcollpw2lem  22719  pm2mpmhmlem1  22760  chpscmat  22784  basis2  22893  eltg2  22900  tg2  22907  isclo  23029  neival  23044  isnei  23045  isneip  23047  restbas  23100  neitr  23122  cnpval  23178  iscnp  23179  cnpimaex  23198  lmbr  23200  lmbr2  23201  cnprest2  23232  lmff  23243  regsep  23276  pnrmopn  23285  nrmsep3  23297  isnrm2  23300  iscmp  23330  cmpsublem  23341  cmpsub  23342  tgcmp  23343  sscmp  23347  hauscmplem  23348  1stcclb  23386  1stcfb  23387  is2ndc  23388  2ndc1stc  23393  1stcrest  23395  2ndcctbss  23397  1stcelcls  23403  llyeq  23412  nllyeq  23413  hausllycmp  23436  lly1stc  23438  refssex  23453  refun0  23457  islocfin  23459  locfinnei  23465  comppfsc  23474  txbas  23509  ptval  23512  ptpjopn  23554  ptclsg  23557  txcnp  23562  ptcnp  23564  txrest  23573  ptrescn  23581  txcmp  23585  tx1stc  23592  xkococn  23602  kqreglem1  23683  fbasssin  23778  fbssfi  23779  fbssint  23780  fbun  23782  fgss2  23816  fgcl  23820  ufli  23856  fmfnfmlem3  23898  fbflim2  23919  hauspwpwf1  23929  flfneii  23934  flftg  23938  txflf  23948  fclscf  23967  alexsubb  23988  alexsubALT  23993  tsmssubm  24085  ustincl  24150  ustdiag  24151  ustinvel  24152  ustexhalf  24153  ust0  24162  trust  24171  elutop  24175  ucnval  24218  ucncn  24226  cfiluexsm  24231  cfiluweak  24236  blssps  24366  blss  24367  imasf1oxms  24431  mopni  24434  metss  24450  metrest  24466  metcnp3  24482  cfilucfil  24501  metuel2  24507  nlmvscn  24629  nrginvrcn  24634  icccmplem1  24765  icccmplem2  24766  icccmp  24768  divcnOLD  24811  divcn  24813  cncfval  24835  elcncf2  24837  cncfmet  24856  cnheibor  24908  evth  24912  lebnumlem3  24916  lebnum  24917  xlebnum  24918  lebnumii  24919  ipcn  25200  lmmbr  25212  lmmbr2  25213  cfilfval  25218  cfili  25222  iscfil3  25227  caufval  25229  iscau  25230  iscau2  25231  equivcfil  25253  equivcau  25254  lmcau  25267  ovolval  25428  elovolm  25430  ovolgelb  25435  ovoliunlem1  25457  ovoliun2  25461  ovolshftlem1  25464  ovolscalem1  25468  ovolicc  25478  ioombl1lem4  25516  uniioombllem2  25538  mbfaddlem  25615  mbfsup  25619  mbfinf  25620  mbflimsup  25621  i1fmulc  25658  itg1climres  25669  itg2val  25683  itg2l  25684  itg2leub  25689  itg2seq  25697  itg2monolem1  25705  itg2mono  25708  itg2i1fseq2  25711  cniccibl  25796  cnicciblnc  25798  ellimc3  25834  limciun  25849  dvferm1  25943  dvferm2  25945  lhop1lem  25972  ply1divex  26096  ig1peu  26134  plyval  26152  elply2  26155  coeval  26182  coeeu  26184  coelem  26185  coeeq  26186  plydivlem4  26258  plydivex  26259  aannenlem2  26291  aalioulem2  26295  aaliou2  26302  ulmval  26343  ulm2  26348  ulmcau  26358  ulmdvlem3  26365  abelthlem9  26404  abelth  26405  efif1olem4  26508  eflogeq  26565  efopn  26621  cxpcn3  26712  cxpeq  26721  rlimcnp  26929  lgamgulmlem6  26998  muval  27096  dchrptlem1  27229  dchrptlem2  27230  lgsdchrval  27319  2lgslem1b  27357  addsq2nreurex  27409  pntpbnd  27553  pntibndlem3  27557  pntibnd  27558  pntlemi  27569  pntleme  27573  pntlemp  27575  pnt3  27577  elno  27611  elnoOLD  27612  sltval  27613  nosupprefixmo  27666  noinfprefixmo  27667  nosupcbv  27668  nosupno  27669  nosupdm  27670  nosupfv  27672  nosupres  27673  nosupbnd1lem1  27674  nosupbnd1lem3  27676  nosupbnd1lem4  27677  nosupbnd1lem5  27678  noinfcbv  27683  noinfno  27684  noinfdm  27685  noinffv  27687  noinfres  27688  noinfbnd1lem3  27691  noinfbnd1lem4  27692  noinfbnd1lem5  27693  madef  27824  cofsslt  27889  coinitsslt  27890  cofss  27901  coiniss  27902  addsval  27932  addsval2  27933  addsproplem2  27940  addsproplem4  27942  addsproplem5  27943  addsproplem6  27944  addscut  27948  sleadd1  27959  addsuniflem  27971  addsunif  27972  addsasslem1  27973  addsasslem2  27974  addsbdaylem  27986  negsid  28010  negsunif  28024  mulsval  28078  mulsuniflem  28118  addsdilem1  28120  mulsasslem1  28132  precsexlemcbv  28174  precsexlem3  28177  precsexlem8  28182  precsexlem9  28183  precsexlem11  28185  precsex  28186  n0s0suc  28302  n0sfincut  28315  bdayn0sf1o  28328  dfnns2  28330  zscut  28365  n0seo  28379  zseo  28380  pw2recs  28396  halfcut  28415  zs12negscl  28427  zs12ge0  28432  elreno  28436  recut  28439  elreno2  28440  1reno  28442  renegscl  28443  readdscl  28444  remulscllem1  28445  remulscl  28447  istrkgld  28480  istrkg3ld  28482  axtgsegcon  28485  axtgpasch  28488  axtgcont1  28489  axtgupdim2  28492  legov  28606  islnopp  28760  ishpg  28780  hpgbr  28781  hpgcom  28788  iscgra1  28831  isinag  28859  isleag  28868  ttgval  28896  ttgitvval  28903  ttgelitv  28904  brbtwn  28921  brcgr  28922  axpasch  28963  axlowdim2  28982  axlowdim  28983  axcontlem2  28987  axcontlem4  28989  axcontlem7  28992  axcontlem8  28993  upgredg2vtx  29163  edglnl  29165  usgredg4  29239  ushgredgedg  29251  ushgredgedgloop  29253  dfnbgr2  29359  nbgrel  29362  nbumgrvtx  29368  nbgrnself  29381  uvtxel1  29418  cusgrfilem2  29479  cusgrfi  29481  vtxd0nedgb  29511  fusgrn0degnn0  29522  wlkonl1iedg  29686  wspniunwspnon  29945  elwwlks2on  29983  clwwlknscsh  30086  erclwwlkneq  30091  eleclclwwlkn  30100  hashecclwwlkn1  30101  umgrhashecclwwlk  30102  3cyclfrgrrn1  30309  friendshipgt3  30422  isgrpo  30521  isgrpoi  30522  grpoidinvlem3  30530  grpoideu  30533  grpoidinv2  30539  nmoofval  30786  nmooval  30787  nmosetn0  30789  nmoolb  30795  nmoubi  30796  nmlno0lem  30817  chcompl  31266  pjhthmo  31326  pjhval  31421  pjpreeq  31422  h1de2ci  31580  elspansn  31590  nmopval  31880  nmopsetn0  31889  nmfnval  31900  nmfnsetn0  31902  eigvecval  31920  hhcno  31928  hhcnf  31929  nmoplb  31931  nmopub  31932  nmfnlb  31948  nmfnleub  31949  eleigvec  31981  nmlnop0iALT  32019  nmopun  32038  nmcexi  32050  branmfn  32129  pjnmopi  32172  cvbr  32306  hatomic  32384  chrelat2  32394  cdjreui  32456  cdj3lem2  32459  elabreximd  32534  br8d  32635  unipreima  32670  abfmpunirn  32679  curry2ima  32737  toslublem  33003  tosglblem  33005  cyc3genpm  33183  archirng  33219  archiexdiv  33221  archiabllem2a  33225  archiabl  33229  isarchiofld  33230  erlcl1  33291  erlcl2  33292  erldi  33293  erlbrd  33294  erler  33296  fracerl  33337  elgrplsmsn  33420  lsmssass  33432  grplsm0l  33433  grplsmid  33434  mxidlprm  33500  1arithidomlem1  33565  1arithidom  33567  1arithufdlem1  33574  1arithufdlem2  33575  1arithufdlem3  33576  1arithufdlem4  33577  1arithufd  33578  dfufd2  33580  fedgmul  33737  ccfldextdgrr  33778  fldext2chn  33834  constrsslem  33847  constrconj  33851  constrextdg2lem  33854  constrextdg2  33855  constrfiss  33857  constrllcllem  33858  constrlccllem  33859  constrcccllem  33860  crefi  33953  pcmplfin  33966  rspectopn  33973  pstmfval  34002  tpr2rico  34018  rge0scvg  34055  ismntop  34132  esumc  34157  esumpcvgval  34184  esum2dlem  34198  inelsros  34284  diffiunisros  34285  dya2icoseg2  34384  dya2iocuni  34389  eulerpartlemgvv  34482  eulerpartlemgh  34484  hgt749d  34755  tgoldbachgt  34769  bnj66  34965  bnj873  35029  bnj18eq1  35032  bnj1234  35118  bnj1318  35130  onvf1odlem3  35248  vonf1owev  35251  cplgredgex  35264  subfacp1lem3  35325  pconncn  35367  cnpconn  35373  txpconn  35375  connpconn  35378  iscvm  35402  cvmcov  35406  cvmopnlem  35421  cvmliftlem15  35441  cvmlift3lem2  35463  cvmlift3lem4  35465  cvmlift3  35471  satf  35496  satfv1  35506  satfvsucsuc  35508  satfbrsuc  35509  satfrnmapom  35513  satf0op  35520  sat1el2xp  35522  fmlafvel  35528  fmlasuc  35529  fmla1  35530  isfmlasuc  35531  fmlaomn0  35533  fmlasucdisj  35542  satffunlem1lem1  35545  satffunlem1lem2  35546  satffunlem2lem1  35547  dmopab3rexdif  35548  satffunlem2lem2  35549  sategoelfvb  35562  satfv1fvfmla1  35566  2goelgoanfmla1  35567  rexxfr3dALT  35782  r1peuqusdeg1  35786  br8  35899  br6  35900  br4  35901  dfrdg2  35936  dfrdg3  35937  altxpeq2  36117  funtransport  36174  fvtransport  36175  brcolinear2  36201  colineardim1  36204  segcon2  36248  brsegle  36251  funray  36283  fvray  36284  funline  36285  linedegen  36286  fvline  36287  ellines  36295  prodeq12sdv  36361  cbvsumdavw  36422  cbvproddavw  36423  cbvsumdavw2  36438  cbvproddavw2  36439  nn0prpwlem  36465  fnessref  36500  neibastop2lem  36503  neibastop2  36504  tailfb  36520  unblimceq0lem  36649  unblimceq0  36650  unbdqndv2  36654  bj-finsumval0  37429  relowlssretop  37507  nlpineqsn  37552  pibp19  37558  phpreu  37744  matunitlindflem2  37757  ptrest  37759  poimirlem4  37764  poimirlem17  37777  poimirlem20  37780  poimirlem24  37784  poimirlem26  37786  poimirlem27  37787  poimirlem28  37788  poimirlem31  37791  poimirlem32  37792  poimir  37793  heicant  37795  mblfinlem1  37797  mblfinlem3  37799  mblfinlem4  37800  ismblfin  37801  itg2addnclem  37811  itg2addnclem3  37813  itg2addnc  37814  itg2gt0cn  37815  ftc1anclem6  37838  unirep  37854  indexa  37873  sdclem2  37882  sdclem1  37883  sdc  37884  fdc  37885  fdc1  37886  incsequz  37888  istotbnd  37909  sstotbnd2  37914  equivtotbnd  37918  isbnd  37920  bndss  37926  ssbnd  37928  totbndbnd  37929  ismtybndlem  37946  heibor1lem  37949  heiborlem1  37951  heiborlem6  37956  heiborlem8  37958  heiborlem10  37960  heibor  37961  rngoid  38042  isgrpda  38095  isdrngo2  38098  divrngidl  38168  prnc  38207  isfldidl  38208  exanres3  38434  brcoels  38637  br1cossxrnres  38650  eldm1cossres2  38663  prtlem5  39059  prtlem13  39067  prtlem16  39068  islshp  39178  lsmsat  39207  lcvbr  39220  lsatcv0  39230  lshpsmreu  39308  lshpkrlem1  39309  lshpkrlem2  39310  lshpkrlem3  39311  lshpkrcl  39315  lshpset2N  39318  islshpkrN  39319  cvrval  39468  atlex  39515  glbconxN  39577  hlsuprexch  39580  islln  39705  islpln  39729  islpln5  39734  lvolex3N  39737  islvol  39772  islvol5  39778  ispointN  39941  pmapglbx  39968  paddval  39997  elpaddn0  39999  elpaddat  40003  elpadd0  40008  4atex  40275  4atex2  40276  cdlemefrs29bpre1  40596  cdlemefrs32fva  40599  cdlemg33b  40906  dvhb1dimN  41185  dvhopellsm  41316  dib1dim  41364  diclspsn  41393  dihglblem2aN  41492  dihglblem2N  41493  dih1dimatlem  41528  dvh3dimatN  41638  dvh2dim  41644  dvh3dim  41645  dvh4dimN  41646  dvh3dim3N  41648  dochfl1  41675  lcfl7N  41700  lcf1o  41750  lcfrlem39  41780  mapdpglem3  41874  hvmapvalvalN  41960  hdmap14lem2a  42066  hdmapglem7a  42126  3factsumint1  42214  primrootsunit1  42290  primrootscoprmpow  42292  primrootscoprbij  42295  remexz  42297  aks6d1c2p2  42312  aks6d1c6lem5  42370  aks5lem8  42394  exfinfldd  42396  3rspcedvd  42413  nnn1suc  42463  sn-negex12  42614  fimgmcyclem  42730  prjspeclsp  42797  elrfi  42878  isnacs  42888  nacsfg  42889  nacsfix  42896  mzpcompact2lem  42935  eldiophb  42941  eldioph  42942  eldioph2  42946  eldioph2b  42947  eldioph3  42950  eldiophss  42958  diophrex  42959  sbcrexgOLD  42969  sbc2rexgOLD  42972  rexrabdioph  42978  rexfrabdioph  42979  elnn0rabdioph  42987  dvdsrabdioph  42994  eldioph4b  42995  eldioph4i  42996  diophren  42997  rencldnfilem  43004  pell1234qrdich  43045  jm2.27  43192  expdiophlem1  43205  wepwsolem  43226  aomclem8  43245  islnr3  43299  lnr2i  43300  lpirlnr  43301  hbtlem1  43307  hbtlem2  43308  hbtlem7  43309  hbtlem4  43310  hbtlem5  43312  hbtlem6  43313  dgraaval  43328  dgraalem  43329  dgraaub  43332  rngunsnply  43353  onsupmaxb  43423  onexoegt  43428  onsucelab  43447  limnsuc  43449  oaordnr  43480  omnord1  43489  oenord1  43500  oaomoencom  43501  oenass  43503  cantnfresb  43508  tfsconcatfv2  43524  tfsconcatb0  43528  tfsconcat0i  43529  ofoafo  43540  naddcnffo  43548  oaun3lem1  43558  oadif1lem  43563  oadif1  43564  minregex2  43718  brtrclfv2  43910  clsk1indlem1  44228  extoimad  44347  mnuop123d  44445  mnuop23d  44449  mnuprdlem1  44455  mnuprdlem2  44456  ismnushort  44484  rexabsobidv  45156  omssaxinf2  45171  disjrnmpt2  45374  upbdrech  45495  ssfiunibd  45499  supxrgere  45520  supxrgelem  45524  supxrge  45525  suplesup  45526  infxr  45553  infleinf  45558  supxrunb3  45585  unb2ltle  45601  uzub  45617  supminfxr  45650  iccshift  45706  iooshift  45710  climinf  45794  climinff  45799  ellimcabssub0  45805  climf  45810  limcperiod  45816  limclner  45837  climf2  45852  clim2d  45859  limsuppnfd  45888  limsuppnf  45897  climinfmpt  45901  limsupubuzmpt  45905  limsupmnf  45907  limsupre2lem  45910  limsupre2  45911  limsupmnfuz  45913  limsupre2mpt  45916  limsupre3lem  45918  limsupre3  45919  limsupre3mpt  45920  limsupre3uzlem  45921  limsupre3uz  45922  limsupreuz  45923  limsupreuzmpt  45925  climuz  45930  liminfreuzlem  45988  liminfreuz  45989  xlimmnfvlem1  46018  xlimmnfv  46020  xlimpnfvlem1  46022  xlimpnfv  46024  cncfshiftioo  46078  fperdvper  46105  itgiccshift  46166  itgperiod  46167  stoweidlem27  46213  stoweidlem31  46217  stoweidlem43  46229  stoweidlem46  46232  stoweidlem52  46238  stoweidlem60  46246  fourierdlem42  46335  fourierdlem48  46340  fourierdlem51  46343  fourierdlem54  46346  fourierdlem63  46355  fourierdlem64  46356  fourierdlem65  46357  fourierdlem68  46360  fourierdlem70  46362  fourierdlem71  46363  fourierdlem73  46365  fourierdlem80  46372  fourierdlem81  46373  fourierdlem89  46381  fourierdlem90  46382  fourierdlem91  46383  fourierdlem92  46384  fourierdlem96  46388  fourierdlem97  46389  fourierdlem98  46390  fourierdlem99  46391  fourierdlem100  46392  fourierdlem103  46395  fourierdlem104  46396  fourierdlem105  46397  fourierdlem108  46400  fourierdlem109  46401  fourierdlem110  46402  fourierdlem112  46404  fourierdlem113  46405  sge0pnffigt  46582  sge0resplit  46592  ovnval2  46731  ovnval2b  46738  ovnlecvr  46744  ovnpnfelsup  46745  ovn0lem  46751  ovnsubaddlem1  46756  hoidmvlelem1  46781  ovnhoilem1  46787  ovnhoi  46789  ovnlecvr2  46796  hoiqssbl  46811  ovolval5lem2  46839  ovolval5lem3  46840  ovolval5  46841  ovnovol  46845  smfsuplem2  46998  smfsup  47000  smfinflem  47003  smfinf  47004  fsetsnf  47239  fsetsnfo  47241  cfsetsnfsetf  47246  cfsetsnfsetfo  47248  cbvrex2  47292  2reu8i  47301  2reuimp0  47302  afvelrnb  47351  afvelrnb0  47352  elsetpreimafvb  47572  imasetpreimafvbijlemfo  47593  iccelpart  47621  iccpartiun  47622  icceuelpart  47624  sprsymrelf1lem  47679  sprsymrelf  47683  fmtnofac2lem  47756  fmtnofac2  47757  fmtnofac1  47758  m1expevenALTV  47835  odd2np1ALTV  47862  opoeALTV  47871  opeoALTV  47872  mogoldbblem  47908  nfermltlrev  47932  isgbow  47940  isgbo  47941  7gbow  47960  9gbo  47962  11gbo  47963  sbgoldbwt  47965  mogoldbb  47973  sbgoldbo  47975  nnsum3primesgbe  47980  nnsum4primesodd  47984  nnsum4primesoddALTV  47985  bgoldbtbnd  47997  dfclnbgr2  48011  clnbgrel  48016  dfsclnbgr2  48034  sclnbgrel  48035  sclnbgrelself  48036  vopnbgrel  48042  vopnbgrelself  48043  dfclnbgr6  48044  dfnbgr6  48045  dfsclnbgr6  48046  clnbgrgrim  48122  stgredgel  48145  stgrusgra  48147  stgr1  48149  isubgr3stgrlem4  48157  isubgr3stgrlem6  48159  grlimgrtri  48191  gpgov  48230  gpgiedgdmel  48237  gpgedgel  48238  gpgprismgr4cycllem3  48285  gpgprismgr4cycllem10  48292  uspgrsprf1  48335  uspgrsprfo  48336  0nodd  48358  1odd  48359  2nodd  48360  0even  48425  1neven  48426  2even  48427  2zlidl  48428  2zrngamgm  48433  2zrngagrp  48437  2zrngmmgm  48440  2zrngnmrid  48444  lcoval  48600  el0ldep  48654  ldepspr  48661  zlmodzxzldep  48692  line  48920  rrxline  48922  sepnsepo  49111