Theorem ralbidv 3185

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 486	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	ralbidva 3183	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077

This theorem is used by:  2ralbidv  3226  rexralbidv  3228  3ralbidv  3229  4ralbidv  3230  cbvral2vw  3244  cbvral4vw  3247  cbvral2v  3353  rspceaimv  3582  rspc2  3585  rspc2v  3587  rspc3v  3592  rspc4v  3596  reu6i  3686  reu7  3690  sbcralt  3819  reu8nf  3824  raaan  4474  raaanv  4475  raaan2  4478  2reu4lem  4479  reusngf  4635  2ralsng  4639  rexreusng  4640  reuprg0  4663  issn  4792  2ralunsn  4855  elintg  4915  elintrabg  4921  eliin  4956  disjprg  5099  disjxun  5101  brralrspcev  5165  reusv2lem2  5361  reusv3  5367  poeq1  5559  solin  5583  somo  5595  frirr  5624  fr2nr  5625  frminex  5627  wereu2  5645  posn  5734  frsn  5736  ralxpf  5821  cnvpo  6280  reu3op  6285  reuop  6286  dfpo2  6289  frpomin  6333  fnmptfvd  7029  iinpreima  7058  dff4  7090  dff13f  7248  fpropnf1  7260  f1ounsn  7269  eusvobj2  7401  ovanraleqv  7433  f1opr  7465  ofreq  7681  sorpssuni  7732  sorpssint  7733  fr3nr  7770  onssmin  7790  funcnvuni  7928  f1oweALT  7968  frxp  8122  frxp2  8140  xpord2indlem  8143  frxp3  8147  xpord3inddlem  8150  poseq  8154  soseq  8155  frecseq123  8279  csbfrecsg  8281  frrlem1  8283  frrlem13  8295  smoeq  8337  tfrlem12  8376  tz7.48lemOLD  8430  naddcllem  8664  naddov2  8667  naddunif  8682  naddasslem1  8683  naddasslem2  8684  elixp2  8908  undifixp  8941  xpf1o  9137  nneneq  9200  ac6sfi  9254  frfi  9255  fipreima  9325  indexfi  9327  marypha1lem  9403  marypha1  9404  supeq1  9415  supeq3  9419  supmo  9422  eqsup  9426  supub  9429  suplub  9430  sup0  9437  supisoex  9445  eqinf  9455  infval  9457  infmo  9467  oieq1  9484  ordtypecbv  9489  ordtypelem3  9492  ordtypelem6  9495  ordtypelem7  9496  ordtypelem9  9498  wemaplem1  9518  wemaplem2  9519  zfregcl  9566  zfregclOLD  9567  oemapval  9662  oemapvali  9663  cantnf  9672  wemapwe  9676  ttrcleq  9688  ttrcltr  9695  ttrclss  9699  ttrclselem2  9705  rankval3b  9808  unbndrank  9825  rankunb  9834  rankuni2b  9837  tcrank  9870  scottex  9890  scottexOLD  9891  scottexsOLD  9900  scott0bsOLD  9902  scottelrankd  9905  bnd2  9913  setrec1lem2  9924  updjud  9972  dfac8clem  10068  ac5num  10072  acni  10081  acni2  10082  alephval3  10146  dfac4  10158  dfac5lem5  10163  dfac5  10164  dfac2a  10165  dfac2b  10166  dfacacn  10177  kmlem2  10187  kmlem13  10198  cflem  10280  cflecard  10287  cfeq0  10291  cfsuc  10292  cfflb  10294  cofsmo  10304  cfsmolem  10305  cfcoflem  10307  coftr  10308  alephsing  10311  fin23lem11  10352  isfin3ds  10364  fin23lem17  10373  fin23lem39  10385  isf33lem  10401  isf34lem6  10415  fin1a2lem13  10447  hsmexlem4  10464  hsmex  10467  axcc2lem  10471  axcc3  10473  dcomex  10482  axdc2lem  10483  axdc3lem2  10486  axdc3lem3  10487  axdc3  10489  axdc4lem  10490  axcclem  10492  zorn2lem2  10532  zorn2lem7  10537  zorn2g  10538  zornn0g  10540  ttukeylem7  10550  axdclem2  10555  brdom3  10564  brdom7disj  10567  brdom6disj  10568  alephval2  10614  inar1  10817  axgroth6  10870  pinq  10969  nqereu  10971  prlem934  11075  supexpr  11096  supsrlem  11153  axpre-sup  11211  dedekind  11430  dedekindle  11431  fiminre2  12220  lbreu  12222  sup2  12228  infm3  12231  nnsub  12337  uzwo  12993  nnwof  12996  ublbneg  13015  lbzbi  13018  zsupss  13019  uzsupss  13022  uzwo3  13025  zmax  13027  rpnnen1lem1  13061  rpnnen1lem3  13062  rpnnen1lem4  13063  rpnnen1lem5  13064  xrsupsslem  13392  xrinfmsslem  13393  xrsupss  13394  xrinfmss  13395  flval2  13908  axdc4uzlem  14080  ssnn0fi  14082  fsuppmapnn0fiubex  14089  faclbnd4lem4  14393  bccl  14419  hashgt12el  14520  hashbc  14551  hashge2el2dif  14578  wrdind  14824  wrd2ind  14825  rexanre  15467  rexico  15474  cau4  15477  reusq0  15585  clim  15614  rlim  15615  rlim2  15616  clim2  15624  clim2c  15625  clim0c  15627  rlim0  15628  rlim0lt  15629  ello12r  15637  ello1d  15643  elo12r  15648  rlimresb  15685  rlimcld2  15698  climabs0  15705  rlimo1  15737  lo1add  15747  lo1mul  15748  isercoll  15788  incexclem  15958  sqrt2irr  16370  gcdcllem1  16622  gcdcllem2  16623  dfgcd2  16669  fissn0dvds  16742  dvdslcmf  16754  lcmfledvds  16755  lcmf  16756  lcmfunsnlem1  16760  lcmfunsnlem2lem1  16761  lcmfunsnlem  16764  lcmfdvds  16765  reumodprminv  16929  pc2dvds  17004  pcz  17006  prmpwdvds  17029  infpn2  17038  prmreclem2  17042  prmreclem3  17043  prmreclem5  17045  prmreclem6  17046  vdwlem6  17111  vdwlem8  17113  vdwlem13  17118  vdwnnlem1  17120  vdwnn  17123  ramcl  17154  cshwrepswhash1  17227  prdsleval  17595  imasval  17630  imasaddfnlem  17647  imasvscafn  17656  mrisval  17751  isacs  17772  isacs2  17774  isacs1i  17778  mreacs  17779  acsfn  17780  acsfn2  17784  iscatd  17794  catidex  17795  catideu  17796  cidval  17798  catidd  17801  comfeq  17827  catpropd  17830  ismon  17855  isfunc  17986  isnat  18072  isinito  18118  istermo  18119  isprs  18417  drsdirfi  18426  ispos  18435  lubfval  18469  lubeldm  18472  lubval  18475  lubprop  18477  lublecllem  18479  glbfval  18482  glbeldm  18485  glbval  18488  glbprop  18490  joinval2lem  18499  joinlem  18502  meetval2lem  18513  meetlem  18516  poslubmo  18530  posglbmo  18531  poslubd  18532  resspos  18550  isglbd  18630  lubl  18633  lubun  18636  clatleglb  18639  isdlat  18643  ipodrsima  18662  chneq1  18733  mgm1  18783  idressid  18809  gsumval2  18822  mgmhmima  18851  sgrp1  18865  mhmimalem  18967  mndind  18971  gsumwspan  18989  efmndmnd  19032  smndex1mnd  19056  sgrp2rid2  19072  sgrp2rid2ex  19073  sgrp2nmndlem4  19074  degenmgm  19084  degenmgm2  19087  pwmnd  19090  dfgrp2  19120  isgrpinv  19151  grpidinv  19156  dfgrp3lem  19195  issubg4  19303  isnsg2  19313  nsgacs  19319  elnmz  19320  cycsubgcl  19368  ghmrn  19390  ghmnsgima  19401  isga  19452  orbsta  19474  cntzfval  19481  elcntz  19483  resscntz  19494  oppgsubg  19524  symgextfo  19583  gsmsymgreqlem2  19592  gsmsymgreq  19593  pmtrdifel  19641  pmtrdifwrdellem3  19644  pmtrdifwrdel2  19647  psgnunilem2  19656  psgnunilem3  19657  odeq  19711  gexid  19742  gexlem2  19743  gexdvds  19745  isslw  19769  sylow2alem1  19778  sylow2alem2  19779  efgval  19878  efgrelexlemb  19911  efgcpbllemb  19916  abl1  20027  dmdprd  20161  dprd2da  20205  pgpfac1lem5  20242  isomnd  20284  ring1  20488  rngisomring  20644  rhmval0  20652  lringuplu  20743  rhmimasubrnglem  20764  isrrg  20897  isabv  21015  islss  21156  lssacs  21189  reslmhm  21274  islbs  21298  pj1lmhm  21322  lbsacsbs  21381  rnglidlmcl  21442  rnglidl0  21456  rspprop  21471  prmidl  21568  zringlpir  21720  psgndiflemA  21854  ocvfval  21919  elocv  21921  iunocv  21934  frlmlbs  22050  islindf  22065  islinds2  22066  islindf2  22067  lindfrn  22074  lsslindf  22083  islindf4  22091  opsrval  22302  ply1coe  22563  cply1coe0bi  22567  mat0dimcrng  22732  mdetunilem1  22874  mdetunilem9  22882  matunitlindflem2  22942  cpmat  22974  cpmatel  22976  1elcpmat  22980  m2cpminvid2lem  23019  basgen2  23254  bastop1  23258  isclo  23352  ordtbaslem  23453  iscn  23500  cnpval  23501  iscnp  23502  iscnp3  23509  lmbr  23523  lmbr2  23524  lmbrf  23525  cnprest  23554  cnprest2  23555  t0sep  23589  isreg  23597  t1sep2  23634  tgcmp  23666  1stcclb  23709  1stcfb  23710  2ndc1stc  23716  1stcrest  23718  2ndcdisj  23722  islly  23734  isnlly  23735  lly1stc  23762  isref  23775  islocfin  23783  elkgen  23802  kgencn  23822  elpt  23838  elptr  23839  ptcnplem  23887  tx1stc  23916  cnmpt21  23937  kqt0lem  24002  isr0  24003  regr1lem2  24006  r0sep  24014  nrmr0reg  24015  flffbas  24261  cnflf  24268  cnflf2  24269  lmflf  24271  txflf  24272  fclsopni  24281  fclsnei  24285  fclsrest  24290  fcfnei  24301  cnfcf  24308  alexsubb  24312  alexsubALTlem3  24315  qustgplem  24387  tsmsfbas  24394  tsmsres  24410  tsmsf1o  24411  tsmsxplem1  24419  ustval  24469  isust  24470  ustincl  24474  ustdiag  24475  ustinvel  24476  ustexhalf  24477  ust0  24486  utopval  24498  ucnval  24542  isucn  24543  isucn2  24544  ucnima  24546  iscfilu  24553  ispsmet  24570  ismet  24589  isxmet  24590  imasdsf1olem  24639  imasf1oxmet  24641  imasf1omet  24642  metss  24774  met1stc  24787  prdsxmslem2  24795  txmetcnp  24813  metucn  24837  tngngp3  24922  nlmvscn  24953  nmoval  24981  nmolb  24983  qtopbaslem  25024  cncfval  25156  elcncf2  25158  mulc1cncf  25173  cncfmet  25177  evth  25227  lebnumlem3  25231  lebnum  25232  xlebnum  25233  ishtpy  25240  isphtpy  25249  pi1xfr  25323  pi1coghm  25329  isclmp  25365  ipcn  25514  lmmbr2  25527  lmmbr3  25528  lmmbrf  25530  cfilfval  25532  iscfil  25533  fmcfil  25540  caufval  25543  iscau  25544  iscau2  25545  iscau3  25546  iscau4  25547  iscauf  25548  caucfil  25551  cfilresi  25563  causs  25566  lmclim  25571  cmetcusp1  25621  minveclem4c  25693  minveclem2  25694  minveclem3b  25696  minveclem4  25700  minveclem6  25702  minveclem7  25703  ovolicc2lem3  25787  ismbl  25794  dyadmax  25866  dyadmbllem  25867  dyadmbl  25868  opnmbllem  25869  ismbf1  25892  ismbf  25896  mbfeqalem2  25910  mbflimsup  25934  mbfi1fseqlem6  25988  mbfi1flimlem  25990  itg2seq  26010  itg2monolem1  26018  isibl  26033  ply1divex  26402  fta1g  26435  dgrco  26541  plydivex  26567  fta1  26578  vieta1  26584  aannenlem1  26604  aannenlem2  26605  aalioulem2  26609  aalioulem3  26610  ulmval  26656  ulm2  26661  ulmi  26662  ulmres  26664  ulmshftlem  26665  ulmcaulem  26670  ulmcau  26671  ulmss  26673  ulmbdd  26674  ulmdvlem1  26676  ulmdvlem3  26678  pilem2  26728  pilem3  26729  cxpcn3  27025  dmarea  27234  rlimcnp  27242  scvxcvx  27262  lgamgulmlem2  27306  lgamgulmlem3  27307  lgamgulmlem5  27309  lgambdd  27313  lgamcvglem  27316  isppw2  27391  perfectlem2  27506  2sqlem6  27699  2sqlem10  27704  addsq2reu  27716  2sqreulem1  27722  2sqreunnlem1  27725  dchrisumlema  27764  dchrisumlem2  27766  dchrisumlem3  27767  pntpbnd  27864  pntibndlem3  27868  pntibnd  27869  pntleme  27884  pntlem3  27885  pntlemp  27886  pnt3  27888  ltsval  27923  nosupprefixmo  27976  noinfprefixmo  27977  nosupcbv  27978  nosupno  27979  nosupdm  27980  nosupfv  27982  nosupres  27983  nosupbnd1lem1  27984  nosupbnd1lem3  27986  nosupbnd1lem5  27988  noinfcbv  27993  noinfno  27994  noinfdm  27995  noinffv  27997  noinfres  27998  noinfbnd1lem3  28001  noinfbnd1lem5  28003  noetalem1  28017  noetalem2  28018  nocvxminlem  28059  brslts  28067  sltssnb  28074  conway  28084  etaslts  28098  lesrec  28104  eqcuts3  28109  madebdaylemlrcut  28204  madebday  28205  bdayle  28221  cofcutr  28229  cutmax  28239  cutmin  28240  lrrecfr  28248  addsprop  28281  negsunif  28360  addonbday  28584  onsfi  28661  n0subs  28668  bdayn0p1  28674  bdaypw2n0bndlem  28768  bdayfinbndlem2  28773  z12zsodd  28787  istrkgld  28840  axtg5seg  28846  tgcgr4  28913  perpln1  29104  perpln2  29105  isperp  29106  prlngmo2  29353  brbtwn2  29402  colinearalg  29407  axsegconlem1  29414  axsegcon  29424  ax5seglem4  29429  ax5seglem5  29430  axlowdim  29458  axeuclidlem  29459  axcontlem1  29461  axcontlem2  29462  axcontlem4  29464  axcontlem5  29465  axcontlem8  29468  axcontlem12  29472  elntg2  29482  uvtxusgr  29902  rgrx0ndm  30093  ewlksfval  30101  wksfval  30109  wwlks  30343  wlkiswwlks2  30383  clwwlk  30493  1conngr  30714  frgrwopregasn  30836  frgrwopregbsn  30837  frgrwopreglem5ALT  30842  frgrregord013  30915  isgrpo  31018  isgrpoi  31019  grpoideu  31030  grpoidinv2  31036  vciOLD  31082  isvclem  31098  cnidOLD  31103  isnvlem  31131  nvi  31135  lnoval  31273  islno  31274  isblo3i  31322  blo3i  31323  blocnilem  31325  ajfval  31330  ubthlem1  31391  ubthlem2  31392  ubthlem3  31393  ubth  31394  minvecolem2  31396  minvecolem3  31397  minvecolem4c  31400  minvecolem4  31401  minvecolem5  31402  minvecolem6  31403  minvecolem7  31404  h2hcau  31500  h2hlm  31501  hilid  31682  hcau  31705  hlimi  31709  hlim2  31713  ocel  31802  adjsym  32354  ellnop  32379  ellnfn  32404  hhcno  32425  hhcnf  32426  lnopeq  32530  elunop2  32534  lnophm  32540  lnconi  32554  lnopcnbd  32557  lnfncnbd  32578  imaelshi  32579  riesz3i  32583  riesz4i  32584  riesz4  32585  riesz1  32586  cnlnadjlem2  32589  cnlnadjlem5  32592  cnlnadjlem8  32595  cnlnadji  32597  nmopadjlei  32609  cnvbraval  32631  leopg  32643  leoppos  32647  mdbr  32815  dmdbr  32820  cdj3i  32962  disjunsn  33107  funcnv5mpt  33180  fgreu  33184  fcnvgreu  33185  xrge0infss  33271  wrdt2ind  33435  mgccole1  33470  mgccole2  33471  mgcmnt1  33472  mgcmnt2  33473  gsumhashmul  33547  isfxp  33648  fxpgaeq  33649  inftmrel  33660  isinftm  33661  archiabl  33678  isarchiofld  33679  elrgspnlem4  33725  0nellinds  33845  lindssn  33852  elrspunidl  33897  ismxidl  33906  1arithidom  33988  1arithufdlem3  33997  evl1deg1  34027  evl1deg2  34028  evl1deg3  34029  vietalem  34130  vieta  34131  crefeq  34396  zarcmplem  34432  esum2d  34644  sigaval  34662  issgon  34674  isrnmeas  34752  ismbfm  34803  mbfmcst  34811  elcarsg  34857  sitgval  34884  eulerpartlemd  34918  ballotleme  35049  tgoldbachgt  35212  bnj1185  35343  bnj1385  35382  bnj66  35410  bnj106  35418  bnj155  35429  bnj852  35471  bnj893  35478  bnj1228  35561  bnj1234  35563  bnj1463  35605  nummin  35639  rankfilimbi  35650  r1omhfb  35663  elscott  35665  fineqvnttrclse  35711  r1omhfbregs  35724  gblacfnacd  35800  onvf1odlem4  35804  vonf1wev  35806  vonf1owevOLD  35808  derangenlem  35851  subfacp1lem3  35862  subfacp1lem5  35864  subfacp1lem6  35865  subfacp1  35866  erdszelem8  35878  kur14  35896  cnpconn  35910  resconn  35926  cvmscbv  35938  iscvm  35939  cvmsi  35945  cvmsval  35946  cvmlift3lem2  36000  snmlval  36011  satfv1  36043  fmlasucdisj  36079  satffunlem1lem1  36082  satffunlem2lem1  36084  satfv1fvfmla1  36103  mclsssvlem  36242  mclsval  36243  mclsax  36249  mclsind  36250  dfon2lem9  36469  dfrdg2  36473  dfrdg3  36474  fwddifnval  36844  nmulprop  36855  ltnadd  36883  nn0prpwlem  37026  isfne  37043  isfne4  37044  isfne2  37046  isfne3  37047  neibastop3  37066  topmeet  37068  topjoin  37069  filnetlem4  37085  weiunlem  37167  weiunfrlem  37168  dfttc4lem1  37232  dfttc4  37234  elttcirr  37235  unblimceq0lem  37288  unblimceq0  37289  unbdqndv2  37293  taupilemrplb  38155  fin2so  38444  lindsadd  38450  ptrecube  38452  poimirlem2  38454  poimirlem3  38455  poimirlem4  38456  poimirlem24  38476  poimirlem25  38477  poimirlem26  38478  poimirlem27  38479  poimirlem28  38480  poimirlem29  38481  poimirlem30  38482  poimirlem32  38484  poimir  38485  heicant  38487  mblfinlem1  38489  mblfinlem2  38490  voliunnfl  38496  volsupnfl  38497  mbfresfi  38498  itg2addnc  38506  upixp  38577  indexdom  38582  filbcmb  38588  sdclem2  38590  fdc  38593  lmclim2  38606  caures  38608  istotbnd  38617  istotbnd3  38619  sstotbnd  38623  isbnd  38628  heibor  38669  bfp  38672  rrncmslem  38680  isgrpda  38803  idlval  38861  isidl  38862  0idl  38873  unichnidl  38879  pridl  38885  ismaxidl  38888  smprngopr  38900  igenval2  38914  prnc  38915  ispridlc  38918  scottexf  39014  scott0f  39015  disjsuc2  39260  riotasvd  39927  islfl  40031  eqlkr  40070  eqlkr3  40072  glbconN  40348  hlsuprexch  40352  ispsubsp  40716  ldilset  41080  isldil  41081  dilsetN  41124  isdilN  41125  trlset  41132  trlval  41133  cdleme27b  41339  cdleme29b  41346  cdleme31so  41350  cdleme31sn1  41352  cdleme31sn1c  41359  cdleme31fv  41361  cdleme40v  41440  istendo  41731  cdlemkid3N  41904  cdlemkid4  41905  cdlemkid5  41906  dihfval  42202  dihval  42203  islpolN  42454  hdmapffval  42797  hdmapfval  42798  hdmapval  42799  hdmapval2lem  42802  hgmapffval  42856  hgmapfval  42857  hgmapval  42858  hgmapvs  42862  isprimroot  43057  aks6d1c1p1  43071  hashscontpow1  43085  sticksstones2  43111  unitscyglem3  43161  exfinfldd  43167  qsalrel  43206  supinf  43207  sn-sup2  43477  fsuppind  43534  isnacs  43647  isnacs2  43649  nacsfix  43655  mzpclval  43668  elmzpcl  43669  rencldnfilem  43759  infmrgelbi  43817  pellfundre  43820  pellfundlb  43823  wepwsolem  43981  fnwe2lem2  43990  aomclem8  44000  dfac11  44001  gicabl  44038  islnr3  44054  hbtlem2  44063  hbtlem5  44067  onintunirab  44166  onsucf1lem  44208  cantnfresb  44263  safesnsupfilb  44356  rp-brsslt  44361  fiinfi  44511  clsk1independent  44984  ntrclsk13  45009  gneispacess2  45084  imo72b2lem0  45103  imo72b2lem2  45105  imo72b2lem1  45107  imo72b2  45110  mnuop23d  45188  ismnushort  45223  ralabsobidv  45893  0elaxnul  45904  pwclaxpow  45905  prclaxpr  45906  uniclaxun  45907  omssaxinf2  45909  modelac8prim  45913  wfac8prim  45923  permac8prim  45935  evth2f  45947  evthf  45959  fnchoice  45961  uzwo4  45985  wessf1ornlem  46115  disjinfi  46122  rnmptlb  46170  rnmptbdd  46172  rnmptbd2  46176  rnmptbd  46183  dstregt0  46213  upbdrech2  46239  rexabslelem  46344  rexabsle  46345  uzub  46357  infrpgernmpt  46391  mccl  46526  ellimcabssub0  46545  climf  46550  clim2f  46562  limsupre  46567  clim2cf  46576  clim0cf  46580  climf2  46592  clim2f2  46596  clim2d  46599  limsupref  46611  limsupbnd1f  46612  climinf2  46633  limsuppnf  46637  climinfmpt  46641  climinf3  46642  limsupubuzmpt  46645  limsupmnf  46647  limsupre2lem  46650  limsupre2  46651  limsupmnfuzlem  46652  limsupmnfuz  46653  limsupre2mpt  46656  limsupre3lem  46658  limsupre3  46659  limsupre3mpt  46660  limsupre3uz  46662  limsupreuz  46663  limsupreuzmpt  46665  climuz  46670  liminfreuzlem  46728  liminfreuz  46729  cnrefiisplem  46755  xlimmnfvlem1  46758  xlimmnfv  46760  xlimpnfvlem1  46762  xlimpnfv  46764  xlimmnfmpt  46769  xlimpnfmpt  46770  cncfshift  46800  cncfperiod  46805  fperdvper  46845  dvbdfbdioo  46856  ioodvbdlimc1lem2  46858  ioodvbdlimc2lem  46860  dvnprodlem3  46874  stoweidlem5  46931  stoweidlem9  46935  stoweidlem15  46941  stoweidlem16  46942  stoweidlem27  46953  stoweidlem28  46954  stoweidlem31  46957  stoweidlem34  46960  stoweidlem37  46963  stoweidlem46  46972  stoweidlem48  46974  stoweidlem51  46977  stoweidlem52  46978  stoweidlem59  46985  wallispilem3  46993  stirlinglem13  47012  fourierdlem2  47035  fourierdlem3  47036  fourierdlem16  47049  fourierdlem20  47053  fourierdlem21  47054  fourierdlem22  47055  fourierdlem25  47058  fourierdlem39  47072  fourierdlem42  47075  fourierdlem54  47086  fourierdlem64  47096  fourierdlem77  47109  fourierdlem83  47115  fourierdlem103  47135  fourierdlem104  47136  subsaliuncllem  47283  iundjiun  47386  meaiunincf  47409  caragenval  47419  isome  47420  caragenel  47421  omessle  47424  ovnlerp  47488  hoidmvlelem3  47523  hoidmvle  47526  issmflem  47653  issmfgt  47682  smfmullem2  47718  smfmullem4  47720  smfmul  47721  smfsuplem2  47738  smfsup  47740  smfinflem  47743  smfinf  47744  fsupdm  47768  finfdm  47772  cfsetsnfsetf  48044  cbvral2  48089  2reu8i  48099  2reuimp0  48100  dfdfat2  48114  iccpart  48414  iccpartigtl  48421  paireqne  48509  reupr  48520  perfectALTVlem2  48736  bgoldbachlt  48827  tgoldbachlt  48830  grimidvtxedg  48899  grimcnv  48902  grimco  48903  isuspgrim0  48908  gricushgr  48931  ushggricedg  48941  uhgrimisgrgric  48945  isubgr3stgr  48989  isgrlim  48996  isgrlim2  48997  uspgrlim  49006  grlicsym  49027  grlictr  49029  gpg5nbgrvtx03star  49094  gpg5nbgr3star  49095  pgnbgreunbgr  49139  upwlksfval  49149  nn0mnd  49192  uzlidlring  49248  smprngprmrng  49352  ply1mulgsumlem1  49414  ply1mulgsumlem2  49415  linindslinci  49476  lindslinindsimp1  49485  lindslinindsimp2lem5  49490  lindslinindsimp2  49491  linds0  49493  lindsrng01  49496  snlindsntor  49499  lmod1  49520  ldepsnlinc  49536  bigoval  49577  elbigo2r  49581  nn0sumshdiglem2  49650  eenglngeehlnmlem1  49765  eenglngeehlnmlem2  49766  lubeldm2d  49982  glbeldm2d  49983  lubsscl  49984  glbsscl  49985  ipolubdm  50011  ipolub  50012  ipoglbdm  50014  ipoglb  50015  nelsubc3lem  50094  upfval2  50201  upfval3  50202  isthincd2lem2  50459  setc1onsubc  50626  cnelsubclem  50627