Theorem ralbidv 3160

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3053

This theorem is referenced by:  2ralbidv  3201  rexralbidv  3203  3ralbidv  3204  4ralbidv  3205  cbvral2vw  3219  cbvral4vw  3222  cbvral2v  3339  rspceaimv  3583  rspc2  3586  rspc2v  3588  rspc3v  3593  rspc4v  3597  reu6i  3687  reu7  3691  sbcralt  3823  reu8nf  3828  raaan  4472  raaanv  4473  raaan2  4476  2reu4lem  4477  reusngf  4632  2ralsng  4636  rexreusng  4637  reuprg0  4660  issn  4789  2ralunsn  4852  elintg  4911  elintrabg  4917  eliin  4952  disjprg  5095  disjxun  5097  brralrspcev  5159  reusv2lem2  5345  reusv3  5351  poeq1  5536  solin  5560  somo  5572  frirr  5601  fr2nr  5602  frminex  5604  wereu2  5622  posn  5711  frsn  5713  ralxpf  5796  cnvpo  6246  reu3op  6251  reuop  6252  dfpo2  6255  frpomin  6299  fnmptfvd  6988  iinpreima  7016  dff4  7048  dff13f  7203  fpropnf1  7215  f1ounsn  7220  eusvobj2  7352  ovanraleqv  7384  f1opr  7416  ofreq  7628  sorpssuni  7679  sorpssint  7680  fr3nr  7719  onssmin  7739  funcnvuni  7876  f1oweALT  7918  frxp  8070  frxp2  8088  xpord2indlem  8091  frxp3  8095  xpord3inddlem  8098  poseq  8102  soseq  8103  frecseq123  8226  csbfrecsg  8228  frrlem1  8230  frrlem13  8242  smoeq  8284  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  9596  oemapvali  9597  cantnf  9606  wemapwe  9610  ttrcleq  9622  ttrcltr  9629  ttrclss  9633  ttrclselem2  9639  rankval3b  9742  unbndrank  9758  rankunb  9766  rankuni2b  9769  tcrank  9800  scottex  9801  scottexs  9803  scott0s  9804  bnd2  9809  updjud  9850  dfac8clem  9946  ac5num  9950  acni  9959  acni2  9960  alephval3  10024  dfac4  10036  dfac5lem5  10041  dfac5  10043  dfac2a  10044  dfac2b  10045  dfacacn  10056  kmlem2  10066  kmlem13  10077  cflem  10159  cflemOLD  10160  cflecard  10167  cfeq0  10170  cfsuc  10171  cfflb  10173  cofsmo  10183  cfsmolem  10184  cfcoflem  10186  coftr  10187  alephsing  10190  fin23lem11  10231  isfin3ds  10243  fin23lem17  10252  fin23lem39  10264  isf33lem  10280  isf34lem6  10294  fin1a2lem13  10326  hsmexlem4  10343  hsmex  10346  axcc2lem  10350  axcc3  10352  dcomex  10361  axdc2lem  10362  axdc3lem2  10365  axdc3lem3  10366  axdc3  10368  axdc4lem  10369  axcclem  10371  zorn2lem2  10411  zorn2lem7  10416  zorn2g  10417  zornn0g  10419  ttukeylem7  10429  axdclem2  10434  brdom3  10442  brdom7disj  10445  brdom6disj  10446  alephval2  10487  inar1  10690  axgroth6  10743  pinq  10842  nqereu  10844  prlem934  10948  supexpr  10969  supsrlem  11026  axpre-sup  11084  dedekind  11300  dedekindle  11301  fiminre2  12094  lbreu  12096  sup2  12102  infm3  12105  nnsub  12193  uzwo  12828  nnwof  12831  ublbneg  12850  lbzbi  12853  zsupss  12854  uzsupss  12857  uzwo3  12860  zmax  12862  rpnnen1lem1  12895  rpnnen1lem3  12896  rpnnen1lem4  12897  rpnnen1lem5  12898  xrsupsslem  13226  xrinfmsslem  13227  xrsupss  13228  xrinfmss  13229  flval2  13738  axdc4uzlem  13910  ssnn0fi  13912  fsuppmapnn0fiubex  13919  faclbnd4lem4  14223  bccl  14249  hashgt12el  14349  hashbc  14380  hashge2el2dif  14407  wrdind  14649  wrd2ind  14650  rexanre  15274  rexico  15281  cau4  15284  reusq0  15392  clim  15421  rlim  15422  rlim2  15423  clim2  15431  clim2c  15432  clim0c  15434  rlim0  15435  rlim0lt  15436  ello12r  15444  ello1d  15450  elo12r  15455  rlimresb  15492  rlimcld2  15505  climabs0  15512  rlimo1  15544  lo1add  15554  lo1mul  15555  isercoll  15595  incexclem  15763  sqrt2irr  16178  gcdcllem1  16430  gcdcllem2  16431  dfgcd2  16477  fissn0dvds  16550  dvdslcmf  16562  lcmfledvds  16563  lcmf  16564  lcmfunsnlem1  16568  lcmfunsnlem2lem1  16569  lcmfunsnlem  16572  lcmfdvds  16573  reumodprminv  16736  pc2dvds  16811  pcz  16813  prmpwdvds  16836  infpn2  16845  prmreclem2  16849  prmreclem3  16850  prmreclem5  16852  prmreclem6  16853  vdwlem6  16918  vdwlem8  16920  vdwlem13  16925  vdwnnlem1  16927  vdwnn  16930  ramcl  16961  cshwrepswhash1  17034  prdsleval  17401  imasval  17436  imasaddfnlem  17453  imasvscafn  17462  mrisval  17557  isacs  17578  isacs2  17580  isacs1i  17584  mreacs  17585  acsfn  17586  acsfn2  17590  iscatd  17600  catidex  17601  catideu  17602  cidval  17604  catidd  17607  comfeq  17633  catpropd  17636  ismon  17661  isfunc  17792  isnat  17878  isinito  17924  istermo  17925  isprs  18223  drsdirfi  18232  ispos  18241  lubfval  18275  lubeldm  18278  lubval  18281  lubprop  18283  lublecllem  18285  glbfval  18288  glbeldm  18291  glbval  18294  glbprop  18296  joinval2lem  18305  joinlem  18308  meetval2lem  18319  meetlem  18322  poslubmo  18336  posglbmo  18337  poslubd  18338  resspos  18356  isglbd  18436  lubl  18439  lubun  18442  clatleglb  18445  isdlat  18449  ipodrsima  18468  chneq1  18539  mgm1  18587  gsumval2  18615  mgmhmima  18644  sgrp1  18658  mhmimalem  18753  mndind  18757  gsumwspan  18775  efmndmnd  18818  smndex1mnd  18839  sgrp2rid2  18855  sgrp2rid2ex  18856  sgrp2nmndlem4  18857  pwmnd  18866  dfgrp2  18896  isgrpinv  18927  grpidinv  18932  dfgrp3lem  18972  issubg4  19079  isnsg2  19089  nsgacs  19095  elnmz  19096  cycsubgcl  19139  ghmrn  19162  ghmnsgima  19173  isga  19224  orbsta  19246  cntzfval  19253  elcntz  19255  resscntz  19266  oppgsubg  19296  symgextfo  19355  gsmsymgreqlem2  19364  gsmsymgreq  19365  pmtrdifel  19413  pmtrdifwrdellem3  19416  pmtrdifwrdel2  19419  psgnunilem2  19428  psgnunilem3  19429  odeq  19483  gexid  19514  gexlem2  19515  gexdvds  19517  isslw  19541  sylow2alem1  19550  sylow2alem2  19551  efgval  19650  efgrelexlemb  19683  efgcpbllemb  19688  abl1  19799  dmdprd  19933  dprd2da  19977  pgpfac1lem5  20014  isomnd  20056  ring1  20249  rngisomring  20407  lringuplu  20481  rhmimasubrnglem  20502  isrrg  20635  isabv  20748  islss  20889  lssacs  20922  reslmhm  21008  islbs  21032  pj1lmhm  21056  lbsacsbs  21115  rnglidlmcl  21175  rnglidl0  21188  zringlpir  21426  psgndiflemA  21560  ocvfval  21625  elocv  21627  iunocv  21640  frlmlbs  21756  islindf  21771  islinds2  21772  islindf2  21773  lindfrn  21780  lsslindf  21789  islindf4  21797  opsrval  22005  ply1coe  22246  cply1coe0bi  22250  mat0dimcrng  22418  mdetunilem1  22560  mdetunilem9  22568  cpmat  22657  cpmatel  22659  1elcpmat  22663  m2cpminvid2lem  22702  basgen2  22937  bastop1  22941  isclo  23035  ordtbaslem  23136  iscn  23183  cnpval  23184  iscnp  23185  iscnp3  23192  lmbr  23206  lmbr2  23207  lmbrf  23208  cnprest  23237  cnprest2  23238  t0sep  23272  isreg  23280  t1sep2  23317  tgcmp  23349  1stcclb  23392  1stcfb  23393  2ndc1stc  23399  1stcrest  23401  2ndcdisj  23404  islly  23416  isnlly  23417  lly1stc  23444  isref  23457  islocfin  23465  elkgen  23484  kgencn  23504  elpt  23520  elptr  23521  ptcnplem  23569  tx1stc  23598  cnmpt21  23619  kqt0lem  23684  isr0  23685  regr1lem2  23688  r0sep  23696  nrmr0reg  23697  flffbas  23943  cnflf  23950  cnflf2  23951  lmflf  23953  txflf  23954  fclsopni  23963  fclsnei  23967  fclsrest  23972  fcfnei  23983  cnfcf  23990  alexsubb  23994  alexsubALTlem3  23997  qustgplem  24069  tsmsfbas  24076  tsmsres  24092  tsmsf1o  24093  tsmsxplem1  24101  ustval  24151  isust  24152  ustincl  24156  ustdiag  24157  ustinvel  24158  ustexhalf  24159  ust0  24168  utopval  24180  ucnval  24224  isucn  24225  isucn2  24226  ucnima  24228  iscfilu  24235  ispsmet  24252  ismet  24271  isxmet  24272  imasdsf1olem  24321  imasf1oxmet  24323  imasf1omet  24324  metss  24456  met1stc  24469  prdsxmslem2  24477  txmetcnp  24495  metucn  24519  tngngp3  24604  nlmvscn  24635  nmoval  24663  nmolb  24665  qtopbaslem  24706  cncfval  24841  elcncf2  24843  mulc1cncf  24858  cncfmet  24862  evth  24918  lebnumlem3  24922  lebnum  24923  xlebnum  24924  ishtpy  24931  isphtpy  24940  pi1xfr  25015  pi1coghm  25021  isclmp  25057  ipcn  25206  lmmbr2  25219  lmmbr3  25220  lmmbrf  25222  cfilfval  25224  iscfil  25225  fmcfil  25232  caufval  25235  iscau  25236  iscau2  25237  iscau3  25238  iscau4  25239  iscauf  25240  caucfil  25243  cfilresi  25255  causs  25258  lmclim  25263  cmetcusp1  25313  minveclem4c  25385  minveclem2  25386  minveclem3b  25388  minveclem4  25392  minveclem6  25394  minveclem7  25395  ovolicc2lem3  25480  ismbl  25487  dyadmax  25559  dyadmbllem  25560  dyadmbl  25561  opnmbllem  25562  ismbf1  25585  ismbf  25589  mbfeqalem2  25603  mbflimsup  25627  mbfi1fseqlem6  25681  mbfi1flimlem  25683  itg2seq  25703  itg2monolem1  25711  isibl  25726  ply1divex  26102  fta1g  26135  dgrco  26241  plydivex  26265  fta1  26276  vieta1  26280  aannenlem1  26296  aannenlem2  26297  aalioulem2  26301  aalioulem3  26302  ulmval  26349  ulm2  26354  ulmi  26355  ulmres  26357  ulmshftlem  26358  ulmcaulem  26363  ulmcau  26364  ulmss  26366  ulmbdd  26367  ulmdvlem1  26369  ulmdvlem3  26371  pilem2  26422  pilem3  26423  cxpcn3  26718  dmarea  26927  rlimcnp  26935  scvxcvx  26956  lgamgulmlem2  27000  lgamgulmlem3  27001  lgamgulmlem5  27003  lgambdd  27007  lgamcvglem  27010  isppw2  27085  perfectlem2  27201  2sqlem6  27394  2sqlem10  27399  addsq2reu  27411  2sqreulem1  27417  2sqreunnlem1  27420  dchrisumlema  27459  dchrisumlem2  27461  dchrisumlem3  27462  pntpbnd  27559  pntibndlem3  27563  pntibnd  27564  pntleme  27579  pntlem3  27580  pntlemp  27581  pnt3  27583  ltsval  27619  nosupprefixmo  27672  noinfprefixmo  27673  nosupcbv  27674  nosupno  27675  nosupdm  27676  nosupfv  27678  nosupres  27679  nosupbnd1lem1  27680  nosupbnd1lem3  27682  nosupbnd1lem5  27684  noinfcbv  27689  noinfno  27690  noinfdm  27691  noinffv  27693  noinfres  27694  noinfbnd1lem3  27697  noinfbnd1lem5  27699  noetalem1  27713  noetalem2  27714  nocvxminlem  27754  brslts  27762  sltssnb  27769  conway  27779  etaslts  27793  lesrec  27799  eqcuts3  27804  madebdaylemlrcut  27899  madebday  27900  bdayle  27916  cofcutr  27924  cutmax  27934  cutmin  27935  lrrecfr  27943  addsprop  27976  negsunif  28055  addonbday  28279  onsfi  28356  n0subs  28363  bdayn0p1  28369  bdaypw2n0bndlem  28463  bdayfinbndlem2  28468  z12zsodd  28482  istrkgld  28535  axtg5seg  28541  tgcgr4  28607  perpln1  28786  perpln2  28787  isperp  28788  brbtwn2  28982  colinearalg  28987  axsegconlem1  28994  axsegcon  29004  ax5seglem4  29009  ax5seglem5  29010  axlowdim  29038  axeuclidlem  29039  axcontlem1  29041  axcontlem2  29042  axcontlem4  29044  axcontlem5  29045  axcontlem8  29048  axcontlem12  29052  elntg2  29062  uvtxusgr  29479  rgrx0ndm  29671  ewlksfval  29679  wksfval  29687  wwlks  29912  wlkiswwlks2  29952  clwwlk  30062  1conngr  30273  frgrwopregasn  30395  frgrwopregbsn  30396  frgrwopreglem5ALT  30401  frgrregord013  30474  isgrpo  30576  isgrpoi  30577  grpoideu  30588  grpoidinv2  30594  vciOLD  30640  isvclem  30656  cnidOLD  30661  isnvlem  30689  nvi  30693  lnoval  30831  islno  30832  isblo3i  30880  blo3i  30881  blocnilem  30883  ajfval  30888  ubthlem1  30949  ubthlem2  30950  ubthlem3  30951  ubth  30952  minvecolem2  30954  minvecolem3  30955  minvecolem4c  30958  minvecolem4  30959  minvecolem5  30960  minvecolem6  30961  minvecolem7  30962  h2hcau  31058  h2hlm  31059  hilid  31240  hcau  31263  hlimi  31267  hlim2  31271  ocel  31360  adjsym  31912  ellnop  31937  ellnfn  31962  hhcno  31983  hhcnf  31984  lnopeq  32088  elunop2  32092  lnophm  32098  lnconi  32112  lnopcnbd  32115  lnfncnbd  32136  imaelshi  32137  riesz3i  32141  riesz4i  32142  riesz4  32143  riesz1  32144  cnlnadjlem2  32147  cnlnadjlem5  32150  cnlnadjlem8  32153  cnlnadji  32155  nmopadjlei  32167  cnvbraval  32189  leopg  32201  leoppos  32205  mdbr  32373  dmdbr  32378  cdj3i  32520  disjunsn  32672  funcnv5mpt  32748  fgreu  32752  fcnvgreu  32753  xrge0infss  32842  wrdt2ind  33037  mgccole1  33074  mgccole2  33075  mgcmnt1  33076  mgcmnt2  33077  gsumhashmul  33152  isfxp  33252  fxpgaeq  33253  inftmrel  33264  isinftm  33265  archiabl  33282  isarchiofld  33283  elrgspnlem4  33329  0nellinds  33453  lindssn  33461  elrspunidl  33511  prmidl  33523  ismxidl  33545  1arithidom  33620  1arithufdlem3  33629  evl1deg1  33659  evl1deg2  33660  evl1deg3  33661  vietalem  33737  vieta  33738  crefeq  34004  zarcmplem  34040  esum2d  34252  sigaval  34270  issgon  34282  isrnmeas  34359  ismbfm  34410  mbfmcst  34418  elcarsg  34464  sitgval  34491  eulerpartlemd  34525  ballotleme  34656  tgoldbachgt  34822  bnj1185  34951  bnj1385  34990  bnj66  35018  bnj106  35026  bnj155  35037  bnj852  35079  bnj893  35086  bnj1228  35169  bnj1234  35171  bnj1463  35213  nummin  35251  rankfilimbi  35259  r1omhfb  35270  fineqvnttrclse  35282  r1omhfbregs  35295  gblacfnacd  35298  onvf1odlem4  35302  vonf1owev  35304  derangenlem  35367  subfacp1lem3  35378  subfacp1lem5  35380  subfacp1lem6  35381  subfacp1  35382  erdszelem8  35394  kur14  35412  cnpconn  35426  resconn  35442  cvmscbv  35454  iscvm  35455  cvmsi  35461  cvmsval  35462  cvmlift3lem2  35516  snmlval  35527  satfv1  35559  fmlasucdisj  35595  satffunlem1lem1  35598  satffunlem2lem1  35600  satfv1fvfmla1  35619  mclsssvlem  35758  mclsval  35759  mclsax  35765  mclsind  35766  dfon2lem9  35985  dfrdg2  35989  dfrdg3  35990  fwddifnval  36359  nn0prpwlem  36518  isfne  36535  isfne4  36536  isfne2  36538  isfne3  36539  neibastop3  36558  topmeet  36560  topjoin  36561  filnetlem4  36577  weiunlem  36659  weiunfrlem  36660  unblimceq0lem  36708  unblimceq0  36709  unbdqndv2  36713  taupilemrplb  37527  fin2so  37810  lindsadd  37816  matunitlindflem2  37820  ptrecube  37823  poimirlem2  37825  poimirlem3  37826  poimirlem4  37827  poimirlem24  37847  poimirlem25  37848  poimirlem26  37849  poimirlem27  37850  poimirlem28  37851  poimirlem29  37852  poimirlem30  37853  poimirlem32  37855  poimir  37856  heicant  37858  mblfinlem1  37860  mblfinlem2  37861  voliunnfl  37867  volsupnfl  37868  mbfresfi  37869  itg2addnc  37877  upixp  37932  indexdom  37937  filbcmb  37943  sdclem2  37945  fdc  37948  lmclim2  37961  caures  37963  istotbnd  37972  istotbnd3  37974  sstotbnd  37978  isbnd  37983  heibor  38024  bfp  38027  rrncmslem  38035  isgrpda  38158  idlval  38216  isidl  38217  0idl  38228  unichnidl  38234  pridl  38240  ismaxidl  38243  smprngopr  38255  igenval2  38269  prnc  38270  ispridlc  38273  scottexf  38371  scott0f  38372  disjsuc2  38617  riotasvd  39284  islfl  39388  eqlkr  39427  eqlkr3  39429  glbconN  39705  hlsuprexch  39709  ispsubsp  40073  ldilset  40437  isldil  40438  dilsetN  40481  isdilN  40482  trlset  40489  trlval  40490  cdleme27b  40696  cdleme29b  40703  cdleme31so  40707  cdleme31sn1  40709  cdleme31sn1c  40716  cdleme31fv  40718  cdleme40v  40797  istendo  41088  cdlemkid3N  41261  cdlemkid4  41262  cdlemkid5  41263  dihfval  41559  dihval  41560  islpolN  41811  hdmapffval  42154  hdmapfval  42155  hdmapval  42156  hdmapval2lem  42159  hgmapffval  42213  hgmapfval  42214  hgmapval  42215  hgmapvs  42219  isprimroot  42415  aks6d1c1p1  42429  hashscontpow1  42443  sticksstones2  42469  unitscyglem3  42519  exfinfldd  42525  qsalrel  42563  supinf  42564  sn-sup2  42813  fsuppind  42900  isnacs  43013  isnacs2  43015  nacsfix  43021  mzpclval  43034  elmzpcl  43035  rencldnfilem  43129  infmrgelbi  43187  pellfundre  43190  pellfundlb  43193  wepwsolem  43351  fnwe2lem2  43360  aomclem8  43370  dfac11  43371  gicabl  43408  islnr3  43424  hbtlem2  43433  hbtlem5  43437  onintunirab  43536  onsucf1lem  43578  cantnfresb  43633  safesnsupfilb  43726  rp-brsslt  43731  fiinfi  43881  clsk1independent  44354  ntrclsk13  44379  gneispacess2  44454  imo72b2lem0  44473  imo72b2lem2  44475  imo72b2lem1  44477  imo72b2  44480  scottelrankd  44555  mnuop23d  44574  ismnushort  44609  ralabsobidv  45280  0elaxnul  45291  pwclaxpow  45292  prclaxpr  45293  uniclaxun  45294  omssaxinf2  45296  modelac8prim  45300  wfac8prim  45310  permac8prim  45322  evth2f  45327  evthf  45339  fnchoice  45341  uzwo4  45365  wessf1ornlem  45496  disjinfi  45503  rnmptlb  45554  rnmptbdd  45556  rnmptbd2  45560  rnmptbd  45567  dstregt0  45597  upbdrech2  45623  rexabslelem  45729  rexabsle  45730  uzub  45742  infrpgernmpt  45776  mccl  45911  ellimcabssub0  45930  climf  45935  clim2f  45947  limsupre  45952  clim2cf  45961  clim0cf  45965  climf2  45977  clim2f2  45981  clim2d  45984  limsupref  45996  limsupbnd1f  45997  climinf2  46018  limsuppnf  46022  climinfmpt  46026  climinf3  46027  limsupubuzmpt  46030  limsupmnf  46032  limsupre2lem  46035  limsupre2  46036  limsupmnfuzlem  46037  limsupmnfuz  46038  limsupre2mpt  46041  limsupre3lem  46043  limsupre3  46044  limsupre3mpt  46045  limsupre3uz  46047  limsupreuz  46048  limsupreuzmpt  46050  climuz  46055  liminfreuzlem  46113  liminfreuz  46114  cnrefiisplem  46140  xlimmnfvlem1  46143  xlimmnfv  46145  xlimpnfvlem1  46147  xlimpnfv  46149  xlimmnfmpt  46154  xlimpnfmpt  46155  cncfshift  46185  cncfperiod  46190  fperdvper  46230  dvbdfbdioo  46241  ioodvbdlimc1lem2  46243  ioodvbdlimc2lem  46245  dvnprodlem3  46259  stoweidlem5  46316  stoweidlem9  46320  stoweidlem15  46326  stoweidlem16  46327  stoweidlem27  46338  stoweidlem28  46339  stoweidlem31  46342  stoweidlem34  46345  stoweidlem37  46348  stoweidlem46  46357  stoweidlem48  46359  stoweidlem51  46362  stoweidlem52  46363  stoweidlem59  46370  wallispilem3  46378  stirlinglem13  46397  fourierdlem2  46420  fourierdlem3  46421  fourierdlem16  46434  fourierdlem20  46438  fourierdlem21  46439  fourierdlem22  46440  fourierdlem25  46443  fourierdlem39  46457  fourierdlem42  46460  fourierdlem54  46471  fourierdlem64  46481  fourierdlem77  46494  fourierdlem83  46500  fourierdlem103  46520  fourierdlem104  46521  subsaliuncllem  46668  iundjiun  46771  meaiunincf  46794  caragenval  46804  isome  46805  caragenel  46806  omessle  46809  ovnlerp  46873  hoidmvlelem3  46908  hoidmvle  46911  issmflem  47038  issmfgt  47067  smfmullem2  47103  smfmullem4  47105  smfmul  47106  smfsuplem2  47123  smfsup  47125  smfinflem  47128  smfinf  47129  fsupdm  47153  finfdm  47157  cfsetsnfsetf  47371  cbvral2  47416  2reu8i  47426  2reuimp0  47427  dfdfat2  47441  iccpart  47729  iccpartigtl  47736  paireqne  47824  reupr  47835  perfectALTVlem2  48035  bgoldbachlt  48126  tgoldbachlt  48129  grimidvtxedg  48198  grimcnv  48201  grimco  48202  isuspgrim0  48207  gricushgr  48230  ushggricedg  48240  uhgrimisgrgric  48244  isubgr3stgr  48288  isgrlim  48295  isgrlim2  48296  uspgrlim  48305  grlicsym  48326  grlictr  48328  gpg5nbgrvtx03star  48393  gpg5nbgr3star  48394  pgnbgreunbgr  48438  upwlksfval  48448  nn0mnd  48492  uzlidlring  48548  ply1mulgsumlem1  48699  ply1mulgsumlem2  48700  linindslinci  48761  lindslinindsimp1  48770  lindslinindsimp2lem5  48775  lindslinindsimp2  48776  linds0  48778  lindsrng01  48781  snlindsntor  48784  lmod1  48805  ldepsnlinc  48821  bigoval  48862  elbigo2r  48866  nn0sumshdiglem2  48935  eenglngeehlnmlem1  49050  eenglngeehlnmlem2  49051  lubeldm2d  49270  glbeldm2d  49271  lubsscl  49272  glbsscl  49273  ipolubdm  49299  ipolub  49300  ipoglbdm  49302  ipoglb  49303  nelsubc3lem  49382  upfval2  49489  upfval3  49490  isthincd2lem2  49747  setc1onsubc  49914  cnelsubclem  49915  setrec1lem2  50000