Theorem ralbidv 3185

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077

This theorem is used by:  2ralbidv  3226  rexralbidv  3228  3ralbidv  3229  4ralbidv  3230  cbvral2vw  3244  cbvral4vw  3247  cbvral2v  3353  rspceaimv  3582  rspc2  3584  rspc2v  3586  rspc3v  3591  rspc4v  3595  reu6i  3685  reu7  3689  sbcralt  3818  reu8nf  3823  raaan  4473  raaanv  4474  raaan2  4477  2reu4lem  4478  reusngf  4634  2ralsng  4638  rexreusng  4639  reuprg0  4662  issn  4791  2ralunsn  4854  elintg  4914  elintrabg  4920  eliin  4955  disjprg  5098  disjxun  5100  brralrspcev  5164  reusv2lem2  5360  reusv3  5366  poeq1  5561  solin  5585  somo  5597  frirr  5626  fr2nr  5627  frminex  5629  wereu2  5647  posn  5736  frsn  5738  ralxpf  5823  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  38242  fin2so  38531  lindsadd  38537  ptrecube  38539  poimirlem2  38541  poimirlem3  38542  poimirlem4  38543  poimirlem24  38563  poimirlem25  38564  poimirlem26  38565  poimirlem27  38566  poimirlem28  38567  poimirlem29  38568  poimirlem30  38569  poimirlem32  38571  poimir  38572  heicant  38574  mblfinlem1  38576  mblfinlem2  38577  voliunnfl  38583  volsupnfl  38584  mbfresfi  38585  itg2addnc  38593  upixp  38664  indexdom  38669  filbcmb  38675  sdclem2  38677  fdc  38680  lmclim2  38693  caures  38695  istotbnd  38704  istotbnd3  38706  sstotbnd  38710  isbnd  38715  heibor  38756  bfp  38759  rrncmslem  38767  isgrpda  38890  idlval  38948  isidl  38949  0idl  38960  unichnidl  38966  pridl  38972  ismaxidl  38975  smprngopr  38987  igenval2  39001  prnc  39002  ispridlc  39005  scottexf  39101  scott0f  39102  disjsuc2  39347  riotasvd  40014  islfl  40118  eqlkr  40157  eqlkr3  40159  glbconN  40435  hlsuprexch  40439  ispsubsp  40803  ldilset  41167  isldil  41168  dilsetN  41211  isdilN  41212  trlset  41219  trlval  41220  cdleme27b  41426  cdleme29b  41433  cdleme31so  41437  cdleme31sn1  41439  cdleme31sn1c  41446  cdleme31fv  41448  cdleme40v  41527  istendo  41818  cdlemkid3N  41991  cdlemkid4  41992  cdlemkid5  41993  dihfval  42289  dihval  42290  islpolN  42541  hdmapffval  42884  hdmapfval  42885  hdmapval  42886  hdmapval2lem  42889  hgmapffval  42943  hgmapfval  42944  hgmapval  42945  hgmapvs  42949  isprimroot  43144  aks6d1c1p1  43158  hashscontpow1  43172  sticksstones2  43198  unitscyglem3  43248  exfinfldd  43254  qsalrel  43293  supinf  43294  sn-sup2  43556  fsuppind  43619  isnacs  43715  isnacs2  43717  nacsfix  43723  mzpclval  43736  elmzpcl  43737  rencldnfilem  43827  infmrgelbi  43885  pellfundre  43888  pellfundlb  43891  wepwsolem  44049  aomclem8  44063  dfac11  44064  gicabl  44101  islnr3  44117  hbtlem2  44126  hbtlem5  44130  onintunirab  44229  onsucf1lem  44271  cantnfresb  44326  safesnsupfilb  44419  rp-brsslt  44424  fiinfi  44574  clsk1independent  45046  ntrclsk13  45071  gneispacess2  45146  imo72b2lem0  45165  imo72b2lem2  45167  imo72b2lem1  45169  imo72b2  45172  mnuop23d  45250  ismnushort  45285  ralabsobidv  45962  0elaxnul  45973  pwclaxpow  45974  prclaxpr  45975  uniclaxun  45976  omssaxinf2  45978  modelac8prim  45982  wfac8prim  45992  permac8prim  46004  evth2f  46032  evthf  46044  fnchoice  46046  uzwo4  46070  wessf1ornlem  46200  disjinfi  46207  rnmptlb  46255  rnmptbdd  46257  rnmptbd2  46261  rnmptbd  46268  dstregt0  46298  upbdrech2  46324  rexabslelem  46428  rexabsle  46429  uzub  46441  infrpgernmpt  46475  mccl  46610  ellimcabssub0  46629  climf  46634  clim2f  46646  limsupre  46651  clim2cf  46660  clim0cf  46664  climf2  46676  clim2f2  46680  clim2d  46683  limsupref  46695  limsupbnd1f  46696  climinf2  46717  limsuppnf  46721  climinfmpt  46725  climinf3  46726  limsupubuzmpt  46729  limsupmnf  46731  limsupre2lem  46734  limsupre2  46735  limsupmnfuzlem  46736  limsupmnfuz  46737  limsupre2mpt  46740  limsupre3lem  46742  limsupre3  46743  limsupre3mpt  46744  limsupre3uz  46746  limsupreuz  46747  limsupreuzmpt  46749  climuz  46754  liminfreuzlem  46812  liminfreuz  46813  cnrefiisplem  46839  xlimmnfvlem1  46842  xlimmnfv  46844  xlimpnfvlem1  46846  xlimpnfv  46848  xlimmnfmpt  46853  xlimpnfmpt  46854  cncfshift  46884  cncfperiod  46889  fperdvper  46929  dvbdfbdioo  46940  ioodvbdlimc1lem2  46942  ioodvbdlimc2lem  46944  dvnprodlem3  46958  stoweidlem5  47015  stoweidlem9  47019  stoweidlem15  47025  stoweidlem16  47026  stoweidlem27  47037  stoweidlem28  47038  stoweidlem31  47041  stoweidlem34  47044  stoweidlem37  47047  stoweidlem46  47056  stoweidlem48  47058  stoweidlem51  47061  stoweidlem52  47062  stoweidlem59  47069  wallispilem3  47077  stirlinglem13  47096  fourierdlem2  47119  fourierdlem3  47120  fourierdlem16  47133  fourierdlem20  47137  fourierdlem21  47138  fourierdlem22  47139  fourierdlem25  47142  fourierdlem39  47156  fourierdlem42  47159  fourierdlem54  47170  fourierdlem64  47180  fourierdlem77  47193  fourierdlem83  47199  fourierdlem103  47219  fourierdlem104  47220  subsaliuncllem  47367  iundjiun  47470  meaiunincf  47493  caragenval  47503  isome  47504  caragenel  47505  omessle  47508  ovnlerp  47572  hoidmvlelem3  47607  hoidmvle  47610  issmflem  47737  issmfgt  47766  smfmullem2  47802  smfmullem4  47804  smfmul  47805  smfsuplem2  47822  smfsup  47824  smfinflem  47827  smfinf  47828  fsupdm  47852  finfdm  47856  cfsetsnfsetf  48128  cbvral2  48173  2reu8i  48183  2reuimp0  48184  dfdfat2  48198  iccpart  48498  iccpartigtl  48505  paireqne  48593  reupr  48604  perfectALTVlem2  48820  bgoldbachlt  48911  tgoldbachlt  48914  grimidvtxedg  48983  grimcnv  48986  grimco  48987  isuspgrim0  48992  gricushgr  49015  ushggricedg  49025  uhgrimisgrgric  49029  isubgr3stgr  49073  isgrlim  49080  isgrlim2  49081  uspgrlim  49090  grlicsym  49111  grlictr  49113  gpg5nbgrvtx03star  49178  gpg5nbgr3star  49179  pgnbgreunbgr  49223  upwlksfval  49233  nn0mnd  49276  uzlidlring  49332  smprngprmrng  49436  ply1mulgsumlem1  49498  ply1mulgsumlem2  49499  linindslinci  49560  lindslinindsimp1  49569  lindslinindsimp2lem5  49574  lindslinindsimp2  49575  linds0  49577  lindsrng01  49580  snlindsntor  49583  lmod1  49604  ldepsnlinc  49620  bigoval  49661  elbigo2r  49665  nn0sumshdiglem2  49734  eenglngeehlnmlem1  49849  eenglngeehlnmlem2  49850  lubeldm2d  50066  glbeldm2d  50067  lubsscl  50068  glbsscl  50069  ipolubdm  50095  ipolub  50096  ipoglbdm  50098  ipoglb  50099  nelsubc3lem  50178  upfval2  50285  upfval3  50286  isthincd2lem2  50543  setc1onsubc  50710  cnelsubclem  50711