Theorem ralbidv 3189

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

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

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 1945

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

This theorem is used by:  2ralbidv  3230  rexralbidv  3232  3ralbidv  3233  4ralbidv  3234  cbvral2vw  3248  cbvral4vw  3251  cbvral2v  3357  rspceaimv  3586  rspc2  3588  rspc2v  3590  rspc3v  3595  rspc4v  3599  reu6i  3689  reu7  3693  sbcralt  3823  reu8nf  3828  raaan  4477  raaanv  4478  raaan2  4481  2reu4lem  4482  reusngf  4635  2ralsng  4639  rexreusng  4640  reuprg0  4663  issn  4790  2ralunsn  4829  elintg  4918  elintrabg  4924  eliin  4959  disjprg  5102  disjxun  5104  brralrspcev  5168  reusv2lem2  5365  reusv3  5371  poeq1  5566  solin  5590  somo  5602  frirr  5631  fr2nr  5632  frminex  5634  wereu2  5652  posn  5742  frsn  5744  ralxpf  5829  cnvpo  6305  reu3op  6310  reuop  6311  dfpo2  6314  frpomin  6358  fnmptfvd  7060  iinpreima  7090  dff4  7122  dff13f  7279  fpropnf1  7291  f1ounsn  7300  eusvobj2  7432  ovanraleqv  7464  f1opr  7496  ofreq  7718  sorpssuni  7769  sorpssint  7770  fr3nr  7807  onssmin  7827  funcnvuni  7965  f1oweALT  8005  frxp  8162  fnwe2lem3  8171  frxp2  8185  xpord2indlem  8188  frxp3  8192  xpord3inddlem  8195  poseq  8199  soseq  8200  frecseq123  8325  csbfrecsg  8327  frrlem1  8329  frrlem13  8341  smoeq  8383  tfrlem12  8422  tz7.48lemOLD  8476  naddcllem  8710  naddov2  8713  naddunif  8728  naddasslem1  8729  naddasslem2  8730  elixp2  8954  undifixp  8987  xpf1o  9183  nneneq  9246  ac6sfi  9300  frfi  9301  fipreima  9372  indexfi  9374  marypha1lem  9449  marypha1  9450  supeq1  9461  supeq3  9465  supmo  9468  eqsup  9472  supub  9475  suplub  9476  sup0  9483  supisoex  9491  eqinf  9501  infval  9503  infmo  9513  oieq1  9530  ordtypecbv  9535  ordtypelem3  9538  ordtypelem6  9541  ordtypelem7  9542  ordtypelem9  9544  wemaplem1  9564  wemaplem2  9565  zfregcl  9612  zfregclOLD  9613  oemapval  9708  oemapvali  9709  cantnf  9718  wemapwe  9722  ttrcleq  9734  ttrcltr  9741  ttrclss  9745  ttrclselem2  9751  rankval3b  9860  unbndrank  9879  rankunb  9888  rankuni2b  9891  tcrank  9925  rankfilimbi  9926  scottex  9957  scottexOLD  9958  scottexsOLD  9967  scott0bsOLD  9969  scottelrankd  9972  bnd2  9980  setrec1lem2  9991  updjud  10039  dfac8clem  10135  ac5num  10139  acni  10148  acni2  10149  alephval3  10213  dfac4  10225  dfac5lem5  10230  dfac5  10231  dfac2a  10232  dfac2b  10233  dfacacn  10244  kmlem2  10254  kmlem13  10265  cflem  10347  cflecard  10354  cfeq0  10358  cfsuc  10359  cfflb  10361  cofsmo  10371  cfsmolem  10372  cfcoflem  10374  coftr  10375  alephsing  10378  fin23lem11  10419  isfin3ds  10431  fin23lem17  10440  fin23lem39  10452  isf33lem  10468  isf34lem6  10482  fin1a2lem13  10514  hsmexlem4  10531  hsmex  10534  axcc2lem  10538  axcc3  10540  dcomex  10549  axdc2lem  10550  axdc3lem2  10553  axdc3lem3  10554  axdc3  10556  axdc4lem  10557  axcclem  10559  zorn2lem2  10599  zorn2lem7  10604  zorn2g  10605  zornn0g  10607  ttukeylem7  10617  axdclem2  10622  brdom3  10631  brdom7disj  10634  brdom6disj  10635  alephval2  10681  inar1  10884  axgroth6  10937  pinq  11036  nqereu  11038  prlem934  11142  supexpr  11163  supsrlem  11220  axpre-sup  11278  dedekind  11497  dedekindle  11498  fiminre2  12289  lbreu  12291  sup2  12297  infm3  12300  nnsub  12406  uzwo  13062  nnwof  13065  ublbneg  13084  lbzbi  13087  zsupss  13088  uzsupss  13091  uzwo3  13094  zmax  13096  rpnnen1lem1  13130  rpnnen1lem3  13131  rpnnen1lem4  13132  rpnnen1lem5  13133  xrsupsslem  13461  xrinfmsslem  13462  xrsupss  13463  xrinfmss  13464  flval2  13978  axdc4uzlem  14150  ssnn0fi  14152  fsuppmapnn0fiubex  14159  faclbnd4lem4  14464  bccl  14490  hashgt12el  14591  hashbc  14622  hashge2el2dif  14649  wrdind  14896  wrd2ind  14897  rexanre  15540  rexico  15547  cau4  15550  reusq0  15658  clim  15687  rlim  15688  rlim2  15689  clim2  15697  clim2c  15698  clim0c  15700  rlim0  15701  rlim0lt  15702  ello12r  15710  ello1d  15716  elo12r  15721  rlimresb  15758  rlimcld2  15771  climabs0  15778  rlimo1  15810  lo1add  15820  lo1mul  15821  isercoll  15861  incexclem  16031  sqrt2irr  16443  gcdcllem1  16695  gcdcllem2  16696  dfgcd2  16745  fissn0dvds  16820  dvdslcmf  16832  lcmfledvds  16833  lcmf  16834  lcmfunsnlem1  16838  lcmfunsnlem2lem1  16839  lcmfunsnlem  16842  lcmfdvds  16843  reumodprminv  17008  pc2dvds  17083  pcz  17085  prmpwdvds  17108  infpn2  17117  prmreclem2  17121  prmreclem3  17122  prmreclem5  17124  prmreclem6  17125  vdwlem6  17190  vdwlem8  17192  vdwlem13  17197  vdwnnlem1  17199  vdwnn  17202  ramcl  17233  cshwrepswhash1  17306  prdsleval  17674  imasval  17709  imasaddfnlem  17726  imasvscafn  17735  mrisval  17830  isacs  17851  isacs2  17853  isacs1i  17857  mreacs  17858  acsfn  17859  acsfn2  17863  iscatd  17873  catidex  17874  catideu  17875  cidval  17877  catidd  17880  comfeq  17906  catpropd  17909  ismon  17934  isfunc  18065  isnat  18151  isinito  18197  istermo  18198  isprs  18496  drsdirfi  18505  ispos  18514  lubfval  18548  lubeldm  18551  lubval  18554  lubprop  18556  lublecllem  18558  glbfval  18561  glbeldm  18564  glbval  18567  glbprop  18569  joinval2lem  18578  joinlem  18581  meetval2lem  18592  meetlem  18595  poslubmo  18609  posglbmo  18610  poslubd  18611  resspos  18629  isglbd  18709  lubl  18712  lubun  18715  clatleglb  18718  isdlat  18722  ipodrsima  18741  chneq1  18812  mgm1  18862  idressid  18888  gsumval2  18901  mgmhmima  18930  sgrp1  18944  mhmimalem  19046  mndind  19050  gsumwspan  19068  efmndmnd  19111  smndex1mnd  19135  sgrp2rid2  19151  sgrp2rid2ex  19152  sgrp2nmndlem4  19153  degenmgm  19163  degenmgm2  19166  pwmnd  19169  dfgrp2  19199  isgrpinv  19230  grpidinv  19235  dfgrp3lem  19274  issubg4  19382  isnsg2  19392  nsgacs  19398  elnmz  19399  cycsubgcl  19447  ghmrn  19469  ghmnsgima  19480  isga  19532  orbsta  19554  cntzfval  19561  elcntz  19563  resscntz  19574  oppgsubg  19604  symgextfo  19663  gsmsymgreqlem2  19672  gsmsymgreq  19673  pmtrdifel  19721  pmtrdifwrdellem3  19724  pmtrdifwrdel2  19727  psgnunilem2  19736  psgnunilem3  19737  odeq  19791  gexid  19822  gexlem2  19823  gexdvds  19825  isslw  19849  sylow2alem1  19858  sylow2alem2  19859  efgval  19958  efgrelexlemb  19991  efgcpbllemb  19996  abl1  20107  dmdprd  20241  dprd2da  20285  pgpfac1lem5  20322  isomnd  20364  ring1  20568  rngisomring  20724  rhmval0  20732  lringuplu  20823  rhmimasubrnglem  20844  isrrg  20977  isabv  21095  islss  21236  lssacs  21269  reslmhm  21354  islbs  21378  pj1lmhm  21402  lbsacsbs  21461  rnglidlmcl  21522  rnglidl0  21536  rspprop  21551  prmidl  21648  zringlpir  21800  psgndiflemA  21934  ocvfval  21999  elocv  22001  iunocv  22014  frlmlbs  22130  islindf  22145  islinds2  22146  islindf2  22147  lindfrn  22154  lsslindf  22163  islindf4  22171  opsrval  22382  ply1coe  22643  cply1coe0bi  22647  mat0dimcrng  22812  mdetunilem1  22954  mdetunilem9  22962  matunitlindflem2  23022  cpmat  23054  cpmatel  23056  1elcpmat  23060  m2cpminvid2lem  23099  basgen2  23334  bastop1  23338  isclo  23432  ordtbaslem  23533  iscn  23580  cnpval  23581  iscnp  23582  iscnp3  23589  lmbr  23603  lmbr2  23604  lmbrf  23605  cnprest  23634  cnprest2  23635  t0sep  23669  isreg  23677  t1sep2  23714  tgcmp  23746  1stcclb  23789  1stcfb  23790  2ndc1stc  23796  1stcrest  23798  2ndcdisj  23802  islly  23814  isnlly  23815  lly1stc  23842  isref  23855  islocfin  23863  elkgen  23882  kgencn  23902  elpt  23918  elptr  23919  ptcnplem  23967  tx1stc  23996  cnmpt21  24017  kqt0lem  24082  isr0  24083  regr1lem2  24086  r0sep  24094  nrmr0reg  24095  flffbas  24341  cnflf  24348  cnflf2  24349  lmflf  24351  txflf  24352  fclsopni  24361  fclsnei  24365  fclsrest  24370  fcfnei  24381  cnfcf  24388  alexsubb  24392  alexsubALTlem3  24395  qustgplem  24467  tsmsfbas  24474  tsmsres  24490  tsmsf1o  24491  tsmsxplem1  24499  ustval  24549  isust  24550  ustincl  24554  ustdiag  24555  ustinvel  24556  ustexhalf  24557  ust0  24566  utopval  24578  ucnval  24622  isucn  24623  isucn2  24624  ucnima  24626  iscfilu  24633  ispsmet  24650  ismet  24669  isxmet  24670  imasdsf1olem  24719  imasf1oxmet  24721  imasf1omet  24722  metss  24854  met1stc  24867  prdsxmslem2  24875  txmetcnp  24893  metucn  24917  tngngp3  25002  nlmvscn  25033  nmoval  25061  nmolb  25063  qtopbaslem  25104  cncfval  25236  elcncf2  25238  mulc1cncf  25253  cncfmet  25257  evth  25307  lebnumlem3  25311  lebnum  25312  xlebnum  25313  ishtpy  25320  isphtpy  25329  pi1xfr  25403  pi1coghm  25409  isclmp  25445  ipcn  25594  lmmbr2  25607  lmmbr3  25608  lmmbrf  25610  cfilfval  25612  iscfil  25613  fmcfil  25620  caufval  25623  iscau  25624  iscau2  25625  iscau3  25626  iscau4  25627  iscauf  25628  caucfil  25631  cfilresi  25643  causs  25646  lmclim  25651  cmetcusp1  25701  minveclem4c  25773  minveclem2  25774  minveclem3b  25776  minveclem4  25780  minveclem6  25782  minveclem7  25783  ovolicc2lem3  25867  ismbl  25874  dyadmax  25946  dyadmbllem  25947  dyadmbl  25948  opnmbllem  25949  ismbf1  25972  ismbf  25976  mbfeqalem2  25990  mbflimsup  26014  mbfi1fseqlem6  26068  mbfi1flimlem  26070  itg2seq  26090  itg2monolem1  26098  isibl  26113  ply1divex  26482  fta1g  26515  dgrco  26621  plydivex  26645  fta1  26656  vieta1  26662  aannenlem1  26682  aannenlem2  26683  aalioulem2  26687  aalioulem3  26688  ulmval  26734  ulm2  26739  ulmi  26740  ulmres  26742  ulmshftlem  26743  ulmcaulem  26748  ulmcau  26749  ulmss  26751  ulmbdd  26752  ulmdvlem1  26754  ulmdvlem3  26756  pilem2  26806  pilem3  26807  cxpcn3  27103  dmarea  27312  rlimcnp  27320  scvxcvx  27340  lgamgulmlem2  27384  lgamgulmlem3  27385  lgamgulmlem5  27387  lgambdd  27391  lgamcvglem  27394  isppw2  27469  perfectlem2  27584  2sqlem6  27777  2sqlem10  27782  addsq2reu  27794  2sqreulem1  27800  2sqreunnlem1  27803  dchrisumlema  27842  dchrisumlem2  27844  dchrisumlem3  27845  pntpbnd  27942  pntibndlem3  27946  pntibnd  27947  pntleme  27962  pntlem3  27963  pntlemp  27964  pnt3  27966  fltoprm  28022  ltsval  28031  nosupprefixmo  28084  noinfprefixmo  28085  nosupcbv  28086  nosupno  28087  nosupdm  28088  nosupfv  28090  nosupres  28091  nosupbnd1lem1  28092  nosupbnd1lem3  28094  nosupbnd1lem5  28096  noinfcbv  28101  noinfno  28102  noinfdm  28103  noinffv  28105  noinfres  28106  noinfbnd1lem3  28109  noinfbnd1lem5  28111  noetalem1  28125  noetalem2  28126  nocvxminlem  28167  brslts  28175  sltssnb  28182  conway  28192  etaslts  28206  lesrec  28212  eqcuts3  28217  madebdaylemlrcut  28312  madebday  28313  bdayle  28329  cofcutr  28337  cutmax  28347  cutmin  28348  lrrecfr  28356  addsprop  28389  negsunif  28468  addonbday  28692  onsfi  28769  n0subs  28776  bdayn0p1  28782  bdaypw2n0bndlem  28876  bdayfinbndlem2  28881  z12zsodd  28895  istrkgld  28948  axtg5seg  28954  tgcgr4  29021  perpln1  29212  perpln2  29213  isperp  29214  prlngmo2  29461  brbtwn2  29510  colinearalg  29515  axsegconlem1  29522  axsegcon  29532  ax5seglem4  29537  ax5seglem5  29538  axlowdim  29566  axeuclidlem  29567  axcontlem1  29569  axcontlem2  29570  axcontlem4  29572  axcontlem5  29573  axcontlem8  29576  axcontlem12  29580  elntg2  29590  uvtxusgr  30010  rgrx0ndm  30201  ewlksfval  30209  wksfval  30217  wwlks  30451  wlkiswwlks2  30491  clwwlk  30601  1conngr  30822  frgrwopregasn  30944  frgrwopregbsn  30945  frgrwopreglem5ALT  30950  frgrregord013  31023  isgrpo  31126  isgrpoi  31127  grpoideu  31138  grpoidinv2  31144  vciOLD  31190  isvclem  31206  cnidOLD  31211  isnvlem  31239  nvi  31243  lnoval  31381  islno  31382  isblo3i  31430  blo3i  31431  blocnilem  31433  ajfval  31438  ubthlem1  31499  ubthlem2  31500  ubthlem3  31501  ubth  31502  minvecolem2  31504  minvecolem3  31505  minvecolem4c  31508  minvecolem4  31509  minvecolem5  31510  minvecolem6  31511  minvecolem7  31512  h2hcau  31608  h2hlm  31609  hilid  31790  hcau  31813  hlimi  31817  hlim2  31821  ocel  31910  adjsym  32462  ellnop  32487  ellnfn  32512  hhcno  32533  hhcnf  32534  lnopeq  32638  elunop2  32642  lnophm  32648  lnconi  32662  lnopcnbd  32665  lnfncnbd  32686  imaelshi  32687  riesz3i  32691  riesz4i  32692  riesz4  32693  riesz1  32694  cnlnadjlem2  32697  cnlnadjlem5  32700  cnlnadjlem8  32703  cnlnadji  32705  nmopadjlei  32717  cnvbraval  32739  leopg  32751  leoppos  32755  mdbr  32923  dmdbr  32928  cdj3i  33070  disjunsn  33257  funcnv5mpt  33330  fgreu  33334  fcnvgreu  33335  xrge0infss  33419  wrdt2ind  33583  mgccole1  33618  mgccole2  33619  mgcmnt1  33620  mgcmnt2  33621  gsumhashmul  33695  isfxp  33796  fxpgaeq  33797  inftmrel  33808  isinftm  33809  archiabl  33826  isarchiofld  33827  elrgspnlem4  33873  0nellinds  33993  lindssn  34000  elrspunidl  34045  ismxidl  34054  1arithidom  34136  1arithufdlem3  34145  evl1deg1  34175  evl1deg2  34176  evl1deg3  34177  vietalem  34278  vieta  34279  crefeq  34544  zarcmplem  34580  esum2d  34792  sigaval  34810  issgon  34822  isrnmeas  34900  ismbfm  34951  mbfmcst  34958  elcarsg  35004  sitgval  35031  eulerpartlemd  35065  ballotleme  35196  tgoldbachgt  35359  bnj1185  35490  bnj1385  35529  bnj66  35557  bnj106  35565  bnj155  35576  bnj852  35618  bnj893  35625  bnj1228  35708  bnj1234  35710  bnj1463  35752  nummin  35803  r1omhfb  35819  rankse  35822  elscott  35824  fineqvnttrclse  35891  r1omhfbregs  35904  gblacfnacd  36028  onvf1odlem4  36033  vonf1wev  36035  vonf1owevOLD  36037  srepdf  36086  derangenlem  36102  subfacp1lem3  36113  subfacp1lem5  36115  subfacp1lem6  36116  subfacp1  36117  erdszelem8  36129  kur14  36147  cnpconn  36161  resconn  36177  cvmscbv  36189  iscvm  36190  cvmsi  36196  cvmsval  36197  cvmlift3lem2  36251  snmlval  36262  satfv1  36294  fmlasucdisj  36330  satffunlem1lem1  36333  satffunlem2lem1  36335  satfv1fvfmla1  36354  mclsssvlem  36493  mclsval  36494  mclsax  36500  mclsind  36501  mirimanoffr  36626  dfon2lem9  36730  dfrdg2  36734  dfrdg3  36735  fwddifnval  37105  nmulprop  37116  ltnadd  37144  nn0prpwlem  37287  isfne  37304  isfne4  37305  isfne2  37307  isfne3  37308  neibastop3  37327  topmeet  37329  topjoin  37330  filnetlem4  37346  weiunlem  37428  weiunfrlem  37429  dfttc4lem1  37493  dfttc4  37495  elttcirr  37496  unblimceq0lem  37549  unblimceq0  37550  unbdqndv2  37554  taupilemrplb  38432  fin2so  38721  lindsadd  38727  ptrecube  38729  poimirlem2  38731  poimirlem3  38732  poimirlem4  38733  poimirlem24  38753  poimirlem25  38754  poimirlem26  38755  poimirlem27  38756  poimirlem28  38757  poimirlem29  38758  poimirlem30  38759  poimirlem32  38761  poimir  38762  heicant  38764  mblfinlem1  38766  mblfinlem2  38767  voliunnfl  38773  volsupnfl  38774  mbfresfi  38775  itg2addnc  38783  upixp  38854  indexdom  38859  filbcmb  38865  sdclem2  38867  fdc  38870  lmclim2  38883  caures  38885  istotbnd  38894  istotbnd3  38896  sstotbnd  38900  isbnd  38905  heibor  38946  bfp  38949  rrncmslem  38957  isgrpda  39080  idlval  39138  isidl  39139  0idl  39150  unichnidl  39156  pridl  39162  ismaxidl  39165  smprngopr  39177  igenval2  39191  prnc  39192  ispridlc  39195  scottexf  39291  scott0f  39292  disjsuc2  39537  riotasvd  40204  islfl  40308  eqlkr  40347  eqlkr3  40349  glbconN  40625  hlsuprexch  40629  ispsubsp  40993  ldilset  41357  isldil  41358  dilsetN  41401  isdilN  41402  trlset  41409  trlval  41410  cdleme27b  41616  cdleme29b  41623  cdleme31so  41627  cdleme31sn1  41629  cdleme31sn1c  41636  cdleme31fv  41638  cdleme40v  41717  istendo  42008  cdlemkid3N  42181  cdlemkid4  42182  cdlemkid5  42183  dihfval  42479  dihval  42480  islpolN  42731  hdmapffval  43074  hdmapfval  43075  hdmapval  43076  hdmapval2lem  43079  hgmapffval  43133  hgmapfval  43134  hgmapval  43135  hgmapvs  43139  isprimroot  43334  aks6d1c1p1  43348  hashscontpow1  43362  sticksstones2  43388  unitscyglem3  43438  exfinfldd  43444  qsalrel  43483  supinf  43484  sn-sup2  43746  fsuppind  43809  isnacs  43906  isnacs2  43908  nacsfix  43914  mzpclval  43927  elmzpcl  43928  rencldnfilem  44018  infmrgelbi  44076  pellfundre  44079  pellfundlb  44082  wepwsolem  44240  aomclem8  44254  dfac11  44255  gicabl  44292  islnr3  44307  hbtlem2  44316  hbtlem5  44320  onintunirab  44419  onsucf1lem  44461  cantnfresb  44516  safesnsupfilb  44609  rp-brsslt  44614  fiinfi  44764  clsk1independent  45236  ntrclsk13  45261  gneispacess2  45336  imo72b2lem0  45355  imo72b2lem2  45357  imo72b2lem1  45359  imo72b2  45362  mnuop23d  45440  ismnushort  45475  ralabsobidv  46155  0elaxnul  46166  pwclaxpow  46167  prclaxpr  46168  uniclaxun  46169  omssaxinf2  46171  modelac8prim  46175  wfac8prim  46185  permac8prim  46197  evth2f  46235  evthf  46247  fnchoice  46249  uzwo4  46273  wessf1ornlem  46403  disjinfi  46410  rnmptlb  46458  rnmptbdd  46460  rnmptbd2  46464  rnmptbd  46471  dstregt0  46501  upbdrech2  46527  rexabslelem  46631  rexabsle  46632  uzub  46644  infrpgernmpt  46678  mccl  46813  ellimcabssub0  46832  climf  46837  clim2f  46849  limsupre  46854  clim2cf  46863  clim0cf  46867  climf2  46879  clim2f2  46883  clim2d  46886  limsupref  46898  limsupbnd1f  46899  climinf2  46920  limsuppnf  46924  climinfmpt  46928  climinf3  46929  limsupubuzmpt  46932  limsupmnf  46934  limsupre2lem  46937  limsupre2  46938  limsupmnfuzlem  46939  limsupmnfuz  46940  limsupre2mpt  46943  limsupre3lem  46945  limsupre3  46946  limsupre3mpt  46947  limsupre3uz  46949  limsupreuz  46950  limsupreuzmpt  46952  climuz  46957  liminfreuzlem  47015  liminfreuz  47016  cnrefiisplem  47042  xlimmnfvlem1  47045  xlimmnfv  47047  xlimpnfvlem1  47049  xlimpnfv  47051  xlimmnfmpt  47056  xlimpnfmpt  47057  cncfshift  47087  cncfperiod  47092  fperdvper  47132  dvbdfbdioo  47143  ioodvbdlimc1lem2  47145  ioodvbdlimc2lem  47147  dvnprodlem3  47161  stoweidlem5  47218  stoweidlem9  47222  stoweidlem15  47228  stoweidlem16  47229  stoweidlem27  47240  stoweidlem28  47241  stoweidlem31  47244  stoweidlem34  47247  stoweidlem37  47250  stoweidlem46  47259  stoweidlem48  47261  stoweidlem51  47264  stoweidlem52  47265  stoweidlem59  47272  wallispilem3  47280  stirlinglem13  47299  fourierdlem2  47322  fourierdlem3  47323  fourierdlem16  47336  fourierdlem20  47340  fourierdlem21  47341  fourierdlem22  47342  fourierdlem25  47345  fourierdlem39  47359  fourierdlem42  47362  fourierdlem54  47373  fourierdlem64  47383  fourierdlem77  47396  fourierdlem83  47402  fourierdlem103  47422  fourierdlem104  47423  subsaliuncllem  47570  iundjiun  47673  meaiunincf  47696  caragenval  47706  isome  47707  caragenel  47708  omessle  47711  ovnlerp  47775  hoidmvlelem3  47810  hoidmvle  47813  issmflem  47940  issmfgt  47969  smfmullem2  48005  smfmullem4  48007  smfmul  48008  smfsuplem2  48025  smfsup  48027  smfinflem  48030  smfinf  48031  fsupdm  48055  finfdm  48059  cfsetsnfsetf  48331  cbvral2  48377  2reu8i  48387  2reuimp0  48388  dfdfat2  48401  iccpart  48701  iccpartigtl  48708  paireqne  48796  reupr  48807  perfectALTVlem2  49023  bgoldbachlt  49114  tgoldbachlt  49117  grimidvtxedg  49186  grimcnv  49189  grimco  49190  isuspgrim0  49195  gricushgr  49218  ushggricedg  49228  uhgrimisgrgric  49232  isubgr3stgr  49276  isgrlim  49283  isgrlim2  49284  uspgrlim  49293  grlicsym  49314  grlictr  49316  gpg5nbgrvtx03star  49381  gpg5nbgr3star  49382  pgnbgreunbgr  49426  upwlksfval  49436  nn0mnd  49479  uzlidlring  49535  smprngprmrng  49639  ply1mulgsumlem1  49701  ply1mulgsumlem2  49702  linindslinci  49763  lindslinindsimp1  49772  lindslinindsimp2lem5  49777  lindslinindsimp2  49778  linds0  49780  lindsrng01  49783  snlindsntor  49786  lmod1  49807  ldepsnlinc  49823  bigoval  49864  elbigo2r  49868  nn0sumshdiglem2  49937  eenglngeehlnmlem1  50053  eenglngeehlnmlem2  50054  lubeldm2d  50275  glbeldm2d  50276  lubsscl  50277  glbsscl  50278  ipolubdm  50304  ipolub  50305  ipoglbdm  50307  ipoglb  50308  nelsubc3lem  50387  upfval2  50496  upfval3  50497  isthincd2lem2  50773  setc1onsubc  50943  cnelsubcw  50944