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

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

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 3078

This theorem is used by:  2ralbidv  3227  rexralbidv  3229  3ralbidv  3230  4ralbidv  3231  cbvral2vw  3245  cbvral4vw  3248  cbvral2v  3354  rspceaimv  3583  rspc2  3585  rspc2v  3587  rspc3v  3592  rspc4v  3596  reu6i  3686  reu7  3690  sbcralt  3819  reu8nf  3824  raaan  4474  raaanv  4475  raaan2  4478  2reu4lem  4479  reusngf  4635  2ralsng  4639  rexreusng  4640  reuprg0  4663  issn  4792  2ralunsn  4855  elintg  4915  elintrabg  4921  eliin  4956  disjprg  5099  disjxun  5101  brralrspcev  5165  reusv2lem2  5361  reusv3  5367  poeq1  5562  solin  5586  somo  5598  frirr  5627  fr2nr  5628  frminex  5630  wereu2  5648  posn  5737  frsn  5739  ralxpf  5824  cnvpo  6290  reu3op  6295  reuop  6296  dfpo2  6299  frpomin  6343  fnmptfvd  7040  iinpreima  7069  dff4  7101  dff13f  7259  fpropnf1  7271  f1ounsn  7280  eusvobj2  7412  ovanraleqv  7444  f1opr  7476  ofreq  7697  sorpssuni  7748  sorpssint  7749  fr3nr  7786  onssmin  7806  funcnvuni  7944  f1oweALT  7984  frxp  8138  fnwe2lem3  8147  frxp2  8161  xpord2indlem  8164  frxp3  8168  xpord3inddlem  8171  poseq  8175  soseq  8176  frecseq123  8300  csbfrecsg  8302  frrlem1  8304  frrlem13  8316  smoeq  8358  tfrlem12  8397  tz7.48lemOLD  8451  naddcllem  8685  naddov2  8688  naddunif  8703  naddasslem1  8704  naddasslem2  8705  elixp2  8929  undifixp  8962  xpf1o  9158  nneneq  9221  ac6sfi  9275  frfi  9276  fipreima  9347  indexfi  9349  marypha1lem  9425  marypha1  9426  supeq1  9437  supeq3  9441  supmo  9444  eqsup  9448  supub  9451  suplub  9452  sup0  9459  supisoex  9467  eqinf  9477  infval  9479  infmo  9489  oieq1  9506  ordtypecbv  9511  ordtypelem3  9514  ordtypelem6  9517  ordtypelem7  9518  ordtypelem9  9520  wemaplem1  9540  wemaplem2  9541  zfregcl  9588  zfregclOLD  9589  oemapval  9684  oemapvali  9685  cantnf  9694  wemapwe  9698  ttrcleq  9710  ttrcltr  9717  ttrclss  9721  ttrclselem2  9727  rankval3b  9836  unbndrank  9855  rankunb  9864  rankuni2b  9867  tcrank  9901  rankfilimbi  9902  scottex  9933  scottexOLD  9934  scottexsOLD  9943  scott0bsOLD  9945  scottelrankd  9948  bnd2  9956  setrec1lem2  9967  updjud  10015  dfac8clem  10111  ac5num  10115  acni  10124  acni2  10125  alephval3  10189  dfac4  10201  dfac5lem5  10206  dfac5  10207  dfac2a  10208  dfac2b  10209  dfacacn  10220  kmlem2  10230  kmlem13  10241  cflem  10323  cflecard  10330  cfeq0  10334  cfsuc  10335  cfflb  10337  cofsmo  10347  cfsmolem  10348  cfcoflem  10350  coftr  10351  alephsing  10354  fin23lem11  10395  isfin3ds  10407  fin23lem17  10416  fin23lem39  10428  isf33lem  10444  isf34lem6  10458  fin1a2lem13  10490  hsmexlem4  10507  hsmex  10510  axcc2lem  10514  axcc3  10516  dcomex  10525  axdc2lem  10526  axdc3lem2  10529  axdc3lem3  10530  axdc3  10532  axdc4lem  10533  axcclem  10535  zorn2lem2  10575  zorn2lem7  10580  zorn2g  10581  zornn0g  10583  ttukeylem7  10593  axdclem2  10598  brdom3  10607  brdom7disj  10610  brdom6disj  10611  alephval2  10657  inar1  10860  axgroth6  10913  pinq  11012  nqereu  11014  prlem934  11118  supexpr  11139  supsrlem  11196  axpre-sup  11254  dedekind  11473  dedekindle  11474  fiminre2  12265  lbreu  12267  sup2  12273  infm3  12276  nnsub  12382  uzwo  13038  nnwof  13041  ublbneg  13060  lbzbi  13063  zsupss  13064  uzsupss  13067  uzwo3  13070  zmax  13072  rpnnen1lem1  13106  rpnnen1lem3  13107  rpnnen1lem4  13108  rpnnen1lem5  13109  xrsupsslem  13437  xrinfmsslem  13438  xrsupss  13439  xrinfmss  13440  flval2  13954  axdc4uzlem  14126  ssnn0fi  14128  fsuppmapnn0fiubex  14135  faclbnd4lem4  14440  bccl  14466  hashgt12el  14567  hashbc  14598  hashge2el2dif  14625  wrdind  14871  wrd2ind  14872  rexanre  15514  rexico  15521  cau4  15524  reusq0  15632  clim  15661  rlim  15662  rlim2  15663  clim2  15671  clim2c  15672  clim0c  15674  rlim0  15675  rlim0lt  15676  ello12r  15684  ello1d  15690  elo12r  15695  rlimresb  15732  rlimcld2  15745  climabs0  15752  rlimo1  15784  lo1add  15794  lo1mul  15795  isercoll  15835  incexclem  16005  sqrt2irr  16417  gcdcllem1  16669  gcdcllem2  16670  dfgcd2  16719  fissn0dvds  16794  dvdslcmf  16806  lcmfledvds  16807  lcmf  16808  lcmfunsnlem1  16812  lcmfunsnlem2lem1  16813  lcmfunsnlem  16816  lcmfdvds  16817  reumodprminv  16982  pc2dvds  17057  pcz  17059  prmpwdvds  17082  infpn2  17091  prmreclem2  17095  prmreclem3  17096  prmreclem5  17098  prmreclem6  17099  vdwlem6  17164  vdwlem8  17166  vdwlem13  17171  vdwnnlem1  17173  vdwnn  17176  ramcl  17207  cshwrepswhash1  17280  prdsleval  17648  imasval  17683  imasaddfnlem  17700  imasvscafn  17709  mrisval  17804  isacs  17825  isacs2  17827  isacs1i  17831  mreacs  17832  acsfn  17833  acsfn2  17837  iscatd  17847  catidex  17848  catideu  17849  cidval  17851  catidd  17854  comfeq  17880  catpropd  17883  ismon  17908  isfunc  18039  isnat  18125  isinito  18171  istermo  18172  isprs  18470  drsdirfi  18479  ispos  18488  lubfval  18522  lubeldm  18525  lubval  18528  lubprop  18530  lublecllem  18532  glbfval  18535  glbeldm  18538  glbval  18541  glbprop  18543  joinval2lem  18552  joinlem  18555  meetval2lem  18566  meetlem  18569  poslubmo  18583  posglbmo  18584  poslubd  18585  resspos  18603  isglbd  18683  lubl  18686  lubun  18689  clatleglb  18692  isdlat  18696  ipodrsima  18715  chneq1  18786  mgm1  18836  idressid  18862  gsumval2  18875  mgmhmima  18904  sgrp1  18918  mhmimalem  19020  mndind  19024  gsumwspan  19042  efmndmnd  19085  smndex1mnd  19109  sgrp2rid2  19125  sgrp2rid2ex  19126  sgrp2nmndlem4  19127  degenmgm  19137  degenmgm2  19140  pwmnd  19143  dfgrp2  19173  isgrpinv  19204  grpidinv  19209  dfgrp3lem  19248  issubg4  19356  isnsg2  19366  nsgacs  19372  elnmz  19373  cycsubgcl  19421  ghmrn  19443  ghmnsgima  19454  isga  19505  orbsta  19527  cntzfval  19534  elcntz  19536  resscntz  19547  oppgsubg  19577  symgextfo  19636  gsmsymgreqlem2  19645  gsmsymgreq  19646  pmtrdifel  19694  pmtrdifwrdellem3  19697  pmtrdifwrdel2  19700  psgnunilem2  19709  psgnunilem3  19710  odeq  19764  gexid  19795  gexlem2  19796  gexdvds  19798  isslw  19822  sylow2alem1  19831  sylow2alem2  19832  efgval  19931  efgrelexlemb  19964  efgcpbllemb  19969  abl1  20080  dmdprd  20214  dprd2da  20258  pgpfac1lem5  20295  isomnd  20337  ring1  20541  rngisomring  20697  rhmval0  20705  lringuplu  20796  rhmimasubrnglem  20817  isrrg  20950  isabv  21068  islss  21209  lssacs  21242  reslmhm  21327  islbs  21351  pj1lmhm  21375  lbsacsbs  21434  rnglidlmcl  21495  rnglidl0  21509  rspprop  21524  prmidl  21621  zringlpir  21773  psgndiflemA  21907  ocvfval  21972  elocv  21974  iunocv  21987  frlmlbs  22103  islindf  22118  islinds2  22119  islindf2  22120  lindfrn  22127  lsslindf  22136  islindf4  22144  opsrval  22355  ply1coe  22616  cply1coe0bi  22620  mat0dimcrng  22785  mdetunilem1  22927  mdetunilem9  22935  matunitlindflem2  22995  cpmat  23027  cpmatel  23029  1elcpmat  23033  m2cpminvid2lem  23072  basgen2  23307  bastop1  23311  isclo  23405  ordtbaslem  23506  iscn  23553  cnpval  23554  iscnp  23555  iscnp3  23562  lmbr  23576  lmbr2  23577  lmbrf  23578  cnprest  23607  cnprest2  23608  t0sep  23642  isreg  23650  t1sep2  23687  tgcmp  23719  1stcclb  23762  1stcfb  23763  2ndc1stc  23769  1stcrest  23771  2ndcdisj  23775  islly  23787  isnlly  23788  lly1stc  23815  isref  23828  islocfin  23836  elkgen  23855  kgencn  23875  elpt  23891  elptr  23892  ptcnplem  23940  tx1stc  23969  cnmpt21  23990  kqt0lem  24055  isr0  24056  regr1lem2  24059  r0sep  24067  nrmr0reg  24068  flffbas  24314  cnflf  24321  cnflf2  24322  lmflf  24324  txflf  24325  fclsopni  24334  fclsnei  24338  fclsrest  24343  fcfnei  24354  cnfcf  24361  alexsubb  24365  alexsubALTlem3  24368  qustgplem  24440  tsmsfbas  24447  tsmsres  24463  tsmsf1o  24464  tsmsxplem1  24472  ustval  24522  isust  24523  ustincl  24527  ustdiag  24528  ustinvel  24529  ustexhalf  24530  ust0  24539  utopval  24551  ucnval  24595  isucn  24596  isucn2  24597  ucnima  24599  iscfilu  24606  ispsmet  24623  ismet  24642  isxmet  24643  imasdsf1olem  24692  imasf1oxmet  24694  imasf1omet  24695  metss  24827  met1stc  24840  prdsxmslem2  24848  txmetcnp  24866  metucn  24890  tngngp3  24975  nlmvscn  25006  nmoval  25034  nmolb  25036  qtopbaslem  25077  cncfval  25209  elcncf2  25211  mulc1cncf  25226  cncfmet  25230  evth  25280  lebnumlem3  25284  lebnum  25285  xlebnum  25286  ishtpy  25293  isphtpy  25302  pi1xfr  25376  pi1coghm  25382  isclmp  25418  ipcn  25567  lmmbr2  25580  lmmbr3  25581  lmmbrf  25583  cfilfval  25585  iscfil  25586  fmcfil  25593  caufval  25596  iscau  25597  iscau2  25598  iscau3  25599  iscau4  25600  iscauf  25601  caucfil  25604  cfilresi  25616  causs  25619  lmclim  25624  cmetcusp1  25674  minveclem4c  25746  minveclem2  25747  minveclem3b  25749  minveclem4  25753  minveclem6  25755  minveclem7  25756  ovolicc2lem3  25840  ismbl  25847  dyadmax  25919  dyadmbllem  25920  dyadmbl  25921  opnmbllem  25922  ismbf1  25945  ismbf  25949  mbfeqalem2  25963  mbflimsup  25987  mbfi1fseqlem6  26041  mbfi1flimlem  26043  itg2seq  26063  itg2monolem1  26071  isibl  26086  ply1divex  26455  fta1g  26488  dgrco  26594  plydivex  26618  fta1  26629  vieta1  26635  aannenlem1  26655  aannenlem2  26656  aalioulem2  26660  aalioulem3  26661  ulmval  26707  ulm2  26712  ulmi  26713  ulmres  26715  ulmshftlem  26716  ulmcaulem  26721  ulmcau  26722  ulmss  26724  ulmbdd  26725  ulmdvlem1  26727  ulmdvlem3  26729  pilem2  26779  pilem3  26780  cxpcn3  27076  dmarea  27285  rlimcnp  27293  scvxcvx  27313  lgamgulmlem2  27357  lgamgulmlem3  27358  lgamgulmlem5  27360  lgambdd  27364  lgamcvglem  27367  isppw2  27442  perfectlem2  27557  2sqlem6  27750  2sqlem10  27755  addsq2reu  27767  2sqreulem1  27773  2sqreunnlem1  27776  dchrisumlema  27815  dchrisumlem2  27817  dchrisumlem3  27818  pntpbnd  27915  pntibndlem3  27919  pntibnd  27920  pntleme  27935  pntlem3  27936  pntlemp  27937  pnt3  27939  fltoprm  27995  ltsval  28004  nosupprefixmo  28057  noinfprefixmo  28058  nosupcbv  28059  nosupno  28060  nosupdm  28061  nosupfv  28063  nosupres  28064  nosupbnd1lem1  28065  nosupbnd1lem3  28067  nosupbnd1lem5  28069  noinfcbv  28074  noinfno  28075  noinfdm  28076  noinffv  28078  noinfres  28079  noinfbnd1lem3  28082  noinfbnd1lem5  28084  noetalem1  28098  noetalem2  28099  nocvxminlem  28140  brslts  28148  sltssnb  28155  conway  28165  etaslts  28179  lesrec  28185  eqcuts3  28190  madebdaylemlrcut  28285  madebday  28286  bdayle  28302  cofcutr  28310  cutmax  28320  cutmin  28321  lrrecfr  28329  addsprop  28362  negsunif  28441  addonbday  28665  onsfi  28742  n0subs  28749  bdayn0p1  28755  bdaypw2n0bndlem  28849  bdayfinbndlem2  28854  z12zsodd  28868  istrkgld  28921  axtg5seg  28927  tgcgr4  28994  perpln1  29185  perpln2  29186  isperp  29187  prlngmo2  29434  brbtwn2  29483  colinearalg  29488  axsegconlem1  29495  axsegcon  29505  ax5seglem4  29510  ax5seglem5  29511  axlowdim  29539  axeuclidlem  29540  axcontlem1  29542  axcontlem2  29543  axcontlem4  29545  axcontlem5  29546  axcontlem8  29549  axcontlem12  29553  elntg2  29563  uvtxusgr  29983  rgrx0ndm  30174  ewlksfval  30182  wksfval  30190  wwlks  30424  wlkiswwlks2  30464  clwwlk  30574  1conngr  30795  frgrwopregasn  30917  frgrwopregbsn  30918  frgrwopreglem5ALT  30923  frgrregord013  30996  isgrpo  31099  isgrpoi  31100  grpoideu  31111  grpoidinv2  31117  vciOLD  31163  isvclem  31179  cnidOLD  31184  isnvlem  31212  nvi  31216  lnoval  31354  islno  31355  isblo3i  31403  blo3i  31404  blocnilem  31406  ajfval  31411  ubthlem1  31472  ubthlem2  31473  ubthlem3  31474  ubth  31475  minvecolem2  31477  minvecolem3  31478  minvecolem4c  31481  minvecolem4  31482  minvecolem5  31483  minvecolem6  31484  minvecolem7  31485  h2hcau  31581  h2hlm  31582  hilid  31763  hcau  31786  hlimi  31790  hlim2  31794  ocel  31883  adjsym  32435  ellnop  32460  ellnfn  32485  hhcno  32506  hhcnf  32507  lnopeq  32611  elunop2  32615  lnophm  32621  lnconi  32635  lnopcnbd  32638  lnfncnbd  32659  imaelshi  32660  riesz3i  32664  riesz4i  32665  riesz4  32666  riesz1  32667  cnlnadjlem2  32670  cnlnadjlem5  32673  cnlnadjlem8  32676  cnlnadji  32678  nmopadjlei  32690  cnvbraval  32712  leopg  32724  leoppos  32728  mdbr  32896  dmdbr  32901  cdj3i  33043  disjunsn  33188  funcnv5mpt  33261  fgreu  33265  fcnvgreu  33266  xrge0infss  33352  wrdt2ind  33516  mgccole1  33551  mgccole2  33552  mgcmnt1  33553  mgcmnt2  33554  gsumhashmul  33628  isfxp  33729  fxpgaeq  33730  inftmrel  33741  isinftm  33742  archiabl  33759  isarchiofld  33760  elrgspnlem4  33806  0nellinds  33926  lindssn  33933  elrspunidl  33978  ismxidl  33987  1arithidom  34069  1arithufdlem3  34078  evl1deg1  34108  evl1deg2  34109  evl1deg3  34110  vietalem  34211  vieta  34212  crefeq  34477  zarcmplem  34513  esum2d  34725  sigaval  34743  issgon  34755  isrnmeas  34833  ismbfm  34884  mbfmcst  34891  elcarsg  34937  sitgval  34964  eulerpartlemd  34998  ballotleme  35129  tgoldbachgt  35292  bnj1185  35423  bnj1385  35462  bnj66  35490  bnj106  35498  bnj155  35509  bnj852  35551  bnj893  35558  bnj1228  35641  bnj1234  35643  bnj1463  35685  nummin  35722  r1omhfb  35738  elscott  35741  fineqvnttrclse  35792  r1omhfbregs  35805  gblacfnacd  35881  onvf1odlem4  35885  vonf1wev  35887  vonf1owevOLD  35889  derangenlem  35936  subfacp1lem3  35947  subfacp1lem5  35949  subfacp1lem6  35950  subfacp1  35951  erdszelem8  35963  kur14  35981  cnpconn  35995  resconn  36011  cvmscbv  36023  iscvm  36024  cvmsi  36030  cvmsval  36031  cvmlift3lem2  36085  snmlval  36096  satfv1  36128  fmlasucdisj  36164  satffunlem1lem1  36167  satffunlem2lem1  36169  satfv1fvfmla1  36188  mclsssvlem  36327  mclsval  36328  mclsax  36334  mclsind  36335  dfon2lem9  36553  dfrdg2  36557  dfrdg3  36558  fwddifnval  36928  nmulprop  36939  ltnadd  36967  nn0prpwlem  37110  isfne  37127  isfne4  37128  isfne2  37130  isfne3  37131  neibastop3  37150  topmeet  37152  topjoin  37153  filnetlem4  37169  weiunlem  37251  weiunfrlem  37252  dfttc4lem1  37316  dfttc4  37318  elttcirr  37319  unblimceq0lem  37372  unblimceq0  37373  unbdqndv2  37377  taupilemrplb  38241  fin2so  38530  lindsadd  38536  ptrecube  38538  poimirlem2  38540  poimirlem3  38541  poimirlem4  38542  poimirlem24  38562  poimirlem25  38563  poimirlem26  38564  poimirlem27  38565  poimirlem28  38566  poimirlem29  38567  poimirlem30  38568  poimirlem32  38570  poimir  38571  heicant  38573  mblfinlem1  38575  mblfinlem2  38576  voliunnfl  38582  volsupnfl  38583  mbfresfi  38584  itg2addnc  38592  upixp  38663  indexdom  38668  filbcmb  38674  sdclem2  38676  fdc  38679  lmclim2  38692  caures  38694  istotbnd  38703  istotbnd3  38705  sstotbnd  38709  isbnd  38714  heibor  38755  bfp  38758  rrncmslem  38766  isgrpda  38889  idlval  38947  isidl  38948  0idl  38959  unichnidl  38965  pridl  38971  ismaxidl  38974  smprngopr  38986  igenval2  39000  prnc  39001  ispridlc  39004  scottexf  39100  scott0f  39101  disjsuc2  39346  riotasvd  40013  islfl  40117  eqlkr  40156  eqlkr3  40158  glbconN  40434  hlsuprexch  40438  ispsubsp  40802  ldilset  41166  isldil  41167  dilsetN  41210  isdilN  41211  trlset  41218  trlval  41219  cdleme27b  41425  cdleme29b  41432  cdleme31so  41436  cdleme31sn1  41438  cdleme31sn1c  41445  cdleme31fv  41447  cdleme40v  41526  istendo  41817  cdlemkid3N  41990  cdlemkid4  41991  cdlemkid5  41992  dihfval  42288  dihval  42289  islpolN  42540  hdmapffval  42883  hdmapfval  42884  hdmapval  42885  hdmapval2lem  42888  hgmapffval  42942  hgmapfval  42943  hgmapval  42944  hgmapvs  42948  isprimroot  43143  aks6d1c1p1  43157  hashscontpow1  43171  sticksstones2  43197  unitscyglem3  43247  exfinfldd  43253  qsalrel  43292  supinf  43293  sn-sup2  43555  fsuppind  43618  isnacs  43714  isnacs2  43716  nacsfix  43722  mzpclval  43735  elmzpcl  43736  rencldnfilem  43826  infmrgelbi  43884  pellfundre  43887  pellfundlb  43890  wepwsolem  44048  aomclem8  44062  dfac11  44063  gicabl  44100  islnr3  44116  hbtlem2  44125  hbtlem5  44129  onintunirab  44228  onsucf1lem  44270  cantnfresb  44325  safesnsupfilb  44418  rp-brsslt  44423  fiinfi  44573  clsk1independent  45045  ntrclsk13  45070  gneispacess2  45145  imo72b2lem0  45164  imo72b2lem2  45166  imo72b2lem1  45168  imo72b2  45171  mnuop23d  45249  ismnushort  45284  ralabsobidv  45961  0elaxnul  45972  pwclaxpow  45973  prclaxpr  45974  uniclaxun  45975  omssaxinf2  45977  modelac8prim  45981  wfac8prim  45991  permac8prim  46003  evth2f  46031  evthf  46043  fnchoice  46045  uzwo4  46069  wessf1ornlem  46199  disjinfi  46206  rnmptlb  46254  rnmptbdd  46256  rnmptbd2  46260  rnmptbd  46267  dstregt0  46297  upbdrech2  46323  rexabslelem  46427  rexabsle  46428  uzub  46440  infrpgernmpt  46474  mccl  46609  ellimcabssub0  46628  climf  46633  clim2f  46645  limsupre  46650  clim2cf  46659  clim0cf  46663  climf2  46675  clim2f2  46679  clim2d  46682  limsupref  46694  limsupbnd1f  46695  climinf2  46716  limsuppnf  46720  climinfmpt  46724  climinf3  46725  limsupubuzmpt  46728  limsupmnf  46730  limsupre2lem  46733  limsupre2  46734  limsupmnfuzlem  46735  limsupmnfuz  46736  limsupre2mpt  46739  limsupre3lem  46741  limsupre3  46742  limsupre3mpt  46743  limsupre3uz  46745  limsupreuz  46746  limsupreuzmpt  46748  climuz  46753  liminfreuzlem  46811  liminfreuz  46812  cnrefiisplem  46838  xlimmnfvlem1  46841  xlimmnfv  46843  xlimpnfvlem1  46845  xlimpnfv  46847  xlimmnfmpt  46852  xlimpnfmpt  46853  cncfshift  46883  cncfperiod  46888  fperdvper  46928  dvbdfbdioo  46939  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  dvnprodlem3  46957  stoweidlem5  47014  stoweidlem9  47018  stoweidlem15  47024  stoweidlem16  47025  stoweidlem27  47036  stoweidlem28  47037  stoweidlem31  47040  stoweidlem34  47043  stoweidlem37  47046  stoweidlem46  47055  stoweidlem48  47057  stoweidlem51  47060  stoweidlem52  47061  stoweidlem59  47068  wallispilem3  47076  stirlinglem13  47095  fourierdlem2  47118  fourierdlem3  47119  fourierdlem16  47132  fourierdlem20  47136  fourierdlem21  47137  fourierdlem22  47138  fourierdlem25  47141  fourierdlem39  47155  fourierdlem42  47158  fourierdlem54  47169  fourierdlem64  47179  fourierdlem77  47192  fourierdlem83  47198  fourierdlem103  47218  fourierdlem104  47219  subsaliuncllem  47366  iundjiun  47469  meaiunincf  47492  caragenval  47502  isome  47503  caragenel  47504  omessle  47507  ovnlerp  47571  hoidmvlelem3  47606  hoidmvle  47609  issmflem  47736  issmfgt  47765  smfmullem2  47801  smfmullem4  47803  smfmul  47804  smfsuplem2  47821  smfsup  47823  smfinflem  47826  smfinf  47827  fsupdm  47851  finfdm  47855  cfsetsnfsetf  48127  cbvral2  48172  2reu8i  48182  2reuimp0  48183  dfdfat2  48197  iccpart  48497  iccpartigtl  48504  paireqne  48592  reupr  48603  perfectALTVlem2  48819  bgoldbachlt  48910  tgoldbachlt  48913  grimidvtxedg  48982  grimcnv  48985  grimco  48986  isuspgrim0  48991  gricushgr  49014  ushggricedg  49024  uhgrimisgrgric  49028  isubgr3stgr  49072  isgrlim  49079  isgrlim2  49080  uspgrlim  49089  grlicsym  49110  grlictr  49112  gpg5nbgrvtx03star  49177  gpg5nbgr3star  49178  pgnbgreunbgr  49222  upwlksfval  49232  nn0mnd  49275  uzlidlring  49331  smprngprmrng  49435  ply1mulgsumlem1  49497  ply1mulgsumlem2  49498  linindslinci  49559  lindslinindsimp1  49568  lindslinindsimp2lem5  49573  lindslinindsimp2  49574  linds0  49576  lindsrng01  49579  snlindsntor  49582  lmod1  49603  ldepsnlinc  49619  bigoval  49660  elbigo2r  49664  nn0sumshdiglem2  49733  eenglngeehlnmlem1  49848  eenglngeehlnmlem2  49849  lubeldm2d  50065  glbeldm2d  50066  lubsscl  50067  glbsscl  50068  ipolubdm  50094  ipolub  50095  ipoglbdm  50097  ipoglb  50098  nelsubc3lem  50177  upfval2  50284  upfval3  50285  isthincd2lem2  50542  setc1onsubc  50709  cnelsubclem  50710