Theorem ralbidv 3187

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

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

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 3079

This theorem is used by:  2ralbidv  3228  rexralbidv  3230  3ralbidv  3231  4ralbidv  3232  cbvral2vw  3246  cbvral4vw  3249  cbvral2v  3355  rspceaimv  3585  rspc2  3588  rspc2v  3590  rspc3v  3595  rspc4v  3599  reu6i  3689  reu7  3693  sbcralt  3822  reu8nf  3827  raaan  4477  raaanv  4478  raaan2  4481  2reu4lem  4482  reusngf  4638  2ralsng  4642  rexreusng  4643  reuprg0  4666  issn  4795  2ralunsn  4858  elintg  4918  elintrabg  4924  eliin  4959  disjprg  5103  disjxun  5105  brralrspcev  5169  reusv2lem2  5368  reusv3  5374  poeq1  5570  solin  5594  somo  5606  frirr  5635  fr2nr  5636  frminex  5638  wereu2  5656  posn  5745  frsn  5747  ralxpf  5830  cnvpo  6289  reu3op  6294  reuop  6295  dfpo2  6298  frpomin  6342  fnmptfvd  7037  iinpreima  7065  dff4  7097  dff13f  7255  fpropnf1  7267  f1ounsn  7276  eusvobj2  7408  ovanraleqv  7440  f1opr  7472  ofreq  7685  sorpssuni  7736  sorpssint  7737  fr3nr  7774  onssmin  7794  funcnvuni  7932  f1oweALT  7972  frxp  8127  frxp2  8145  xpord2indlem  8148  frxp3  8152  xpord3inddlem  8155  poseq  8159  soseq  8160  frecseq123  8284  csbfrecsg  8286  frrlem1  8288  frrlem13  8300  smoeq  8342  tfrlem12  8381  tz7.48lem  8433  naddcllem  8667  naddov2  8670  naddunif  8685  naddasslem1  8686  naddasslem2  8687  elixp2  8911  undifixp  8944  xpf1o  9140  nneneq  9203  ac6sfi  9257  frfi  9258  fipreima  9328  indexfi  9330  marypha1lem  9406  marypha1  9407  supeq1  9418  supeq3  9422  supmo  9425  eqsup  9429  supub  9432  suplub  9433  sup0  9440  supisoex  9448  eqinf  9458  infval  9460  infmo  9470  oieq1  9487  ordtypecbv  9492  ordtypelem3  9495  ordtypelem6  9498  ordtypelem7  9499  ordtypelem9  9501  wemaplem1  9521  wemaplem2  9522  zfregcl  9569  zfregclOLD  9570  oemapval  9665  oemapvali  9666  cantnf  9675  wemapwe  9679  ttrcleq  9691  ttrcltr  9698  ttrclss  9702  ttrclselem2  9708  rankval3b  9811  unbndrank  9827  rankunb  9835  rankuni2b  9838  tcrank  9869  scottex  9875  scottexOLD  9876  scottexsOLD  9885  scott0bsOLD  9887  scottelrankd  9890  bnd2  9898  updjud  9942  dfac8clem  10038  ac5num  10042  acni  10051  acni2  10052  alephval3  10116  dfac4  10128  dfac5lem5  10133  dfac5  10134  dfac2a  10135  dfac2b  10136  dfacacn  10147  kmlem2  10157  kmlem13  10168  cflem  10250  cflecard  10257  cfeq0  10261  cfsuc  10262  cfflb  10264  cofsmo  10274  cfsmolem  10275  cfcoflem  10277  coftr  10278  alephsing  10281  fin23lem11  10322  isfin3ds  10334  fin23lem17  10343  fin23lem39  10355  isf33lem  10371  isf34lem6  10385  fin1a2lem13  10417  hsmexlem4  10434  hsmex  10437  axcc2lem  10441  axcc3  10443  dcomex  10452  axdc2lem  10453  axdc3lem2  10456  axdc3lem3  10457  axdc3  10459  axdc4lem  10460  axcclem  10462  zorn2lem2  10502  zorn2lem7  10507  zorn2g  10508  zornn0g  10510  ttukeylem7  10520  axdclem2  10525  brdom3  10534  brdom7disj  10537  brdom6disj  10538  alephval2  10584  inar1  10787  axgroth6  10840  pinq  10939  nqereu  10941  prlem934  11045  supexpr  11066  supsrlem  11123  axpre-sup  11181  dedekind  11400  dedekindle  11401  fiminre2  12190  lbreu  12192  sup2  12198  infm3  12201  nnsub  12307  uzwo  12963  nnwof  12966  ublbneg  12985  lbzbi  12988  zsupss  12989  uzsupss  12992  uzwo3  12995  zmax  12997  rpnnen1lem1  13030  rpnnen1lem3  13031  rpnnen1lem4  13032  rpnnen1lem5  13033  xrsupsslem  13361  xrinfmsslem  13362  xrsupss  13363  xrinfmss  13364  flval2  13877  axdc4uzlem  14049  ssnn0fi  14051  fsuppmapnn0fiubex  14058  faclbnd4lem4  14362  bccl  14388  hashgt12el  14489  hashbc  14520  hashge2el2dif  14547  wrdind  14793  wrd2ind  14794  rexanre  15436  rexico  15443  cau4  15446  reusq0  15554  clim  15583  rlim  15584  rlim2  15585  clim2  15593  clim2c  15594  clim0c  15596  rlim0  15597  rlim0lt  15598  ello12r  15606  ello1d  15612  elo12r  15617  rlimresb  15654  rlimcld2  15667  climabs0  15674  rlimo1  15706  lo1add  15716  lo1mul  15717  isercoll  15757  incexclem  15927  sqrt2irr  16341  gcdcllem1  16593  gcdcllem2  16594  dfgcd2  16640  fissn0dvds  16713  dvdslcmf  16725  lcmfledvds  16726  lcmf  16727  lcmfunsnlem1  16731  lcmfunsnlem2lem1  16732  lcmfunsnlem  16735  lcmfdvds  16736  reumodprminv  16900  pc2dvds  16975  pcz  16977  prmpwdvds  17000  infpn2  17009  prmreclem2  17013  prmreclem3  17014  prmreclem5  17016  prmreclem6  17017  vdwlem6  17082  vdwlem8  17084  vdwlem13  17089  vdwnnlem1  17091  vdwnn  17094  ramcl  17125  cshwrepswhash1  17198  prdsleval  17566  imasval  17601  imasaddfnlem  17618  imasvscafn  17627  mrisval  17722  isacs  17743  isacs2  17745  isacs1i  17749  mreacs  17750  acsfn  17751  acsfn2  17755  iscatd  17765  catidex  17766  catideu  17767  cidval  17769  catidd  17772  comfeq  17798  catpropd  17801  ismon  17826  isfunc  17957  isnat  18043  isinito  18089  istermo  18090  isprs  18388  drsdirfi  18397  ispos  18406  lubfval  18440  lubeldm  18443  lubval  18446  lubprop  18448  lublecllem  18450  glbfval  18453  glbeldm  18456  glbval  18459  glbprop  18461  joinval2lem  18470  joinlem  18473  meetval2lem  18484  meetlem  18487  poslubmo  18501  posglbmo  18502  poslubd  18503  resspos  18521  isglbd  18601  lubl  18604  lubun  18607  clatleglb  18610  isdlat  18614  ipodrsima  18633  chneq1  18704  mgm1  18754  idressid  18779  gsumval2  18790  mgmhmima  18819  sgrp1  18833  mhmimalem  18934  mndind  18938  gsumwspan  18956  efmndmnd  18999  smndex1mnd  19023  sgrp2rid2  19039  sgrp2rid2ex  19040  sgrp2nmndlem4  19041  degenmgm  19051  degenmgm2  19054  pwmnd  19057  dfgrp2  19087  isgrpinv  19118  grpidinv  19123  dfgrp3lem  19162  issubg4  19270  isnsg2  19280  nsgacs  19286  elnmz  19287  cycsubgcl  19335  ghmrn  19357  ghmnsgima  19368  isga  19419  orbsta  19441  cntzfval  19448  elcntz  19450  resscntz  19461  oppgsubg  19491  symgextfo  19550  gsmsymgreqlem2  19559  gsmsymgreq  19560  pmtrdifel  19608  pmtrdifwrdellem3  19611  pmtrdifwrdel2  19614  psgnunilem2  19623  psgnunilem3  19624  odeq  19678  gexid  19709  gexlem2  19710  gexdvds  19712  isslw  19736  sylow2alem1  19745  sylow2alem2  19746  efgval  19845  efgrelexlemb  19878  efgcpbllemb  19883  abl1  19994  dmdprd  20128  dprd2da  20172  pgpfac1lem5  20209  isomnd  20251  ring1  20453  rngisomring  20609  rhmval0  20617  lringuplu  20707  rhmimasubrnglem  20728  isrrg  20861  isabv  20978  islss  21119  lssacs  21152  reslmhm  21237  islbs  21261  pj1lmhm  21285  lbsacsbs  21344  rnglidlmcl  21405  rnglidl0  21419  rspprop  21434  prmidl  21529  zringlpir  21681  psgndiflemA  21815  ocvfval  21880  elocv  21882  iunocv  21895  frlmlbs  22011  islindf  22026  islinds2  22027  islindf2  22028  lindfrn  22035  lsslindf  22044  islindf4  22052  opsrval  22263  ply1coe  22524  cply1coe0bi  22528  mat0dimcrng  22693  mdetunilem1  22835  mdetunilem9  22843  matunitlindflem2  22903  cpmat  22935  cpmatel  22937  1elcpmat  22941  m2cpminvid2lem  22980  basgen2  23215  bastop1  23219  isclo  23313  ordtbaslem  23414  iscn  23461  cnpval  23462  iscnp  23463  iscnp3  23470  lmbr  23484  lmbr2  23485  lmbrf  23486  cnprest  23515  cnprest2  23516  t0sep  23550  isreg  23558  t1sep2  23595  tgcmp  23627  1stcclb  23670  1stcfb  23671  2ndc1stc  23677  1stcrest  23679  2ndcdisj  23683  islly  23695  isnlly  23696  lly1stc  23723  isref  23736  islocfin  23744  elkgen  23763  kgencn  23783  elpt  23799  elptr  23800  ptcnplem  23848  tx1stc  23877  cnmpt21  23898  kqt0lem  23963  isr0  23964  regr1lem2  23967  r0sep  23975  nrmr0reg  23976  flffbas  24222  cnflf  24229  cnflf2  24230  lmflf  24232  txflf  24233  fclsopni  24242  fclsnei  24246  fclsrest  24251  fcfnei  24262  cnfcf  24269  alexsubb  24273  alexsubALTlem3  24276  qustgplem  24348  tsmsfbas  24355  tsmsres  24371  tsmsf1o  24372  tsmsxplem1  24380  ustval  24430  isust  24431  ustincl  24435  ustdiag  24436  ustinvel  24437  ustexhalf  24438  ust0  24447  utopval  24459  ucnval  24503  isucn  24504  isucn2  24505  ucnima  24507  iscfilu  24514  ispsmet  24531  ismet  24550  isxmet  24551  imasdsf1olem  24600  imasf1oxmet  24602  imasf1omet  24603  metss  24735  met1stc  24748  prdsxmslem2  24756  txmetcnp  24774  metucn  24798  tngngp3  24883  nlmvscn  24914  nmoval  24942  nmolb  24944  qtopbaslem  24985  cncfval  25117  elcncf2  25119  mulc1cncf  25134  cncfmet  25138  evth  25188  lebnumlem3  25192  lebnum  25193  xlebnum  25194  ishtpy  25201  isphtpy  25210  pi1xfr  25284  pi1coghm  25290  isclmp  25326  ipcn  25475  lmmbr2  25488  lmmbr3  25489  lmmbrf  25491  cfilfval  25493  iscfil  25494  fmcfil  25501  caufval  25504  iscau  25505  iscau2  25506  iscau3  25507  iscau4  25508  iscauf  25509  caucfil  25512  cfilresi  25524  causs  25527  lmclim  25532  cmetcusp1  25582  minveclem4c  25654  minveclem2  25655  minveclem3b  25657  minveclem4  25661  minveclem6  25663  minveclem7  25664  ovolicc2lem3  25748  ismbl  25755  dyadmax  25827  dyadmbllem  25828  dyadmbl  25829  opnmbllem  25830  ismbf1  25853  ismbf  25857  mbfeqalem2  25871  mbflimsup  25895  mbfi1fseqlem6  25949  mbfi1flimlem  25951  itg2seq  25971  itg2monolem1  25979  isibl  25994  ply1divex  26364  fta1g  26397  dgrco  26502  plydivex  26528  fta1  26539  vieta1  26543  aannenlem1  26561  aannenlem2  26562  aalioulem2  26566  aalioulem3  26567  ulmval  26613  ulm2  26618  ulmi  26619  ulmres  26621  ulmshftlem  26622  ulmcaulem  26627  ulmcau  26628  ulmss  26630  ulmbdd  26631  ulmdvlem1  26633  ulmdvlem3  26635  pilem2  26685  pilem3  26686  cxpcn3  26983  dmarea  27192  rlimcnp  27200  scvxcvx  27220  lgamgulmlem2  27264  lgamgulmlem3  27265  lgamgulmlem5  27267  lgambdd  27271  lgamcvglem  27274  isppw2  27349  perfectlem2  27464  2sqlem6  27657  2sqlem10  27662  addsq2reu  27674  2sqreulem1  27680  2sqreunnlem1  27683  dchrisumlema  27722  dchrisumlem2  27724  dchrisumlem3  27725  pntpbnd  27822  pntibndlem3  27826  pntibnd  27827  pntleme  27842  pntlem3  27843  pntlemp  27844  pnt3  27846  ltsval  27881  nosupprefixmo  27934  noinfprefixmo  27935  nosupcbv  27936  nosupno  27937  nosupdm  27938  nosupfv  27940  nosupres  27941  nosupbnd1lem1  27942  nosupbnd1lem3  27944  nosupbnd1lem5  27946  noinfcbv  27951  noinfno  27952  noinfdm  27953  noinffv  27955  noinfres  27956  noinfbnd1lem3  27959  noinfbnd1lem5  27961  noetalem1  27975  noetalem2  27976  nocvxminlem  28017  brslts  28025  sltssnb  28032  conway  28042  etaslts  28056  lesrec  28062  eqcuts3  28067  madebdaylemlrcut  28162  madebday  28163  bdayle  28179  cofcutr  28187  cutmax  28197  cutmin  28198  lrrecfr  28206  addsprop  28239  negsunif  28318  addonbday  28542  onsfi  28619  n0subs  28626  bdayn0p1  28632  bdaypw2n0bndlem  28726  bdayfinbndlem2  28731  z12zsodd  28745  istrkgld  28798  axtg5seg  28804  tgcgr4  28871  perpln1  29062  perpln2  29063  isperp  29064  prlngmo2  29299  brbtwn2  29348  colinearalg  29353  axsegconlem1  29360  axsegcon  29370  ax5seglem4  29375  ax5seglem5  29376  axlowdim  29404  axeuclidlem  29405  axcontlem1  29407  axcontlem2  29408  axcontlem4  29410  axcontlem5  29411  axcontlem8  29414  axcontlem12  29418  elntg2  29428  uvtxusgr  29848  rgrx0ndm  30039  ewlksfval  30047  wksfval  30055  wwlks  30289  wlkiswwlks2  30329  clwwlk  30439  1conngr  30660  frgrwopregasn  30782  frgrwopregbsn  30783  frgrwopreglem5ALT  30788  frgrregord013  30861  isgrpo  30964  isgrpoi  30965  grpoideu  30976  grpoidinv2  30982  vciOLD  31028  isvclem  31044  cnidOLD  31049  isnvlem  31077  nvi  31081  lnoval  31219  islno  31220  isblo3i  31268  blo3i  31269  blocnilem  31271  ajfval  31276  ubthlem1  31337  ubthlem2  31338  ubthlem3  31339  ubth  31340  minvecolem2  31342  minvecolem3  31343  minvecolem4c  31346  minvecolem4  31347  minvecolem5  31348  minvecolem6  31349  minvecolem7  31350  h2hcau  31446  h2hlm  31447  hilid  31628  hcau  31651  hlimi  31655  hlim2  31659  ocel  31748  adjsym  32300  ellnop  32325  ellnfn  32350  hhcno  32371  hhcnf  32372  lnopeq  32476  elunop2  32480  lnophm  32486  lnconi  32500  lnopcnbd  32503  lnfncnbd  32524  imaelshi  32525  riesz3i  32529  riesz4i  32530  riesz4  32531  riesz1  32532  cnlnadjlem2  32535  cnlnadjlem5  32538  cnlnadjlem8  32541  cnlnadji  32543  nmopadjlei  32555  cnvbraval  32577  leopg  32589  leoppos  32593  mdbr  32761  dmdbr  32766  cdj3i  32908  disjunsn  33054  funcnv5mpt  33127  fgreu  33131  fcnvgreu  33132  xrge0infss  33218  wrdt2ind  33382  mgccole1  33417  mgccole2  33418  mgcmnt1  33419  mgcmnt2  33420  gsumhashmul  33494  isfxp  33595  fxpgaeq  33596  inftmrel  33607  isinftm  33608  archiabl  33625  isarchiofld  33626  elrgspnlem4  33672  0nellinds  33792  lindssn  33798  elrspunidl  33843  ismxidl  33852  1arithidom  33934  1arithufdlem3  33943  evl1deg1  33973  evl1deg2  33974  evl1deg3  33975  vietalem  34076  vieta  34077  crefeq  34342  zarcmplem  34378  esum2d  34590  sigaval  34608  issgon  34620  isrnmeas  34698  ismbfm  34749  mbfmcst  34757  elcarsg  34803  sitgval  34830  eulerpartlemd  34864  ballotleme  34995  tgoldbachgt  35158  bnj1185  35289  bnj1385  35328  bnj66  35356  bnj106  35364  bnj155  35375  bnj852  35417  bnj893  35424  bnj1228  35507  bnj1234  35509  bnj1463  35551  nummin  35585  rankfilimbi  35596  r1omhfb  35609  elscott  35611  fineqvnttrclse  35637  r1omhfbregs  35650  gblacfnacd  35686  onvf1odlem4  35690  vonf1wev  35692  vonf1owevOLD  35694  derangenlem  35737  subfacp1lem3  35748  subfacp1lem5  35750  subfacp1lem6  35751  subfacp1  35752  erdszelem8  35764  kur14  35782  cnpconn  35796  resconn  35812  cvmscbv  35824  iscvm  35825  cvmsi  35831  cvmsval  35832  cvmlift3lem2  35886  snmlval  35897  satfv1  35929  fmlasucdisj  35965  satffunlem1lem1  35968  satffunlem2lem1  35970  satfv1fvfmla1  35989  mclsssvlem  36128  mclsval  36129  mclsax  36135  mclsind  36136  dfon2lem9  36355  dfrdg2  36359  dfrdg3  36360  fwddifnval  36730  nmulprop  36757  ltnadd  36785  nn0prpwlem  36928  isfne  36945  isfne4  36946  isfne2  36948  isfne3  36949  neibastop3  36968  topmeet  36970  topjoin  36971  filnetlem4  36987  weiunlem  37069  weiunfrlem  37070  dfttc4lem1  37134  dfttc4  37136  elttcirr  37137  unblimceq0lem  37190  unblimceq0  37191  unbdqndv2  37195  taupilemrplb  38059  fin2so  38348  lindsadd  38354  ptrecube  38356  poimirlem2  38358  poimirlem3  38359  poimirlem4  38360  poimirlem24  38380  poimirlem25  38381  poimirlem26  38382  poimirlem27  38383  poimirlem28  38384  poimirlem29  38385  poimirlem30  38386  poimirlem32  38388  poimir  38389  heicant  38391  mblfinlem1  38393  mblfinlem2  38394  voliunnfl  38400  volsupnfl  38401  mbfresfi  38402  itg2addnc  38410  upixp  38466  indexdom  38471  filbcmb  38477  sdclem2  38479  fdc  38482  lmclim2  38495  caures  38497  istotbnd  38506  istotbnd3  38508  sstotbnd  38512  isbnd  38517  heibor  38558  bfp  38561  rrncmslem  38569  isgrpda  38692  idlval  38750  isidl  38751  0idl  38762  unichnidl  38768  pridl  38774  ismaxidl  38777  smprngopr  38789  igenval2  38803  prnc  38804  ispridlc  38807  scottexf  38903  scott0f  38904  disjsuc2  39149  riotasvd  39816  islfl  39920  eqlkr  39959  eqlkr3  39961  glbconN  40237  hlsuprexch  40241  ispsubsp  40605  ldilset  40969  isldil  40970  dilsetN  41013  isdilN  41014  trlset  41021  trlval  41022  cdleme27b  41228  cdleme29b  41235  cdleme31so  41239  cdleme31sn1  41241  cdleme31sn1c  41248  cdleme31fv  41250  cdleme40v  41329  istendo  41620  cdlemkid3N  41793  cdlemkid4  41794  cdlemkid5  41795  dihfval  42091  dihval  42092  islpolN  42343  hdmapffval  42686  hdmapfval  42687  hdmapval  42688  hdmapval2lem  42691  hgmapffval  42745  hgmapfval  42746  hgmapval  42747  hgmapvs  42751  isprimroot  42946  aks6d1c1p1  42960  hashscontpow1  42974  sticksstones2  43000  unitscyglem3  43050  exfinfldd  43056  qsalrel  43095  supinf  43096  sn-sup2  43366  fsuppind  43423  isnacs  43536  isnacs2  43538  nacsfix  43544  mzpclval  43557  elmzpcl  43558  rencldnfilem  43648  infmrgelbi  43706  pellfundre  43709  pellfundlb  43712  wepwsolem  43870  fnwe2lem2  43879  aomclem8  43889  dfac11  43890  gicabl  43927  islnr3  43943  hbtlem2  43952  hbtlem5  43956  onintunirab  44055  onsucf1lem  44097  cantnfresb  44152  safesnsupfilb  44245  rp-brsslt  44250  fiinfi  44400  clsk1independent  44873  ntrclsk13  44898  gneispacess2  44973  imo72b2lem0  44992  imo72b2lem2  44994  imo72b2lem1  44996  imo72b2  44999  mnuop23d  45077  ismnushort  45112  ralabsobidv  45782  0elaxnul  45793  pwclaxpow  45794  prclaxpr  45795  uniclaxun  45796  omssaxinf2  45798  modelac8prim  45802  wfac8prim  45812  permac8prim  45824  evth2f  45836  evthf  45848  fnchoice  45850  uzwo4  45874  wessf1ornlem  46004  disjinfi  46011  rnmptlb  46059  rnmptbdd  46061  rnmptbd2  46065  rnmptbd  46072  dstregt0  46102  upbdrech2  46128  rexabslelem  46233  rexabsle  46234  uzub  46246  infrpgernmpt  46280  mccl  46415  ellimcabssub0  46434  climf  46439  clim2f  46451  limsupre  46456  clim2cf  46465  clim0cf  46469  climf2  46481  clim2f2  46485  clim2d  46488  limsupref  46500  limsupbnd1f  46501  climinf2  46522  limsuppnf  46526  climinfmpt  46530  climinf3  46531  limsupubuzmpt  46534  limsupmnf  46536  limsupre2lem  46539  limsupre2  46540  limsupmnfuzlem  46541  limsupmnfuz  46542  limsupre2mpt  46545  limsupre3lem  46547  limsupre3  46548  limsupre3mpt  46549  limsupre3uz  46551  limsupreuz  46552  limsupreuzmpt  46554  climuz  46559  liminfreuzlem  46617  liminfreuz  46618  cnrefiisplem  46644  xlimmnfvlem1  46647  xlimmnfv  46649  xlimpnfvlem1  46651  xlimpnfv  46653  xlimmnfmpt  46658  xlimpnfmpt  46659  cncfshift  46689  cncfperiod  46694  fperdvper  46734  dvbdfbdioo  46745  ioodvbdlimc1lem2  46747  ioodvbdlimc2lem  46749  dvnprodlem3  46763  stoweidlem5  46820  stoweidlem9  46824  stoweidlem15  46830  stoweidlem16  46831  stoweidlem27  46842  stoweidlem28  46843  stoweidlem31  46846  stoweidlem34  46849  stoweidlem37  46852  stoweidlem46  46861  stoweidlem48  46863  stoweidlem51  46866  stoweidlem52  46867  stoweidlem59  46874  wallispilem3  46882  stirlinglem13  46901  fourierdlem2  46924  fourierdlem3  46925  fourierdlem16  46938  fourierdlem20  46942  fourierdlem21  46943  fourierdlem22  46944  fourierdlem25  46947  fourierdlem39  46961  fourierdlem42  46964  fourierdlem54  46975  fourierdlem64  46985  fourierdlem77  46998  fourierdlem83  47004  fourierdlem103  47024  fourierdlem104  47025  subsaliuncllem  47172  iundjiun  47275  meaiunincf  47298  caragenval  47308  isome  47309  caragenel  47310  omessle  47313  ovnlerp  47377  hoidmvlelem3  47412  hoidmvle  47415  issmflem  47542  issmfgt  47571  smfmullem2  47607  smfmullem4  47609  smfmul  47610  smfsuplem2  47627  smfsup  47629  smfinflem  47632  smfinf  47633  fsupdm  47657  finfdm  47661  cfsetsnfsetf  47933  cbvral2  47978  2reu8i  47988  2reuimp0  47989  dfdfat2  48003  iccpart  48303  iccpartigtl  48310  paireqne  48398  reupr  48409  perfectALTVlem2  48625  bgoldbachlt  48716  tgoldbachlt  48719  grimidvtxedg  48788  grimcnv  48791  grimco  48792  isuspgrim0  48797  gricushgr  48820  ushggricedg  48830  uhgrimisgrgric  48834  isubgr3stgr  48878  isgrlim  48885  isgrlim2  48886  uspgrlim  48895  grlicsym  48916  grlictr  48918  gpg5nbgrvtx03star  48983  gpg5nbgr3star  48984  pgnbgreunbgr  49028  upwlksfval  49038  nn0mnd  49081  uzlidlring  49137  smprngprmrng  49241  ply1mulgsumlem1  49303  ply1mulgsumlem2  49304  linindslinci  49365  lindslinindsimp1  49374  lindslinindsimp2lem5  49379  lindslinindsimp2  49380  linds0  49382  lindsrng01  49385  snlindsntor  49388  lmod1  49409  ldepsnlinc  49425  bigoval  49466  elbigo2r  49470  nn0sumshdiglem2  49539  eenglngeehlnmlem1  49654  eenglngeehlnmlem2  49655  lubeldm2d  49871  glbeldm2d  49872  lubsscl  49873  glbsscl  49874  ipolubdm  49900  ipolub  49901  ipoglbdm  49903  ipoglb  49904  nelsubc3lem  49983  upfval2  50090  upfval3  50091  isthincd2lem2  50348  setc1onsubc  50515  cnelsubclem  50516  setrec1lem2  50601