Theorem ralbidv 3186

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2141  ∀wral 3077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3078

This theorem is referenced by:  2ralbidv  3227  rexralbidv  3229  3ralbidv  3230  4ralbidv  3231  cbvral2vw  3245  cbvral4vw  3248  cbvral2v  3355  rspceaimv  3586  rspc2  3589  rspc2v  3591  rspc3v  3596  rspc4v  3600  reu6i  3690  reu7  3694  sbcralt  3824  reu8nf  3829  raaan  4478  raaanv  4479  raaan2  4482  2reu4lem  4483  reusngf  4639  2ralsng  4643  rexreusng  4644  reuprg0  4667  issn  4796  2ralunsn  4859  elintg  4919  elintrabg  4925  eliin  4960  disjprg  5104  disjxun  5106  brralrspcev  5170  reusv2lem2  5370  reusv3  5376  poeq1  5572  solin  5596  somo  5608  frirr  5637  fr2nr  5638  frminex  5640  wereu2  5658  posn  5747  frsn  5749  ralxpf  5832  cnvpo  6288  reu3op  6293  reuop  6294  dfpo2  6297  frpomin  6341  fnmptfvd  7036  iinpreima  7064  dff4  7096  dff13f  7253  fpropnf1  7265  f1ounsn  7270  eusvobj2  7402  ovanraleqv  7434  f1opr  7466  ofreq  7678  sorpssuni  7729  sorpssint  7730  fr3nr  7770  onssmin  7790  funcnvuni  7928  f1oweALT  7968  frxp  8121  frxp2  8139  xpord2indlem  8142  frxp3  8146  xpord3inddlem  8149  poseq  8153  soseq  8154  frecseq123  8278  csbfrecsg  8280  frrlem1  8282  frrlem13  8294  smoeq  8336  tfrlem12  8375  tz7.48lem  8427  naddcllem  8661  naddov2  8664  naddunif  8679  naddasslem1  8680  naddasslem2  8681  elixp2  8898  undifixp  8931  xpf1o  9126  nneneq  9189  ac6sfi  9243  frfi  9244  fipreima  9314  indexfi  9316  marypha1lem  9392  marypha1  9393  supeq1  9404  supeq3  9408  supmo  9411  eqsup  9415  supub  9418  suplub  9419  sup0  9426  supisoex  9434  eqinf  9444  infval  9446  infmo  9456  oieq1  9473  ordtypecbv  9478  ordtypelem3  9481  ordtypelem6  9484  ordtypelem7  9485  ordtypelem9  9487  wemaplem1  9507  wemaplem2  9508  zfregcl  9555  zfregclOLD  9556  oemapval  9651  oemapvali  9652  cantnf  9661  wemapwe  9665  ttrcleq  9677  ttrcltr  9684  ttrclss  9688  ttrclselem2  9694  rankval3b  9797  unbndrank  9813  rankunb  9821  rankuni2b  9824  tcrank  9855  scottex  9858  scottexs  9860  scott0s  9861  scottelrankd  9872  bnd2  9878  updjud  9919  dfac8clem  10015  ac5num  10019  acni  10028  acni2  10029  alephval3  10093  dfac4  10105  dfac5lem5  10110  dfac5  10111  dfac2a  10112  dfac2b  10113  dfacacn  10124  kmlem2  10134  kmlem13  10145  cflem  10227  cflemOLD  10228  cflecard  10235  cfeq0  10239  cfsuc  10240  cfflb  10242  cofsmo  10252  cfsmolem  10253  cfcoflem  10255  coftr  10256  alephsing  10259  fin23lem11  10300  isfin3ds  10312  fin23lem17  10321  fin23lem39  10333  isf33lem  10349  isf34lem6  10363  fin1a2lem13  10395  hsmexlem4  10412  hsmex  10415  axcc2lem  10419  axcc3  10421  dcomex  10430  axdc2lem  10431  axdc3lem2  10434  axdc3lem3  10435  axdc3  10437  axdc4lem  10438  axcclem  10440  zorn2lem2  10480  zorn2lem7  10485  zorn2g  10486  zornn0g  10488  ttukeylem7  10498  axdclem2  10503  brdom3  10511  brdom7disj  10514  brdom6disj  10515  alephval2  10556  inar1  10759  axgroth6  10812  pinq  10911  nqereu  10913  prlem934  11017  supexpr  11038  supsrlem  11095  axpre-sup  11153  dedekind  11372  dedekindle  11373  fiminre2  12162  lbreu  12164  sup2  12170  infm3  12173  nnsub  12279  uzwo  12934  nnwof  12937  ublbneg  12956  lbzbi  12959  zsupss  12960  uzsupss  12963  uzwo3  12966  zmax  12968  rpnnen1lem1  13001  rpnnen1lem3  13002  rpnnen1lem4  13003  rpnnen1lem5  13004  xrsupsslem  13332  xrinfmsslem  13333  xrsupss  13334  xrinfmss  13335  flval2  13846  axdc4uzlem  14018  ssnn0fi  14020  fsuppmapnn0fiubex  14027  faclbnd4lem4  14331  bccl  14357  hashgt12el  14458  hashbc  14489  hashge2el2dif  14516  wrdind  14758  wrd2ind  14759  rexanre  15397  rexico  15404  cau4  15407  reusq0  15515  clim  15544  rlim  15545  rlim2  15546  clim2  15554  clim2c  15555  clim0c  15557  rlim0  15558  rlim0lt  15559  ello12r  15567  ello1d  15573  elo12r  15578  rlimresb  15615  rlimcld2  15628  climabs0  15635  rlimo1  15667  lo1add  15677  lo1mul  15678  isercoll  15718  incexclem  15889  sqrt2irr  16304  gcdcllem1  16556  gcdcllem2  16557  dfgcd2  16603  fissn0dvds  16676  dvdslcmf  16688  lcmfledvds  16689  lcmf  16690  lcmfunsnlem1  16694  lcmfunsnlem2lem1  16695  lcmfunsnlem  16698  lcmfdvds  16699  reumodprminv  16863  pc2dvds  16938  pcz  16940  prmpwdvds  16963  infpn2  16972  prmreclem2  16976  prmreclem3  16977  prmreclem5  16979  prmreclem6  16980  vdwlem6  17045  vdwlem8  17047  vdwlem13  17052  vdwnnlem1  17054  vdwnn  17057  ramcl  17088  cshwrepswhash1  17161  prdsleval  17529  imasval  17564  imasaddfnlem  17581  imasvscafn  17590  mrisval  17685  isacs  17706  isacs2  17708  isacs1i  17712  mreacs  17713  acsfn  17714  acsfn2  17718  iscatd  17728  catidex  17729  catideu  17730  cidval  17732  catidd  17735  comfeq  17761  catpropd  17764  ismon  17789  isfunc  17920  isnat  18006  isinito  18052  istermo  18053  isprs  18351  drsdirfi  18360  ispos  18369  lubfval  18403  lubeldm  18406  lubval  18409  lubprop  18411  lublecllem  18413  glbfval  18416  glbeldm  18419  glbval  18422  glbprop  18424  joinval2lem  18433  joinlem  18436  meetval2lem  18447  meetlem  18450  poslubmo  18464  posglbmo  18465  poslubd  18466  resspos  18484  isglbd  18564  lubl  18567  lubun  18570  clatleglb  18573  isdlat  18577  ipodrsima  18596  chneq1  18667  mgm1  18715  gsumval2  18743  mgmhmima  18772  sgrp1  18786  mhmimalem  18882  mndind  18886  gsumwspan  18904  efmndmnd  18947  smndex1mnd  18971  sgrp2rid2  18987  sgrp2rid2ex  18988  sgrp2nmndlem4  18989  pwmnd  18998  dfgrp2  19028  isgrpinv  19059  grpidinv  19064  dfgrp3lem  19103  issubg4  19211  isnsg2  19221  nsgacs  19227  elnmz  19228  cycsubgcl  19276  ghmrn  19298  ghmnsgima  19309  isga  19360  orbsta  19382  cntzfval  19389  elcntz  19391  resscntz  19402  oppgsubg  19432  symgextfo  19491  gsmsymgreqlem2  19500  gsmsymgreq  19501  pmtrdifel  19549  pmtrdifwrdellem3  19552  pmtrdifwrdel2  19555  psgnunilem2  19564  psgnunilem3  19565  odeq  19619  gexid  19650  gexlem2  19651  gexdvds  19653  isslw  19677  sylow2alem1  19686  sylow2alem2  19687  efgval  19786  efgrelexlemb  19819  efgcpbllemb  19824  abl1  19935  dmdprd  20069  dprd2da  20113  pgpfac1lem5  20150  isomnd  20192  ring1  20392  rngisomring  20548  lringuplu  20628  rhmimasubrnglem  20649  isrrg  20782  isabv  20893  islss  21034  lssacs  21067  reslmhm  21152  islbs  21176  pj1lmhm  21200  lbsacsbs  21259  rnglidlmcl  21320  rnglidl0  21334  rspprop  21349  prmidl  21444  zringlpir  21596  psgndiflemA  21730  ocvfval  21795  elocv  21797  iunocv  21810  frlmlbs  21926  islindf  21941  islinds2  21942  islindf2  21943  lindfrn  21950  lsslindf  21959  islindf4  21967  opsrval  22176  ply1coe  22437  cply1coe0bi  22441  mat0dimcrng  22606  mdetunilem1  22748  mdetunilem9  22756  cpmat  22845  cpmatel  22847  1elcpmat  22851  m2cpminvid2lem  22890  basgen2  23125  bastop1  23129  isclo  23223  ordtbaslem  23324  iscn  23371  cnpval  23372  iscnp  23373  iscnp3  23380  lmbr  23394  lmbr2  23395  lmbrf  23396  cnprest  23425  cnprest2  23426  t0sep  23460  isreg  23468  t1sep2  23505  tgcmp  23537  1stcclb  23580  1stcfb  23581  2ndc1stc  23587  1stcrest  23589  2ndcdisj  23592  islly  23604  isnlly  23605  lly1stc  23632  isref  23645  islocfin  23653  elkgen  23672  kgencn  23692  elpt  23708  elptr  23709  ptcnplem  23757  tx1stc  23786  cnmpt21  23807  kqt0lem  23872  isr0  23873  regr1lem2  23876  r0sep  23884  nrmr0reg  23885  flffbas  24131  cnflf  24138  cnflf2  24139  lmflf  24141  txflf  24142  fclsopni  24151  fclsnei  24155  fclsrest  24160  fcfnei  24171  cnfcf  24178  alexsubb  24182  alexsubALTlem3  24185  qustgplem  24257  tsmsfbas  24264  tsmsres  24280  tsmsf1o  24281  tsmsxplem1  24289  ustval  24339  isust  24340  ustincl  24344  ustdiag  24345  ustinvel  24346  ustexhalf  24347  ust0  24356  utopval  24368  ucnval  24412  isucn  24413  isucn2  24414  ucnima  24416  iscfilu  24423  ispsmet  24440  ismet  24459  isxmet  24460  imasdsf1olem  24509  imasf1oxmet  24511  imasf1omet  24512  metss  24644  met1stc  24657  prdsxmslem2  24665  txmetcnp  24683  metucn  24707  tngngp3  24792  nlmvscn  24823  nmoval  24851  nmolb  24853  qtopbaslem  24894  cncfval  25026  elcncf2  25028  mulc1cncf  25043  cncfmet  25047  evth  25097  lebnumlem3  25101  lebnum  25102  xlebnum  25103  ishtpy  25110  isphtpy  25119  pi1xfr  25193  pi1coghm  25199  isclmp  25235  ipcn  25384  lmmbr2  25397  lmmbr3  25398  lmmbrf  25400  cfilfval  25402  iscfil  25403  fmcfil  25410  caufval  25413  iscau  25414  iscau2  25415  iscau3  25416  iscau4  25417  iscauf  25418  caucfil  25421  cfilresi  25433  causs  25436  lmclim  25441  cmetcusp1  25491  minveclem4c  25563  minveclem2  25564  minveclem3b  25566  minveclem4  25570  minveclem6  25572  minveclem7  25573  ovolicc2lem3  25657  ismbl  25664  dyadmax  25736  dyadmbllem  25737  dyadmbl  25738  opnmbllem  25739  ismbf1  25762  ismbf  25766  mbfeqalem2  25780  mbflimsup  25804  mbfi1fseqlem6  25858  mbfi1flimlem  25860  itg2seq  25880  itg2monolem1  25888  isibl  25903  ply1divex  26273  fta1g  26306  dgrco  26411  plydivex  26437  fta1  26448  vieta1  26452  aannenlem1  26468  aannenlem2  26469  aalioulem2  26473  aalioulem3  26474  ulmval  26519  ulm2  26524  ulmi  26525  ulmres  26527  ulmshftlem  26528  ulmcaulem  26533  ulmcau  26534  ulmss  26536  ulmbdd  26537  ulmdvlem1  26539  ulmdvlem3  26541  pilem2  26591  pilem3  26592  cxpcn3  26889  dmarea  27098  rlimcnp  27106  scvxcvx  27126  lgamgulmlem2  27170  lgamgulmlem3  27171  lgamgulmlem5  27173  lgambdd  27177  lgamcvglem  27180  isppw2  27255  perfectlem2  27370  2sqlem6  27563  2sqlem10  27568  addsq2reu  27580  2sqreulem1  27586  2sqreunnlem1  27589  dchrisumlema  27628  dchrisumlem2  27630  dchrisumlem3  27631  pntpbnd  27728  pntibndlem3  27732  pntibnd  27733  pntleme  27748  pntlem3  27749  pntlemp  27750  pnt3  27752  ltsval  27787  nosupprefixmo  27840  noinfprefixmo  27841  nosupcbv  27842  nosupno  27843  nosupdm  27844  nosupfv  27846  nosupres  27847  nosupbnd1lem1  27848  nosupbnd1lem3  27850  nosupbnd1lem5  27852  noinfcbv  27857  noinfno  27858  noinfdm  27859  noinffv  27861  noinfres  27862  noinfbnd1lem3  27865  noinfbnd1lem5  27867  noetalem1  27881  noetalem2  27882  nocvxminlem  27923  brslts  27931  sltssnb  27938  conway  27948  etaslts  27962  lesrec  27968  eqcuts3  27973  madebdaylemlrcut  28068  madebday  28069  bdayle  28085  cofcutr  28093  cutmax  28103  cutmin  28104  lrrecfr  28112  addsprop  28145  negsunif  28224  addonbday  28448  onsfi  28525  n0subs  28532  bdayn0p1  28538  bdaypw2n0bndlem  28632  bdayfinbndlem2  28637  z12zsodd  28651  istrkgld  28704  axtg5seg  28710  tgcgr4  28776  perpln1  28965  perpln2  28966  isperp  28967  prlngmo2  29179  brbtwn2  29221  colinearalg  29226  axsegconlem1  29233  axsegcon  29243  ax5seglem4  29248  ax5seglem5  29249  axlowdim  29277  axeuclidlem  29278  axcontlem1  29280  axcontlem2  29281  axcontlem4  29283  axcontlem5  29284  axcontlem8  29287  axcontlem12  29291  elntg2  29301  uvtxusgr  29718  rgrx0ndm  29909  ewlksfval  29917  wksfval  29925  wwlks  30150  wlkiswwlks2  30190  clwwlk  30300  1conngr  30511  frgrwopregasn  30633  frgrwopregbsn  30634  frgrwopreglem5ALT  30639  frgrregord013  30712  isgrpo  30815  isgrpoi  30816  grpoideu  30827  grpoidinv2  30833  vciOLD  30879  isvclem  30895  cnidOLD  30900  isnvlem  30928  nvi  30932  lnoval  31070  islno  31071  isblo3i  31119  blo3i  31120  blocnilem  31122  ajfval  31127  ubthlem1  31188  ubthlem2  31189  ubthlem3  31190  ubth  31191  minvecolem2  31193  minvecolem3  31194  minvecolem4c  31197  minvecolem4  31198  minvecolem5  31199  minvecolem6  31200  minvecolem7  31201  h2hcau  31297  h2hlm  31298  hilid  31479  hcau  31502  hlimi  31506  hlim2  31510  ocel  31599  adjsym  32151  ellnop  32176  ellnfn  32201  hhcno  32222  hhcnf  32223  lnopeq  32327  elunop2  32331  lnophm  32337  lnconi  32351  lnopcnbd  32354  lnfncnbd  32375  imaelshi  32376  riesz3i  32380  riesz4i  32381  riesz4  32382  riesz1  32383  cnlnadjlem2  32386  cnlnadjlem5  32389  cnlnadjlem8  32392  cnlnadji  32394  nmopadjlei  32406  cnvbraval  32428  leopg  32440  leoppos  32444  mdbr  32612  dmdbr  32617  cdj3i  32759  disjunsn  32905  funcnv5mpt  32978  fgreu  32982  fcnvgreu  32983  xrge0infss  33071  wrdt2ind  33239  mgccole1  33276  mgccole2  33277  mgcmnt1  33278  mgcmnt2  33279  gsumhashmul  33353  isfxp  33454  fxpgaeq  33455  inftmrel  33466  isinftm  33467  archiabl  33484  isarchiofld  33485  elrgspnlem4  33531  0nellinds  33651  lindssn  33657  elrspunidl  33702  ismxidl  33711  1arithidom  33793  1arithufdlem3  33802  evl1deg1  33832  evl1deg2  33833  evl1deg3  33834  vietalem  33935  vieta  33936  crefeq  34201  zarcmplem  34237  esum2d  34449  sigaval  34467  issgon  34479  isrnmeas  34556  ismbfm  34607  mbfmcst  34615  elcarsg  34661  sitgval  34688  eulerpartlemd  34722  ballotleme  34853  tgoldbachgt  35016  bnj1185  35147  bnj1385  35186  bnj66  35214  bnj106  35222  bnj155  35233  bnj852  35275  bnj893  35282  bnj1228  35365  bnj1234  35367  bnj1463  35409  nummin  35448  rankfilimbi  35459  r1omhfb  35470  elscott  35472  fineqvnttrclse  35491  r1omhfbregs  35504  gblacfnacd  35540  onvf1odlem4  35544  vonf1wev  35546  vonf1owevOLD  35548  derangenlem  35617  subfacp1lem3  35628  subfacp1lem5  35630  subfacp1lem6  35631  subfacp1  35632  erdszelem8  35644  kur14  35662  cnpconn  35676  resconn  35692  cvmscbv  35704  iscvm  35705  cvmsi  35711  cvmsval  35712  cvmlift3lem2  35766  snmlval  35777  satfv1  35809  fmlasucdisj  35845  satffunlem1lem1  35848  satffunlem2lem1  35850  satfv1fvfmla1  35869  mclsssvlem  36008  mclsval  36009  mclsax  36015  mclsind  36016  dfon2lem9  36235  dfrdg2  36239  dfrdg3  36240  fwddifnval  36609  nmulprop  36636  nn0prpwlem  36777  isfne  36794  isfne4  36795  isfne2  36797  isfne3  36798  neibastop3  36817  topmeet  36819  topjoin  36820  filnetlem4  36836  weiunlem  36918  weiunfrlem  36919  dfttc4lem1  36983  dfttc4  36985  elttcirr  36986  unblimceq0lem  37039  unblimceq0  37040  unbdqndv2  37044  taupilemrplb  37908  fin2so  38202  lindsadd  38208  matunitlindflem2  38212  ptrecube  38215  poimirlem2  38217  poimirlem3  38218  poimirlem4  38219  poimirlem24  38239  poimirlem25  38240  poimirlem26  38241  poimirlem27  38242  poimirlem28  38243  poimirlem29  38244  poimirlem30  38245  poimirlem32  38247  poimir  38248  heicant  38250  mblfinlem1  38252  mblfinlem2  38253  voliunnfl  38259  volsupnfl  38260  mbfresfi  38261  itg2addnc  38269  upixp  38324  indexdom  38329  filbcmb  38335  sdclem2  38337  fdc  38340  lmclim2  38353  caures  38355  istotbnd  38364  istotbnd3  38366  sstotbnd  38370  isbnd  38375  heibor  38416  bfp  38419  rrncmslem  38427  isgrpda  38550  idlval  38608  isidl  38609  0idl  38620  unichnidl  38626  pridl  38632  ismaxidl  38635  smprngopr  38647  igenval2  38661  prnc  38662  ispridlc  38665  scottexf  38763  scott0f  38764  disjsuc2  39009  riotasvd  39676  islfl  39780  eqlkr  39819  eqlkr3  39821  glbconN  40097  hlsuprexch  40101  ispsubsp  40465  ldilset  40829  isldil  40830  dilsetN  40873  isdilN  40874  trlset  40881  trlval  40882  cdleme27b  41088  cdleme29b  41095  cdleme31so  41099  cdleme31sn1  41101  cdleme31sn1c  41108  cdleme31fv  41110  cdleme40v  41189  istendo  41480  cdlemkid3N  41653  cdlemkid4  41654  cdlemkid5  41655  dihfval  41951  dihval  41952  islpolN  42203  hdmapffval  42546  hdmapfval  42547  hdmapval  42548  hdmapval2lem  42551  hgmapffval  42605  hgmapfval  42606  hgmapval  42607  hgmapvs  42611  isprimroot  42806  aks6d1c1p1  42820  hashscontpow1  42834  sticksstones2  42860  unitscyglem3  42910  exfinfldd  42916  qsalrel  42955  supinf  42956  sn-sup2  43211  fsuppind  43270  isnacs  43383  isnacs2  43385  nacsfix  43391  mzpclval  43404  elmzpcl  43405  rencldnfilem  43495  infmrgelbi  43553  pellfundre  43556  pellfundlb  43559  wepwsolem  43717  fnwe2lem2  43726  aomclem8  43736  dfac11  43737  gicabl  43774  islnr3  43790  hbtlem2  43799  hbtlem5  43803  onintunirab  43902  onsucf1lem  43944  cantnfresb  43999  safesnsupfilb  44092  rp-brsslt  44097  fiinfi  44247  clsk1independent  44720  ntrclsk13  44745  gneispacess2  44820  imo72b2lem0  44839  imo72b2lem2  44841  imo72b2lem1  44843  imo72b2  44846  mnuop23d  44924  ismnushort  44959  ralabsobidv  45629  0elaxnul  45640  pwclaxpow  45641  prclaxpr  45642  uniclaxun  45643  omssaxinf2  45645  modelac8prim  45649  wfac8prim  45659  permac8prim  45671  evth2f  45683  evthf  45695  fnchoice  45697  uzwo4  45721  wessf1ornlem  45851  disjinfi  45858  rnmptlb  45906  rnmptbdd  45908  rnmptbd2  45912  rnmptbd  45919  dstregt0  45949  upbdrech2  45975  rexabslelem  46080  rexabsle  46081  uzub  46093  infrpgernmpt  46127  mccl  46262  ellimcabssub0  46281  climf  46286  clim2f  46298  limsupre  46303  clim2cf  46312  clim0cf  46316  climf2  46328  clim2f2  46332  clim2d  46335  limsupref  46347  limsupbnd1f  46348  climinf2  46369  limsuppnf  46373  climinfmpt  46377  climinf3  46378  limsupubuzmpt  46381  limsupmnf  46383  limsupre2lem  46386  limsupre2  46387  limsupmnfuzlem  46388  limsupmnfuz  46389  limsupre2mpt  46392  limsupre3lem  46394  limsupre3  46395  limsupre3mpt  46396  limsupre3uz  46398  limsupreuz  46399  limsupreuzmpt  46401  climuz  46406  liminfreuzlem  46464  liminfreuz  46465  cnrefiisplem  46491  xlimmnfvlem1  46494  xlimmnfv  46496  xlimpnfvlem1  46498  xlimpnfv  46500  xlimmnfmpt  46505  xlimpnfmpt  46506  cncfshift  46536  cncfperiod  46541  fperdvper  46581  dvbdfbdioo  46592  ioodvbdlimc1lem2  46594  ioodvbdlimc2lem  46596  dvnprodlem3  46610  stoweidlem5  46667  stoweidlem9  46671  stoweidlem15  46677  stoweidlem16  46678  stoweidlem27  46689  stoweidlem28  46690  stoweidlem31  46693  stoweidlem34  46696  stoweidlem37  46699  stoweidlem46  46708  stoweidlem48  46710  stoweidlem51  46713  stoweidlem52  46714  stoweidlem59  46721  wallispilem3  46729  stirlinglem13  46748  fourierdlem2  46771  fourierdlem3  46772  fourierdlem16  46785  fourierdlem20  46789  fourierdlem21  46790  fourierdlem22  46791  fourierdlem25  46794  fourierdlem39  46808  fourierdlem42  46811  fourierdlem54  46822  fourierdlem64  46832  fourierdlem77  46845  fourierdlem83  46851  fourierdlem103  46871  fourierdlem104  46872  subsaliuncllem  47019  iundjiun  47122  meaiunincf  47145  caragenval  47155  isome  47156  caragenel  47157  omessle  47160  ovnlerp  47224  hoidmvlelem3  47259  hoidmvle  47262  issmflem  47389  issmfgt  47418  smfmullem2  47454  smfmullem4  47456  smfmul  47457  smfsuplem2  47474  smfsup  47476  smfinflem  47479  smfinf  47480  fsupdm  47504  finfdm  47508  cfsetsnfsetf  47740  cbvral2  47785  2reu8i  47795  2reuimp0  47796  dfdfat2  47810  iccpart  48110  iccpartigtl  48117  paireqne  48205  reupr  48216  perfectALTVlem2  48432  bgoldbachlt  48523  tgoldbachlt  48526  grimidvtxedg  48595  grimcnv  48598  grimco  48599  isuspgrim0  48604  gricushgr  48627  ushggricedg  48637  uhgrimisgrgric  48641  isubgr3stgr  48685  isgrlim  48692  isgrlim2  48693  uspgrlim  48702  grlicsym  48723  grlictr  48725  gpg5nbgrvtx03star  48790  gpg5nbgr3star  48791  pgnbgreunbgr  48835  upwlksfval  48845  nn0mnd  48889  uzlidlring  48945  smprngprmrng  49049  ply1mulgsumlem1  49111  ply1mulgsumlem2  49112  linindslinci  49173  lindslinindsimp1  49182  lindslinindsimp2lem5  49187  lindslinindsimp2  49188  linds0  49190  lindsrng01  49193  snlindsntor  49196  lmod1  49217  ldepsnlinc  49233  bigoval  49274  elbigo2r  49278  nn0sumshdiglem2  49347  eenglngeehlnmlem1  49462  eenglngeehlnmlem2  49463  lubeldm2d  49681  glbeldm2d  49682  lubsscl  49683  glbsscl  49684  ipolubdm  49710  ipolub  49711  ipoglbdm  49713  ipoglb  49714  nelsubc3lem  49793  upfval2  49900  upfval3  49901  isthincd2lem2  50158  setc1onsubc  50325  cnelsubclem  50326  setrec1lem2  50411