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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939

This proof depends on definitions:  df-bi 210  df-an 401  df-ral 3079

This theorem is used by:  2ralbidv  3228  rexralbidv  3230  3ralbidv  3231  4ralbidv  3232  cbvral2vw  3246  cbvral4vw  3249  cbvral2v  3356  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  5369  reusv3  5375  poeq1  5571  solin  5595  somo  5607  frirr  5636  fr2nr  5637  frminex  5639  wereu2  5657  posn  5746  frsn  5748  ralxpf  5831  cnvpo  6288  reu3op  6293  reuop  6294  dfpo2  6297  frpomin  6341  fnmptfvd  7036  iinpreima  7064  dff4  7096  dff13f  7253  fpropnf1  7265  f1ounsn  7270  eusvobj2  7404  ovanraleqv  7436  f1opr  7468  ofreq  7680  sorpssuni  7731  sorpssint  7732  fr3nr  7769  onssmin  7789  funcnvuni  7927  f1oweALT  7967  frxp  8120  frxp2  8138  xpord2indlem  8141  frxp3  8145  xpord3inddlem  8148  poseq  8152  soseq  8153  frecseq123  8277  csbfrecsg  8279  frrlem1  8281  frrlem13  8293  smoeq  8335  tfrlem12  8374  tz7.48lem  8426  naddcllem  8660  naddov2  8663  naddunif  8678  naddasslem1  8679  naddasslem2  8680  elixp2  8897  undifixp  8930  xpf1o  9125  nneneq  9188  ac6sfi  9242  frfi  9243  fipreima  9313  indexfi  9315  marypha1lem  9391  marypha1  9392  supeq1  9403  supeq3  9407  supmo  9410  eqsup  9414  supub  9417  suplub  9418  sup0  9425  supisoex  9433  eqinf  9443  infval  9445  infmo  9455  oieq1  9472  ordtypecbv  9477  ordtypelem3  9480  ordtypelem6  9483  ordtypelem7  9484  ordtypelem9  9486  wemaplem1  9506  wemaplem2  9507  zfregcl  9554  zfregclOLD  9555  oemapval  9650  oemapvali  9651  cantnf  9660  wemapwe  9664  ttrcleq  9676  ttrcltr  9683  ttrclss  9687  ttrclselem2  9693  rankval3b  9796  unbndrank  9812  rankunb  9820  rankuni2b  9823  tcrank  9854  scottex  9860  scottexOLD  9861  scottexsOLD  9870  scott0bsOLD  9872  scottelrankd  9875  bnd2  9883  updjud  9927  dfac8clem  10023  ac5num  10027  acni  10036  acni2  10037  alephval3  10101  dfac4  10113  dfac5lem5  10118  dfac5  10119  dfac2a  10120  dfac2b  10121  dfacacn  10132  kmlem2  10142  kmlem13  10153  cflem  10235  cflecard  10242  cfeq0  10246  cfsuc  10247  cfflb  10249  cofsmo  10259  cfsmolem  10260  cfcoflem  10262  coftr  10263  alephsing  10266  fin23lem11  10307  isfin3ds  10319  fin23lem17  10328  fin23lem39  10340  isf33lem  10356  isf34lem6  10370  fin1a2lem13  10402  hsmexlem4  10419  hsmex  10422  axcc2lem  10426  axcc3  10428  dcomex  10437  axdc2lem  10438  axdc3lem2  10441  axdc3lem3  10442  axdc3  10444  axdc4lem  10445  axcclem  10447  zorn2lem2  10487  zorn2lem7  10492  zorn2g  10493  zornn0g  10495  ttukeylem7  10505  axdclem2  10510  brdom3  10518  brdom7disj  10521  brdom6disj  10522  alephval2  10563  inar1  10766  axgroth6  10819  pinq  10918  nqereu  10920  prlem934  11024  supexpr  11045  supsrlem  11102  axpre-sup  11160  dedekind  11379  dedekindle  11380  fiminre2  12169  lbreu  12171  sup2  12177  infm3  12180  nnsub  12286  uzwo  12941  nnwof  12944  ublbneg  12963  lbzbi  12966  zsupss  12967  uzsupss  12970  uzwo3  12973  zmax  12975  rpnnen1lem1  13008  rpnnen1lem3  13009  rpnnen1lem4  13010  rpnnen1lem5  13011  xrsupsslem  13339  xrinfmsslem  13340  xrsupss  13341  xrinfmss  13342  flval2  13854  axdc4uzlem  14026  ssnn0fi  14028  fsuppmapnn0fiubex  14035  faclbnd4lem4  14339  bccl  14365  hashgt12el  14466  hashbc  14497  hashge2el2dif  14524  wrdind  14766  wrd2ind  14767  rexanre  15405  rexico  15412  cau4  15415  reusq0  15523  clim  15552  rlim  15553  rlim2  15554  clim2  15562  clim2c  15563  clim0c  15565  rlim0  15566  rlim0lt  15567  ello12r  15575  ello1d  15581  elo12r  15586  rlimresb  15623  rlimcld2  15636  climabs0  15643  rlimo1  15675  lo1add  15685  lo1mul  15686  isercoll  15726  incexclem  15897  sqrt2irr  16311  gcdcllem1  16563  gcdcllem2  16564  dfgcd2  16610  fissn0dvds  16683  dvdslcmf  16695  lcmfledvds  16696  lcmf  16697  lcmfunsnlem1  16701  lcmfunsnlem2lem1  16702  lcmfunsnlem  16705  lcmfdvds  16706  reumodprminv  16870  pc2dvds  16945  pcz  16947  prmpwdvds  16970  infpn2  16979  prmreclem2  16983  prmreclem3  16984  prmreclem5  16986  prmreclem6  16987  vdwlem6  17052  vdwlem8  17054  vdwlem13  17059  vdwnnlem1  17061  vdwnn  17064  ramcl  17095  cshwrepswhash1  17168  prdsleval  17536  imasval  17571  imasaddfnlem  17588  imasvscafn  17597  mrisval  17692  isacs  17713  isacs2  17715  isacs1i  17719  mreacs  17720  acsfn  17721  acsfn2  17725  iscatd  17735  catidex  17736  catideu  17737  cidval  17739  catidd  17742  comfeq  17768  catpropd  17771  ismon  17796  isfunc  17927  isnat  18013  isinito  18059  istermo  18060  isprs  18358  drsdirfi  18367  ispos  18376  lubfval  18410  lubeldm  18413  lubval  18416  lubprop  18418  lublecllem  18420  glbfval  18423  glbeldm  18426  glbval  18429  glbprop  18431  joinval2lem  18440  joinlem  18443  meetval2lem  18454  meetlem  18457  poslubmo  18471  posglbmo  18472  poslubd  18473  resspos  18491  isglbd  18571  lubl  18574  lubun  18577  clatleglb  18580  isdlat  18584  ipodrsima  18603  chneq1  18674  mgm1  18722  gsumval2  18750  mgmhmima  18779  sgrp1  18793  mhmimalem  18889  mndind  18893  gsumwspan  18911  efmndmnd  18954  smndex1mnd  18978  sgrp2rid2  18994  sgrp2rid2ex  18995  sgrp2nmndlem4  18996  pwmnd  19005  dfgrp2  19035  isgrpinv  19066  grpidinv  19071  dfgrp3lem  19110  issubg4  19218  isnsg2  19228  nsgacs  19234  elnmz  19235  cycsubgcl  19283  ghmrn  19305  ghmnsgima  19316  isga  19367  orbsta  19389  cntzfval  19396  elcntz  19398  resscntz  19409  oppgsubg  19439  symgextfo  19498  gsmsymgreqlem2  19507  gsmsymgreq  19508  pmtrdifel  19556  pmtrdifwrdellem3  19559  pmtrdifwrdel2  19562  psgnunilem2  19571  psgnunilem3  19572  odeq  19626  gexid  19657  gexlem2  19658  gexdvds  19660  isslw  19684  sylow2alem1  19693  sylow2alem2  19694  efgval  19793  efgrelexlemb  19826  efgcpbllemb  19831  abl1  19942  dmdprd  20076  dprd2da  20120  pgpfac1lem5  20157  isomnd  20199  ring1  20400  rngisomring  20556  rhmval0  20564  lringuplu  20654  rhmimasubrnglem  20675  isrrg  20808  isabv  20925  islss  21066  lssacs  21099  reslmhm  21184  islbs  21208  pj1lmhm  21232  lbsacsbs  21291  rnglidlmcl  21352  rnglidl0  21366  rspprop  21381  prmidl  21476  zringlpir  21628  psgndiflemA  21762  ocvfval  21827  elocv  21829  iunocv  21842  frlmlbs  21958  islindf  21973  islinds2  21974  islindf2  21975  lindfrn  21982  lsslindf  21991  islindf4  21999  opsrval  22208  ply1coe  22469  cply1coe0bi  22473  mat0dimcrng  22638  mdetunilem1  22780  mdetunilem9  22788  cpmat  22877  cpmatel  22879  1elcpmat  22883  m2cpminvid2lem  22922  basgen2  23157  bastop1  23161  isclo  23255  ordtbaslem  23356  iscn  23403  cnpval  23404  iscnp  23405  iscnp3  23412  lmbr  23426  lmbr2  23427  lmbrf  23428  cnprest  23457  cnprest2  23458  t0sep  23492  isreg  23500  t1sep2  23537  tgcmp  23569  1stcclb  23612  1stcfb  23613  2ndc1stc  23619  1stcrest  23621  2ndcdisj  23624  islly  23636  isnlly  23637  lly1stc  23664  isref  23677  islocfin  23685  elkgen  23704  kgencn  23724  elpt  23740  elptr  23741  ptcnplem  23789  tx1stc  23818  cnmpt21  23839  kqt0lem  23904  isr0  23905  regr1lem2  23908  r0sep  23916  nrmr0reg  23917  flffbas  24163  cnflf  24170  cnflf2  24171  lmflf  24173  txflf  24174  fclsopni  24183  fclsnei  24187  fclsrest  24192  fcfnei  24203  cnfcf  24210  alexsubb  24214  alexsubALTlem3  24217  qustgplem  24289  tsmsfbas  24296  tsmsres  24312  tsmsf1o  24313  tsmsxplem1  24321  ustval  24371  isust  24372  ustincl  24376  ustdiag  24377  ustinvel  24378  ustexhalf  24379  ust0  24388  utopval  24400  ucnval  24444  isucn  24445  isucn2  24446  ucnima  24448  iscfilu  24455  ispsmet  24472  ismet  24491  isxmet  24492  imasdsf1olem  24541  imasf1oxmet  24543  imasf1omet  24544  metss  24676  met1stc  24689  prdsxmslem2  24697  txmetcnp  24715  metucn  24739  tngngp3  24824  nlmvscn  24855  nmoval  24883  nmolb  24885  qtopbaslem  24926  cncfval  25058  elcncf2  25060  mulc1cncf  25075  cncfmet  25079  evth  25129  lebnumlem3  25133  lebnum  25134  xlebnum  25135  ishtpy  25142  isphtpy  25151  pi1xfr  25225  pi1coghm  25231  isclmp  25267  ipcn  25416  lmmbr2  25429  lmmbr3  25430  lmmbrf  25432  cfilfval  25434  iscfil  25435  fmcfil  25442  caufval  25445  iscau  25446  iscau2  25447  iscau3  25448  iscau4  25449  iscauf  25450  caucfil  25453  cfilresi  25465  causs  25468  lmclim  25473  cmetcusp1  25523  minveclem4c  25595  minveclem2  25596  minveclem3b  25598  minveclem4  25602  minveclem6  25604  minveclem7  25605  ovolicc2lem3  25689  ismbl  25696  dyadmax  25768  dyadmbllem  25769  dyadmbl  25770  opnmbllem  25771  ismbf1  25794  ismbf  25798  mbfeqalem2  25812  mbflimsup  25836  mbfi1fseqlem6  25890  mbfi1flimlem  25892  itg2seq  25912  itg2monolem1  25920  isibl  25935  ply1divex  26305  fta1g  26338  dgrco  26443  plydivex  26469  fta1  26480  vieta1  26484  aannenlem1  26502  aannenlem2  26503  aalioulem2  26507  aalioulem3  26508  ulmval  26554  ulm2  26559  ulmi  26560  ulmres  26562  ulmshftlem  26563  ulmcaulem  26568  ulmcau  26569  ulmss  26571  ulmbdd  26572  ulmdvlem1  26574  ulmdvlem3  26576  pilem2  26626  pilem3  26627  cxpcn3  26924  dmarea  27133  rlimcnp  27141  scvxcvx  27161  lgamgulmlem2  27205  lgamgulmlem3  27206  lgamgulmlem5  27208  lgambdd  27212  lgamcvglem  27215  isppw2  27290  perfectlem2  27405  2sqlem6  27598  2sqlem10  27603  addsq2reu  27615  2sqreulem1  27621  2sqreunnlem1  27624  dchrisumlema  27663  dchrisumlem2  27665  dchrisumlem3  27666  pntpbnd  27763  pntibndlem3  27767  pntibnd  27768  pntleme  27783  pntlem3  27784  pntlemp  27785  pnt3  27787  ltsval  27822  nosupprefixmo  27875  noinfprefixmo  27876  nosupcbv  27877  nosupno  27878  nosupdm  27879  nosupfv  27881  nosupres  27882  nosupbnd1lem1  27883  nosupbnd1lem3  27885  nosupbnd1lem5  27887  noinfcbv  27892  noinfno  27893  noinfdm  27894  noinffv  27896  noinfres  27897  noinfbnd1lem3  27900  noinfbnd1lem5  27902  noetalem1  27916  noetalem2  27917  nocvxminlem  27958  brslts  27966  sltssnb  27973  conway  27983  etaslts  27997  lesrec  28003  eqcuts3  28008  madebdaylemlrcut  28103  madebday  28104  bdayle  28120  cofcutr  28128  cutmax  28138  cutmin  28139  lrrecfr  28147  addsprop  28180  negsunif  28259  addonbday  28483  onsfi  28560  n0subs  28567  bdayn0p1  28573  bdaypw2n0bndlem  28667  bdayfinbndlem2  28672  z12zsodd  28686  istrkgld  28739  axtg5seg  28745  tgcgr4  28811  perpln1  29001  perpln2  29002  isperp  29003  prlngmo2  29217  brbtwn2  29266  colinearalg  29271  axsegconlem1  29278  axsegcon  29288  ax5seglem4  29293  ax5seglem5  29294  axlowdim  29322  axeuclidlem  29323  axcontlem1  29325  axcontlem2  29326  axcontlem4  29328  axcontlem5  29329  axcontlem8  29332  axcontlem12  29336  elntg2  29346  uvtxusgr  29763  rgrx0ndm  29954  ewlksfval  29962  wksfval  29970  wwlks  30195  wlkiswwlks2  30235  clwwlk  30345  1conngr  30556  frgrwopregasn  30678  frgrwopregbsn  30679  frgrwopreglem5ALT  30684  frgrregord013  30757  isgrpo  30860  isgrpoi  30861  grpoideu  30872  grpoidinv2  30878  vciOLD  30924  isvclem  30940  cnidOLD  30945  isnvlem  30973  nvi  30977  lnoval  31115  islno  31116  isblo3i  31164  blo3i  31165  blocnilem  31167  ajfval  31172  ubthlem1  31233  ubthlem2  31234  ubthlem3  31235  ubth  31236  minvecolem2  31238  minvecolem3  31239  minvecolem4c  31242  minvecolem4  31243  minvecolem5  31244  minvecolem6  31245  minvecolem7  31246  h2hcau  31342  h2hlm  31343  hilid  31524  hcau  31547  hlimi  31551  hlim2  31555  ocel  31644  adjsym  32196  ellnop  32221  ellnfn  32246  hhcno  32267  hhcnf  32268  lnopeq  32372  elunop2  32376  lnophm  32382  lnconi  32396  lnopcnbd  32399  lnfncnbd  32420  imaelshi  32421  riesz3i  32425  riesz4i  32426  riesz4  32427  riesz1  32428  cnlnadjlem2  32431  cnlnadjlem5  32434  cnlnadjlem8  32437  cnlnadji  32439  nmopadjlei  32451  cnvbraval  32473  leopg  32485  leoppos  32489  mdbr  32657  dmdbr  32662  cdj3i  32804  disjunsn  32950  funcnv5mpt  33023  fgreu  33027  fcnvgreu  33028  xrge0infss  33116  wrdt2ind  33282  mgccole1  33319  mgccole2  33320  mgcmnt1  33321  mgcmnt2  33322  gsumhashmul  33396  isfxp  33497  fxpgaeq  33498  inftmrel  33509  isinftm  33510  archiabl  33527  isarchiofld  33528  elrgspnlem4  33574  0nellinds  33694  lindssn  33700  elrspunidl  33745  ismxidl  33754  1arithidom  33836  1arithufdlem3  33845  evl1deg1  33875  evl1deg2  33876  evl1deg3  33877  vietalem  33978  vieta  33979  crefeq  34244  zarcmplem  34280  esum2d  34492  sigaval  34510  issgon  34522  isrnmeas  34599  ismbfm  34650  mbfmcst  34658  elcarsg  34704  sitgval  34731  eulerpartlemd  34765  ballotleme  34896  tgoldbachgt  35059  bnj1185  35190  bnj1385  35229  bnj66  35257  bnj106  35265  bnj155  35276  bnj852  35318  bnj893  35325  bnj1228  35408  bnj1234  35410  bnj1463  35452  nummin  35493  rankfilimbi  35504  r1omhfb  35517  elscott  35519  fineqvnttrclse  35545  r1omhfbregs  35558  gblacfnacd  35594  onvf1odlem4  35598  vonf1wev  35600  vonf1owevOLD  35602  derangenlem  35671  subfacp1lem3  35682  subfacp1lem5  35684  subfacp1lem6  35685  subfacp1  35686  erdszelem8  35698  kur14  35716  cnpconn  35730  resconn  35746  cvmscbv  35758  iscvm  35759  cvmsi  35765  cvmsval  35766  cvmlift3lem2  35820  snmlval  35831  satfv1  35863  fmlasucdisj  35899  satffunlem1lem1  35902  satffunlem2lem1  35904  satfv1fvfmla1  35923  mclsssvlem  36062  mclsval  36063  mclsax  36069  mclsind  36070  dfon2lem9  36289  dfrdg2  36293  dfrdg3  36294  fwddifnval  36663  nmulprop  36690  ltnadd  36718  nn0prpwlem  36861  isfne  36878  isfne4  36879  isfne2  36881  isfne3  36882  neibastop3  36901  topmeet  36903  topjoin  36904  filnetlem4  36920  weiunlem  37002  weiunfrlem  37003  dfttc4lem1  37067  dfttc4  37069  elttcirr  37070  unblimceq0lem  37123  unblimceq0  37124  unbdqndv2  37128  taupilemrplb  37992  fin2so  38286  lindsadd  38292  matunitlindflem2  38296  ptrecube  38299  poimirlem2  38301  poimirlem3  38302  poimirlem4  38303  poimirlem24  38323  poimirlem25  38324  poimirlem26  38325  poimirlem27  38326  poimirlem28  38327  poimirlem29  38328  poimirlem30  38329  poimirlem32  38331  poimir  38332  heicant  38334  mblfinlem1  38336  mblfinlem2  38337  voliunnfl  38343  volsupnfl  38344  mbfresfi  38345  itg2addnc  38353  upixp  38408  indexdom  38413  filbcmb  38419  sdclem2  38421  fdc  38424  lmclim2  38437  caures  38439  istotbnd  38448  istotbnd3  38450  sstotbnd  38454  isbnd  38459  heibor  38500  bfp  38503  rrncmslem  38511  isgrpda  38634  idlval  38692  isidl  38693  0idl  38704  unichnidl  38710  pridl  38716  ismaxidl  38719  smprngopr  38731  igenval2  38745  prnc  38746  ispridlc  38749  scottexf  38845  scott0f  38846  disjsuc2  39091  riotasvd  39758  islfl  39862  eqlkr  39901  eqlkr3  39903  glbconN  40179  hlsuprexch  40183  ispsubsp  40547  ldilset  40911  isldil  40912  dilsetN  40955  isdilN  40956  trlset  40963  trlval  40964  cdleme27b  41170  cdleme29b  41177  cdleme31so  41181  cdleme31sn1  41183  cdleme31sn1c  41190  cdleme31fv  41192  cdleme40v  41271  istendo  41562  cdlemkid3N  41735  cdlemkid4  41736  cdlemkid5  41737  dihfval  42033  dihval  42034  islpolN  42285  hdmapffval  42628  hdmapfval  42629  hdmapval  42630  hdmapval2lem  42633  hgmapffval  42687  hgmapfval  42688  hgmapval  42689  hgmapvs  42693  isprimroot  42888  aks6d1c1p1  42902  hashscontpow1  42916  sticksstones2  42942  unitscyglem3  42992  exfinfldd  42998  qsalrel  43037  supinf  43038  sn-sup2  43293  fsuppind  43350  isnacs  43463  isnacs2  43465  nacsfix  43471  mzpclval  43484  elmzpcl  43485  rencldnfilem  43575  infmrgelbi  43633  pellfundre  43636  pellfundlb  43639  wepwsolem  43797  fnwe2lem2  43806  aomclem8  43816  dfac11  43817  gicabl  43854  islnr3  43870  hbtlem2  43879  hbtlem5  43883  onintunirab  43982  onsucf1lem  44024  cantnfresb  44079  safesnsupfilb  44172  rp-brsslt  44177  fiinfi  44327  clsk1independent  44800  ntrclsk13  44825  gneispacess2  44900  imo72b2lem0  44919  imo72b2lem2  44921  imo72b2lem1  44923  imo72b2  44926  mnuop23d  45004  ismnushort  45039  ralabsobidv  45709  0elaxnul  45720  pwclaxpow  45721  prclaxpr  45722  uniclaxun  45723  omssaxinf2  45725  modelac8prim  45729  wfac8prim  45739  permac8prim  45751  evth2f  45763  evthf  45775  fnchoice  45777  uzwo4  45801  wessf1ornlem  45931  disjinfi  45938  rnmptlb  45986  rnmptbdd  45988  rnmptbd2  45992  rnmptbd  45999  dstregt0  46029  upbdrech2  46055  rexabslelem  46160  rexabsle  46161  uzub  46173  infrpgernmpt  46207  mccl  46342  ellimcabssub0  46361  climf  46366  clim2f  46378  limsupre  46383  clim2cf  46392  clim0cf  46396  climf2  46408  clim2f2  46412  clim2d  46415  limsupref  46427  limsupbnd1f  46428  climinf2  46449  limsuppnf  46453  climinfmpt  46457  climinf3  46458  limsupubuzmpt  46461  limsupmnf  46463  limsupre2lem  46466  limsupre2  46467  limsupmnfuzlem  46468  limsupmnfuz  46469  limsupre2mpt  46472  limsupre3lem  46474  limsupre3  46475  limsupre3mpt  46476  limsupre3uz  46478  limsupreuz  46479  limsupreuzmpt  46481  climuz  46486  liminfreuzlem  46544  liminfreuz  46545  cnrefiisplem  46571  xlimmnfvlem1  46574  xlimmnfv  46576  xlimpnfvlem1  46578  xlimpnfv  46580  xlimmnfmpt  46585  xlimpnfmpt  46586  cncfshift  46616  cncfperiod  46621  fperdvper  46661  dvbdfbdioo  46672  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  dvnprodlem3  46690  stoweidlem5  46747  stoweidlem9  46751  stoweidlem15  46757  stoweidlem16  46758  stoweidlem27  46769  stoweidlem28  46770  stoweidlem31  46773  stoweidlem34  46776  stoweidlem37  46779  stoweidlem46  46788  stoweidlem48  46790  stoweidlem51  46793  stoweidlem52  46794  stoweidlem59  46801  wallispilem3  46809  stirlinglem13  46828  fourierdlem2  46851  fourierdlem3  46852  fourierdlem16  46865  fourierdlem20  46869  fourierdlem21  46870  fourierdlem22  46871  fourierdlem25  46874  fourierdlem39  46888  fourierdlem42  46891  fourierdlem54  46902  fourierdlem64  46912  fourierdlem77  46925  fourierdlem83  46931  fourierdlem103  46951  fourierdlem104  46952  subsaliuncllem  47099  iundjiun  47202  meaiunincf  47225  caragenval  47235  isome  47236  caragenel  47237  omessle  47240  ovnlerp  47304  hoidmvlelem3  47339  hoidmvle  47342  issmflem  47469  issmfgt  47498  smfmullem2  47534  smfmullem4  47536  smfmul  47537  smfsuplem2  47554  smfsup  47556  smfinflem  47559  smfinf  47560  fsupdm  47584  finfdm  47588  cfsetsnfsetf  47823  cbvral2  47868  2reu8i  47878  2reuimp0  47879  dfdfat2  47893  iccpart  48193  iccpartigtl  48200  paireqne  48288  reupr  48299  perfectALTVlem2  48515  bgoldbachlt  48606  tgoldbachlt  48609  grimidvtxedg  48678  grimcnv  48681  grimco  48682  isuspgrim0  48687  gricushgr  48710  ushggricedg  48720  uhgrimisgrgric  48724  isubgr3stgr  48768  isgrlim  48775  isgrlim2  48776  uspgrlim  48785  grlicsym  48806  grlictr  48808  gpg5nbgrvtx03star  48873  gpg5nbgr3star  48874  pgnbgreunbgr  48918  upwlksfval  48928  nn0mnd  48972  uzlidlring  49028  smprngprmrng  49132  ply1mulgsumlem1  49194  ply1mulgsumlem2  49195  linindslinci  49256  lindslinindsimp1  49265  lindslinindsimp2lem5  49270  lindslinindsimp2  49271  linds0  49273  lindsrng01  49276  snlindsntor  49279  lmod1  49300  ldepsnlinc  49316  bigoval  49357  elbigo2r  49361  nn0sumshdiglem2  49430  eenglngeehlnmlem1  49545  eenglngeehlnmlem2  49546  lubeldm2d  49764  glbeldm2d  49765  lubsscl  49766  glbsscl  49767  ipolubdm  49793  ipolub  49794  ipoglbdm  49796  ipoglb  49797  nelsubc3lem  49876  upfval2  49983  upfval3  49984  isthincd2lem2  50241  setc1onsubc  50408  cnelsubclem  50409  setrec1lem2  50494