Theorem ralbidv 3164

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

Hypothesis

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

Assertion

Ref	Expression
ralbidv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem ralbidv

Step	Hyp	Ref	Expression
1		ralbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 482	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	ralbidva 3162	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2121  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 209  df-an 398  df-ral 3056

This theorem is referenced by:  2ralbidv  3205  rexralbidv  3207  3ralbidv  3208  4ralbidv  3209  cbvral2vw  3223  cbvral4vw  3226  cbvral2v  3334  rspceaimv  3567  rspc2  3570  rspc2v  3572  rspc3v  3577  rspc4v  3581  reu6i  3670  reu7  3674  sbcralt  3805  reu8nf  3810  raaan  4448  raaanv  4449  raaan2  4452  2reu4lem  4453  reusngf  4608  2ralsng  4612  rexreusng  4613  reuprg0  4636  issn  4765  2ralunsn  4828  elintg  4887  elintrabg  4893  eliin  4928  disjprg  5070  disjxun  5072  brralrspcev  5134  reusv2lem2  5330  reusv3  5336  poeq1  5531  solin  5555  somo  5567  frirr  5596  fr2nr  5597  frminex  5599  wereu2  5617  posn  5706  frsn  5708  ralxpf  5790  cnvpo  6241  reu3op  6246  reuop  6247  dfpo2  6250  frpomin  6294  fnmptfvd  6985  iinpreima  7013  dff4  7045  dff13f  7202  fpropnf1  7214  f1ounsn  7219  eusvobj2  7351  ovanraleqv  7383  f1opr  7415  ofreq  7627  sorpssuni  7678  sorpssint  7679  fr3nr  7718  onssmin  7738  funcnvuni  7876  f1oweALT  7916  frxp  8068  frxp2  8086  xpord2indlem  8089  frxp3  8093  xpord3inddlem  8096  poseq  8100  soseq  8101  frecseq123  8225  csbfrecsg  8227  frrlem1  8229  frrlem13  8241  smoeq  8283  tfrlem12  8322  tz7.48lem  8374  naddcllem  8606  naddov2  8609  naddunif  8623  naddasslem1  8624  naddasslem2  8625  elixp2  8843  undifixp  8876  xpf1o  9071  nneneq  9134  ac6sfi  9188  frfi  9189  fipreima  9262  indexfi  9264  marypha1lem  9340  marypha1  9341  supeq1  9352  supeq3  9356  supmo  9359  eqsup  9363  supub  9366  suplub  9367  sup0  9374  supisoex  9382  eqinf  9392  infval  9394  infmo  9404  oieq1  9421  ordtypecbv  9426  ordtypelem3  9429  ordtypelem6  9432  ordtypelem7  9433  ordtypelem9  9435  wemaplem1  9455  wemaplem2  9456  zfregcl  9503  zfregclOLD  9504  oemapval  9599  oemapvali  9600  cantnf  9609  wemapwe  9613  ttrcleq  9625  ttrcltr  9632  ttrclss  9636  ttrclselem2  9642  rankval3b  9745  unbndrank  9761  rankunb  9769  rankuni2b  9772  tcrank  9803  scottex  9804  scottexs  9806  scott0s  9807  bnd2  9812  updjud  9853  dfac8clem  9949  ac5num  9953  acni  9962  acni2  9963  alephval3  10027  dfac4  10039  dfac5lem5  10044  dfac5  10046  dfac2a  10047  dfac2b  10048  dfacacn  10059  kmlem2  10069  kmlem13  10080  cflem  10162  cflemOLD  10163  cflecard  10170  cfeq0  10174  cfsuc  10175  cfflb  10177  cofsmo  10187  cfsmolem  10188  cfcoflem  10190  coftr  10191  alephsing  10194  fin23lem11  10235  isfin3ds  10247  fin23lem17  10256  fin23lem39  10268  isf33lem  10284  isf34lem6  10298  fin1a2lem13  10330  hsmexlem4  10347  hsmex  10350  axcc2lem  10354  axcc3  10356  dcomex  10365  axdc2lem  10366  axdc3lem2  10369  axdc3lem3  10370  axdc3  10372  axdc4lem  10373  axcclem  10375  zorn2lem2  10415  zorn2lem7  10420  zorn2g  10421  zornn0g  10423  ttukeylem7  10433  axdclem2  10438  brdom3  10446  brdom7disj  10449  brdom6disj  10450  alephval2  10491  inar1  10694  axgroth6  10747  pinq  10846  nqereu  10848  prlem934  10952  supexpr  10973  supsrlem  11030  axpre-sup  11088  dedekind  11305  dedekindle  11306  fiminre2  12099  lbreu  12101  sup2  12107  infm3  12110  nnsub  12216  uzwo  12856  nnwof  12859  ublbneg  12878  lbzbi  12881  zsupss  12882  uzsupss  12885  uzwo3  12888  zmax  12890  rpnnen1lem1  12923  rpnnen1lem3  12924  rpnnen1lem4  12925  rpnnen1lem5  12926  xrsupsslem  13254  xrinfmsslem  13255  xrsupss  13256  xrinfmss  13257  flval2  13768  axdc4uzlem  13940  ssnn0fi  13942  fsuppmapnn0fiubex  13949  faclbnd4lem4  14253  bccl  14279  hashgt12el  14379  hashbc  14410  hashge2el2dif  14437  wrdind  14679  wrd2ind  14680  rexanre  15304  rexico  15311  cau4  15314  reusq0  15422  clim  15451  rlim  15452  rlim2  15453  clim2  15461  clim2c  15462  clim0c  15464  rlim0  15465  rlim0lt  15466  ello12r  15474  ello1d  15480  elo12r  15485  rlimresb  15522  rlimcld2  15535  climabs0  15542  rlimo1  15574  lo1add  15584  lo1mul  15585  isercoll  15625  incexclem  15796  sqrt2irr  16211  gcdcllem1  16463  gcdcllem2  16464  dfgcd2  16510  fissn0dvds  16583  dvdslcmf  16595  lcmfledvds  16596  lcmf  16597  lcmfunsnlem1  16601  lcmfunsnlem2lem1  16602  lcmfunsnlem  16605  lcmfdvds  16606  reumodprminv  16770  pc2dvds  16845  pcz  16847  prmpwdvds  16870  infpn2  16879  prmreclem2  16883  prmreclem3  16884  prmreclem5  16886  prmreclem6  16887  vdwlem6  16952  vdwlem8  16954  vdwlem13  16959  vdwnnlem1  16961  vdwnn  16964  ramcl  16995  cshwrepswhash1  17068  prdsleval  17435  imasval  17470  imasaddfnlem  17487  imasvscafn  17496  mrisval  17591  isacs  17612  isacs2  17614  isacs1i  17618  mreacs  17619  acsfn  17620  acsfn2  17624  iscatd  17634  catidex  17635  catideu  17636  cidval  17638  catidd  17641  comfeq  17667  catpropd  17670  ismon  17695  isfunc  17826  isnat  17912  isinito  17958  istermo  17959  isprs  18257  drsdirfi  18266  ispos  18275  lubfval  18309  lubeldm  18312  lubval  18315  lubprop  18317  lublecllem  18319  glbfval  18322  glbeldm  18325  glbval  18328  glbprop  18330  joinval2lem  18339  joinlem  18342  meetval2lem  18353  meetlem  18356  poslubmo  18370  posglbmo  18371  poslubd  18372  resspos  18390  isglbd  18470  lubl  18473  lubun  18476  clatleglb  18479  isdlat  18483  ipodrsima  18502  chneq1  18573  mgm1  18621  gsumval2  18649  mgmhmima  18678  sgrp1  18692  mhmimalem  18787  mndind  18791  gsumwspan  18809  efmndmnd  18852  smndex1mnd  18876  sgrp2rid2  18892  sgrp2rid2ex  18893  sgrp2nmndlem4  18894  pwmnd  18903  dfgrp2  18933  isgrpinv  18964  grpidinv  18969  dfgrp3lem  19009  issubg4  19116  isnsg2  19126  nsgacs  19132  elnmz  19133  cycsubgcl  19176  ghmrn  19198  ghmnsgima  19209  isga  19260  orbsta  19282  cntzfval  19289  elcntz  19291  resscntz  19302  oppgsubg  19332  symgextfo  19391  gsmsymgreqlem2  19400  gsmsymgreq  19401  pmtrdifel  19449  pmtrdifwrdellem3  19452  pmtrdifwrdel2  19455  psgnunilem2  19464  psgnunilem3  19465  odeq  19519  gexid  19550  gexlem2  19551  gexdvds  19553  isslw  19577  sylow2alem1  19586  sylow2alem2  19587  efgval  19686  efgrelexlemb  19719  efgcpbllemb  19724  abl1  19835  dmdprd  19969  dprd2da  20013  pgpfac1lem5  20050  isomnd  20092  ring1  20285  rngisomring  20441  lringuplu  20519  rhmimasubrnglem  20540  isrrg  20673  isabv  20786  islss  20927  lssacs  20960  reslmhm  21045  islbs  21069  pj1lmhm  21093  lbsacsbs  21152  rnglidlmcl  21212  rnglidl0  21225  zringlpir  21445  psgndiflemA  21579  ocvfval  21644  elocv  21646  iunocv  21659  frlmlbs  21775  islindf  21790  islinds2  21791  islindf2  21792  lindfrn  21799  lsslindf  21808  islindf4  21816  opsrval  22025  ply1coe  22287  cply1coe0bi  22291  mat0dimcrng  22456  mdetunilem1  22598  mdetunilem9  22606  cpmat  22695  cpmatel  22697  1elcpmat  22701  m2cpminvid2lem  22740  basgen2  22975  bastop1  22979  isclo  23073  ordtbaslem  23174  iscn  23221  cnpval  23222  iscnp  23223  iscnp3  23230  lmbr  23244  lmbr2  23245  lmbrf  23246  cnprest  23275  cnprest2  23276  t0sep  23310  isreg  23318  t1sep2  23355  tgcmp  23387  1stcclb  23430  1stcfb  23431  2ndc1stc  23437  1stcrest  23439  2ndcdisj  23442  islly  23454  isnlly  23455  lly1stc  23482  isref  23495  islocfin  23503  elkgen  23522  kgencn  23542  elpt  23558  elptr  23559  ptcnplem  23607  tx1stc  23636  cnmpt21  23657  kqt0lem  23722  isr0  23723  regr1lem2  23726  r0sep  23734  nrmr0reg  23735  flffbas  23981  cnflf  23988  cnflf2  23989  lmflf  23991  txflf  23992  fclsopni  24001  fclsnei  24005  fclsrest  24010  fcfnei  24021  cnfcf  24028  alexsubb  24032  alexsubALTlem3  24035  qustgplem  24107  tsmsfbas  24114  tsmsres  24130  tsmsf1o  24131  tsmsxplem1  24139  ustval  24189  isust  24190  ustincl  24194  ustdiag  24195  ustinvel  24196  ustexhalf  24197  ust0  24206  utopval  24218  ucnval  24262  isucn  24263  isucn2  24264  ucnima  24266  iscfilu  24273  ispsmet  24290  ismet  24309  isxmet  24310  imasdsf1olem  24359  imasf1oxmet  24361  imasf1omet  24362  metss  24494  met1stc  24507  prdsxmslem2  24515  txmetcnp  24533  metucn  24557  tngngp3  24642  nlmvscn  24673  nmoval  24701  nmolb  24703  qtopbaslem  24744  cncfval  24876  elcncf2  24878  mulc1cncf  24893  cncfmet  24897  evth  24947  lebnumlem3  24951  lebnum  24952  xlebnum  24953  ishtpy  24960  isphtpy  24969  pi1xfr  25043  pi1coghm  25049  isclmp  25085  ipcn  25234  lmmbr2  25247  lmmbr3  25248  lmmbrf  25250  cfilfval  25252  iscfil  25253  fmcfil  25260  caufval  25263  iscau  25264  iscau2  25265  iscau3  25266  iscau4  25267  iscauf  25268  caucfil  25271  cfilresi  25283  causs  25286  lmclim  25291  cmetcusp1  25341  minveclem4c  25413  minveclem2  25414  minveclem3b  25416  minveclem4  25420  minveclem6  25422  minveclem7  25423  ovolicc2lem3  25507  ismbl  25514  dyadmax  25586  dyadmbllem  25587  dyadmbl  25588  opnmbllem  25589  ismbf1  25612  ismbf  25616  mbfeqalem2  25630  mbflimsup  25654  mbfi1fseqlem6  25708  mbfi1flimlem  25710  itg2seq  25730  itg2monolem1  25738  isibl  25753  ply1divex  26123  fta1g  26156  dgrco  26261  plydivex  26284  fta1  26295  vieta1  26299  aannenlem1  26315  aannenlem2  26316  aalioulem2  26320  aalioulem3  26321  ulmval  26366  ulm2  26371  ulmi  26372  ulmres  26374  ulmshftlem  26375  ulmcaulem  26380  ulmcau  26381  ulmss  26383  ulmbdd  26384  ulmdvlem1  26386  ulmdvlem3  26388  pilem2  26438  pilem3  26439  cxpcn3  26733  dmarea  26942  rlimcnp  26950  scvxcvx  26970  lgamgulmlem2  27014  lgamgulmlem3  27015  lgamgulmlem5  27017  lgambdd  27021  lgamcvglem  27024  isppw2  27099  perfectlem2  27214  2sqlem6  27407  2sqlem10  27412  addsq2reu  27424  2sqreulem1  27430  2sqreunnlem1  27433  dchrisumlema  27472  dchrisumlem2  27474  dchrisumlem3  27475  pntpbnd  27572  pntibndlem3  27576  pntibnd  27577  pntleme  27592  pntlem3  27593  pntlemp  27594  pnt3  27596  ltsval  27631  nosupprefixmo  27684  noinfprefixmo  27685  nosupcbv  27686  nosupno  27687  nosupdm  27688  nosupfv  27690  nosupres  27691  nosupbnd1lem1  27692  nosupbnd1lem3  27694  nosupbnd1lem5  27696  noinfcbv  27701  noinfno  27702  noinfdm  27703  noinffv  27705  noinfres  27706  noinfbnd1lem3  27709  noinfbnd1lem5  27711  noetalem1  27725  noetalem2  27726  nocvxminlem  27766  brslts  27774  sltssnb  27781  conway  27791  etaslts  27805  lesrec  27811  eqcuts3  27816  madebdaylemlrcut  27911  madebday  27912  bdayle  27928  cofcutr  27936  cutmax  27946  cutmin  27947  lrrecfr  27955  addsprop  27988  negsunif  28067  addonbday  28291  onsfi  28368  n0subs  28375  bdayn0p1  28381  bdaypw2n0bndlem  28475  bdayfinbndlem2  28480  z12zsodd  28494  istrkgld  28547  axtg5seg  28553  tgcgr4  28619  perpln1  28798  perpln2  28799  isperp  28800  brbtwn2  28994  colinearalg  28999  axsegconlem1  29006  axsegcon  29016  ax5seglem4  29021  ax5seglem5  29022  axlowdim  29050  axeuclidlem  29051  axcontlem1  29053  axcontlem2  29054  axcontlem4  29056  axcontlem5  29057  axcontlem8  29060  axcontlem12  29064  elntg2  29074  uvtxusgr  29491  rgrx0ndm  29682  ewlksfval  29690  wksfval  29698  wwlks  29923  wlkiswwlks2  29963  clwwlk  30073  1conngr  30284  frgrwopregasn  30406  frgrwopregbsn  30407  frgrwopreglem5ALT  30412  frgrregord013  30485  isgrpo  30588  isgrpoi  30589  grpoideu  30600  grpoidinv2  30606  vciOLD  30652  isvclem  30668  cnidOLD  30673  isnvlem  30701  nvi  30705  lnoval  30843  islno  30844  isblo3i  30892  blo3i  30893  blocnilem  30895  ajfval  30900  ubthlem1  30961  ubthlem2  30962  ubthlem3  30963  ubth  30964  minvecolem2  30966  minvecolem3  30967  minvecolem4c  30970  minvecolem4  30971  minvecolem5  30972  minvecolem6  30973  minvecolem7  30974  h2hcau  31070  h2hlm  31071  hilid  31252  hcau  31275  hlimi  31279  hlim2  31283  ocel  31372  adjsym  31924  ellnop  31949  ellnfn  31974  hhcno  31995  hhcnf  31996  lnopeq  32100  elunop2  32104  lnophm  32110  lnconi  32124  lnopcnbd  32127  lnfncnbd  32148  imaelshi  32149  riesz3i  32153  riesz4i  32154  riesz4  32155  riesz1  32156  cnlnadjlem2  32159  cnlnadjlem5  32162  cnlnadjlem8  32165  cnlnadji  32167  nmopadjlei  32179  cnvbraval  32201  leopg  32213  leoppos  32217  mdbr  32385  dmdbr  32390  cdj3i  32532  disjunsn  32685  funcnv5mpt  32761  fgreu  32765  fcnvgreu  32766  xrge0infss  32854  wrdt2ind  33034  mgccole1  33071  mgccole2  33072  mgcmnt1  33073  mgcmnt2  33074  gsumhashmul  33150  isfxp  33251  fxpgaeq  33252  inftmrel  33263  isinftm  33264  archiabl  33281  isarchiofld  33282  elrgspnlem4  33328  0nellinds  33455  lindssn  33463  elrspunidl  33513  prmidl  33525  ismxidl  33547  1arithidom  33630  1arithufdlem3  33639  evl1deg1  33669  evl1deg2  33670  evl1deg3  33671  vietalem  33773  vieta  33774  crefeq  34039  zarcmplem  34075  esum2d  34287  sigaval  34305  issgon  34317  isrnmeas  34394  ismbfm  34445  mbfmcst  34453  elcarsg  34499  sitgval  34526  eulerpartlemd  34560  ballotleme  34691  tgoldbachgt  34857  bnj1185  34988  bnj1385  35027  bnj66  35055  bnj106  35063  bnj155  35074  bnj852  35116  bnj893  35123  bnj1228  35206  bnj1234  35208  bnj1463  35250  nummin  35287  rankfilimbi  35295  r1omhfb  35306  fineqvnttrclse  35318  r1omhfbregs  35331  gblacfnacd  35343  onvf1odlem4  35347  vonf1owev  35349  derangenlem  35412  subfacp1lem3  35423  subfacp1lem5  35425  subfacp1lem6  35426  subfacp1  35427  erdszelem8  35439  kur14  35457  cnpconn  35471  resconn  35487  cvmscbv  35499  iscvm  35500  cvmsi  35506  cvmsval  35507  cvmlift3lem2  35561  snmlval  35572  satfv1  35604  fmlasucdisj  35640  satffunlem1lem1  35643  satffunlem2lem1  35645  satfv1fvfmla1  35664  mclsssvlem  35803  mclsval  35804  mclsax  35810  mclsind  35811  dfon2lem9  36030  dfrdg2  36034  dfrdg3  36035  fwddifnval  36404  nn0prpwlem  36563  isfne  36580  isfne4  36581  isfne2  36583  isfne3  36584  neibastop3  36603  topmeet  36605  topjoin  36606  filnetlem4  36622  weiunlem  36704  weiunfrlem  36705  dfttc4lem1  36769  dfttc4  36771  elttcirr  36772  unblimceq0lem  36825  unblimceq0  36826  unbdqndv2  36830  taupilemrplb  37693  fin2so  37987  lindsadd  37993  matunitlindflem2  37997  ptrecube  38000  poimirlem2  38002  poimirlem3  38003  poimirlem4  38004  poimirlem24  38024  poimirlem25  38025  poimirlem26  38026  poimirlem27  38027  poimirlem28  38028  poimirlem29  38029  poimirlem30  38030  poimirlem32  38032  poimir  38033  heicant  38035  mblfinlem1  38037  mblfinlem2  38038  voliunnfl  38044  volsupnfl  38045  mbfresfi  38046  itg2addnc  38054  upixp  38109  indexdom  38114  filbcmb  38120  sdclem2  38122  fdc  38125  lmclim2  38138  caures  38140  istotbnd  38149  istotbnd3  38151  sstotbnd  38155  isbnd  38160  heibor  38201  bfp  38204  rrncmslem  38212  isgrpda  38335  idlval  38393  isidl  38394  0idl  38405  unichnidl  38411  pridl  38417  ismaxidl  38420  smprngopr  38432  igenval2  38446  prnc  38447  ispridlc  38450  scottexf  38548  scott0f  38549  disjsuc2  38794  riotasvd  39461  islfl  39565  eqlkr  39604  eqlkr3  39606  glbconN  39882  hlsuprexch  39886  ispsubsp  40250  ldilset  40614  isldil  40615  dilsetN  40658  isdilN  40659  trlset  40666  trlval  40667  cdleme27b  40873  cdleme29b  40880  cdleme31so  40884  cdleme31sn1  40886  cdleme31sn1c  40893  cdleme31fv  40895  cdleme40v  40974  istendo  41265  cdlemkid3N  41438  cdlemkid4  41439  cdlemkid5  41440  dihfval  41736  dihval  41737  islpolN  41988  hdmapffval  42331  hdmapfval  42332  hdmapval  42333  hdmapval2lem  42336  hgmapffval  42390  hgmapfval  42391  hgmapval  42392  hgmapvs  42396  isprimroot  42591  aks6d1c1p1  42605  hashscontpow1  42619  sticksstones2  42645  unitscyglem3  42695  exfinfldd  42701  qsalrel  42738  supinf  42739  sn-sup2  42994  fsuppind  43053  isnacs  43166  isnacs2  43168  nacsfix  43174  mzpclval  43187  elmzpcl  43188  rencldnfilem  43278  infmrgelbi  43336  pellfundre  43339  pellfundlb  43342  wepwsolem  43500  fnwe2lem2  43509  aomclem8  43519  dfac11  43520  gicabl  43557  islnr3  43573  hbtlem2  43582  hbtlem5  43586  onintunirab  43685  onsucf1lem  43727  cantnfresb  43782  safesnsupfilb  43875  rp-brsslt  43880  fiinfi  44030  clsk1independent  44503  ntrclsk13  44528  gneispacess2  44603  imo72b2lem0  44622  imo72b2lem2  44624  imo72b2lem1  44626  imo72b2  44629  scottelrankd  44704  mnuop23d  44723  ismnushort  44758  ralabsobidv  45429  0elaxnul  45440  pwclaxpow  45441  prclaxpr  45442  uniclaxun  45443  omssaxinf2  45445  modelac8prim  45449  wfac8prim  45459  permac8prim  45471  evth2f  45476  evthf  45488  fnchoice  45490  uzwo4  45514  wessf1ornlem  45644  disjinfi  45651  rnmptlb  45699  rnmptbdd  45701  rnmptbd2  45705  rnmptbd  45712  dstregt0  45742  upbdrech2  45768  rexabslelem  45873  rexabsle  45874  uzub  45886  infrpgernmpt  45920  mccl  46055  ellimcabssub0  46074  climf  46079  clim2f  46091  limsupre  46096  clim2cf  46105  clim0cf  46109  climf2  46121  clim2f2  46125  clim2d  46128  limsupref  46140  limsupbnd1f  46141  climinf2  46162  limsuppnf  46166  climinfmpt  46170  climinf3  46171  limsupubuzmpt  46174  limsupmnf  46176  limsupre2lem  46179  limsupre2  46180  limsupmnfuzlem  46181  limsupmnfuz  46182  limsupre2mpt  46185  limsupre3lem  46187  limsupre3  46188  limsupre3mpt  46189  limsupre3uz  46191  limsupreuz  46192  limsupreuzmpt  46194  climuz  46199  liminfreuzlem  46257  liminfreuz  46258  cnrefiisplem  46284  xlimmnfvlem1  46287  xlimmnfv  46289  xlimpnfvlem1  46291  xlimpnfv  46293  xlimmnfmpt  46298  xlimpnfmpt  46299  cncfshift  46329  cncfperiod  46334  fperdvper  46374  dvbdfbdioo  46385  ioodvbdlimc1lem2  46387  ioodvbdlimc2lem  46389  dvnprodlem3  46403  stoweidlem5  46460  stoweidlem9  46464  stoweidlem15  46470  stoweidlem16  46471  stoweidlem27  46482  stoweidlem28  46483  stoweidlem31  46486  stoweidlem34  46489  stoweidlem37  46492  stoweidlem46  46501  stoweidlem48  46503  stoweidlem51  46506  stoweidlem52  46507  stoweidlem59  46514  wallispilem3  46522  stirlinglem13  46541  fourierdlem2  46564  fourierdlem3  46565  fourierdlem16  46578  fourierdlem20  46582  fourierdlem21  46583  fourierdlem22  46584  fourierdlem25  46587  fourierdlem39  46601  fourierdlem42  46604  fourierdlem54  46615  fourierdlem64  46625  fourierdlem77  46638  fourierdlem83  46644  fourierdlem103  46664  fourierdlem104  46665  subsaliuncllem  46812  iundjiun  46915  meaiunincf  46938  caragenval  46948  isome  46949  caragenel  46950  omessle  46953  ovnlerp  47017  hoidmvlelem3  47052  hoidmvle  47055  issmflem  47182  issmfgt  47211  smfmullem2  47247  smfmullem4  47249  smfmul  47250  smfsuplem2  47267  smfsup  47269  smfinflem  47272  smfinf  47273  fsupdm  47297  finfdm  47301  cfsetsnfsetf  47533  cbvral2  47578  2reu8i  47588  2reuimp0  47589  dfdfat2  47603  iccpart  47903  iccpartigtl  47910  paireqne  47998  reupr  48009  perfectALTVlem2  48225  bgoldbachlt  48316  tgoldbachlt  48319  grimidvtxedg  48388  grimcnv  48391  grimco  48392  isuspgrim0  48397  gricushgr  48420  ushggricedg  48430  uhgrimisgrgric  48434  isubgr3stgr  48478  isgrlim  48485  isgrlim2  48486  uspgrlim  48495  grlicsym  48516  grlictr  48518  gpg5nbgrvtx03star  48583  gpg5nbgr3star  48584  pgnbgreunbgr  48628  upwlksfval  48638  nn0mnd  48682  uzlidlring  48738  ply1mulgsumlem1  48889  ply1mulgsumlem2  48890  linindslinci  48951  lindslinindsimp1  48960  lindslinindsimp2lem5  48965  lindslinindsimp2  48966  linds0  48968  lindsrng01  48971  snlindsntor  48974  lmod1  48995  ldepsnlinc  49011  bigoval  49052  elbigo2r  49056  nn0sumshdiglem2  49125  eenglngeehlnmlem1  49240  eenglngeehlnmlem2  49241  lubeldm2d  49460  glbeldm2d  49461  lubsscl  49462  glbsscl  49463  ipolubdm  49489  ipolub  49490  ipoglbdm  49492  ipoglb  49493  nelsubc3lem  49572  upfval2  49679  upfval3  49680  isthincd2lem2  49937  setc1onsubc  50104  cnelsubclem  50105  setrec1lem2  50190