Theorem ralbidv 3161

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 3159	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  3202  rexralbidv  3204  3ralbidv  3205  4ralbidv  3206  cbvral2vw  3220  cbvral4vw  3223  cbvral2v  3331  rspceaimv  3571  rspc2  3574  rspc2v  3576  rspc3v  3581  rspc4v  3585  reu6i  3675  reu7  3679  sbcralt  3811  reu8nf  3816  raaan  4459  raaanv  4460  raaan2  4463  2reu4lem  4464  reusngf  4619  2ralsng  4623  rexreusng  4624  reuprg0  4647  issn  4776  2ralunsn  4839  elintg  4898  elintrabg  4904  eliin  4939  disjprg  5082  disjxun  5084  brralrspcev  5146  reusv2lem2  5340  reusv3  5346  poeq1  5539  solin  5563  somo  5575  frirr  5604  fr2nr  5605  frminex  5607  wereu2  5625  posn  5714  frsn  5716  ralxpf  5799  cnvpo  6249  reu3op  6254  reuop  6255  dfpo2  6258  frpomin  6302  fnmptfvd  6991  iinpreima  7019  dff4  7051  dff13f  7207  fpropnf1  7219  f1ounsn  7224  eusvobj2  7356  ovanraleqv  7388  f1opr  7420  ofreq  7632  sorpssuni  7683  sorpssint  7684  fr3nr  7723  onssmin  7743  funcnvuni  7880  f1oweALT  7922  frxp  8073  frxp2  8091  xpord2indlem  8094  frxp3  8098  xpord3inddlem  8101  poseq  8105  soseq  8106  frecseq123  8229  csbfrecsg  8231  frrlem1  8233  frrlem13  8245  smoeq  8287  tfrlem12  8325  tz7.48lem  8377  naddcllem  8609  naddov2  8612  naddunif  8626  naddasslem1  8627  naddasslem2  8628  elixp2  8846  undifixp  8879  xpf1o  9074  nneneq  9137  ac6sfi  9191  frfi  9192  fipreima  9265  indexfi  9267  marypha1lem  9343  marypha1  9344  supeq1  9355  supeq3  9359  supmo  9362  eqsup  9366  supub  9369  suplub  9370  sup0  9377  supisoex  9385  eqinf  9395  infval  9397  infmo  9407  oieq1  9424  ordtypecbv  9429  ordtypelem3  9432  ordtypelem6  9435  ordtypelem7  9436  ordtypelem9  9438  wemaplem1  9458  wemaplem2  9459  zfregcl  9506  zfregclOLD  9507  oemapval  9601  oemapvali  9602  cantnf  9611  wemapwe  9615  ttrcleq  9627  ttrcltr  9634  ttrclss  9638  ttrclselem2  9644  rankval3b  9747  unbndrank  9763  rankunb  9771  rankuni2b  9774  tcrank  9805  scottex  9806  scottexs  9808  scott0s  9809  bnd2  9814  updjud  9855  dfac8clem  9951  ac5num  9955  acni  9964  acni2  9965  alephval3  10029  dfac4  10041  dfac5lem5  10046  dfac5  10048  dfac2a  10049  dfac2b  10050  dfacacn  10061  kmlem2  10071  kmlem13  10082  cflem  10164  cflemOLD  10165  cflecard  10172  cfeq0  10175  cfsuc  10176  cfflb  10178  cofsmo  10188  cfsmolem  10189  cfcoflem  10191  coftr  10192  alephsing  10195  fin23lem11  10236  isfin3ds  10248  fin23lem17  10257  fin23lem39  10269  isf33lem  10285  isf34lem6  10299  fin1a2lem13  10331  hsmexlem4  10348  hsmex  10351  axcc2lem  10355  axcc3  10357  dcomex  10366  axdc2lem  10367  axdc3lem2  10370  axdc3lem3  10371  axdc3  10373  axdc4lem  10374  axcclem  10376  zorn2lem2  10416  zorn2lem7  10421  zorn2g  10422  zornn0g  10424  ttukeylem7  10434  axdclem2  10439  brdom3  10447  brdom7disj  10450  brdom6disj  10451  alephval2  10492  inar1  10695  axgroth6  10748  pinq  10847  nqereu  10849  prlem934  10953  supexpr  10974  supsrlem  11031  axpre-sup  11089  dedekind  11306  dedekindle  11307  fiminre2  12101  lbreu  12103  sup2  12109  infm3  12112  nnsub  12218  uzwo  12858  nnwof  12861  ublbneg  12880  lbzbi  12883  zsupss  12884  uzsupss  12887  uzwo3  12890  zmax  12892  rpnnen1lem1  12925  rpnnen1lem3  12926  rpnnen1lem4  12927  rpnnen1lem5  12928  xrsupsslem  13256  xrinfmsslem  13257  xrsupss  13258  xrinfmss  13259  flval2  13770  axdc4uzlem  13942  ssnn0fi  13944  fsuppmapnn0fiubex  13951  faclbnd4lem4  14255  bccl  14281  hashgt12el  14381  hashbc  14412  hashge2el2dif  14439  wrdind  14681  wrd2ind  14682  rexanre  15306  rexico  15313  cau4  15316  reusq0  15424  clim  15453  rlim  15454  rlim2  15455  clim2  15463  clim2c  15464  clim0c  15466  rlim0  15467  rlim0lt  15468  ello12r  15476  ello1d  15482  elo12r  15487  rlimresb  15524  rlimcld2  15537  climabs0  15544  rlimo1  15576  lo1add  15586  lo1mul  15587  isercoll  15627  incexclem  15798  sqrt2irr  16213  gcdcllem1  16465  gcdcllem2  16466  dfgcd2  16512  fissn0dvds  16585  dvdslcmf  16597  lcmfledvds  16598  lcmf  16599  lcmfunsnlem1  16603  lcmfunsnlem2lem1  16604  lcmfunsnlem  16607  lcmfdvds  16608  reumodprminv  16772  pc2dvds  16847  pcz  16849  prmpwdvds  16872  infpn2  16881  prmreclem2  16885  prmreclem3  16886  prmreclem5  16888  prmreclem6  16889  vdwlem6  16954  vdwlem8  16956  vdwlem13  16961  vdwnnlem1  16963  vdwnn  16966  ramcl  16997  cshwrepswhash1  17070  prdsleval  17437  imasval  17472  imasaddfnlem  17489  imasvscafn  17498  mrisval  17593  isacs  17614  isacs2  17616  isacs1i  17620  mreacs  17621  acsfn  17622  acsfn2  17626  iscatd  17636  catidex  17637  catideu  17638  cidval  17640  catidd  17643  comfeq  17669  catpropd  17672  ismon  17697  isfunc  17828  isnat  17914  isinito  17960  istermo  17961  isprs  18259  drsdirfi  18268  ispos  18277  lubfval  18311  lubeldm  18314  lubval  18317  lubprop  18319  lublecllem  18321  glbfval  18324  glbeldm  18327  glbval  18330  glbprop  18332  joinval2lem  18341  joinlem  18344  meetval2lem  18355  meetlem  18358  poslubmo  18372  posglbmo  18373  poslubd  18374  resspos  18392  isglbd  18472  lubl  18475  lubun  18478  clatleglb  18481  isdlat  18485  ipodrsima  18504  chneq1  18575  mgm1  18623  gsumval2  18651  mgmhmima  18680  sgrp1  18694  mhmimalem  18789  mndind  18793  gsumwspan  18811  efmndmnd  18854  smndex1mnd  18878  sgrp2rid2  18894  sgrp2rid2ex  18895  sgrp2nmndlem4  18896  pwmnd  18905  dfgrp2  18935  isgrpinv  18966  grpidinv  18971  dfgrp3lem  19011  issubg4  19118  isnsg2  19128  nsgacs  19134  elnmz  19135  cycsubgcl  19178  ghmrn  19201  ghmnsgima  19212  isga  19263  orbsta  19285  cntzfval  19292  elcntz  19294  resscntz  19305  oppgsubg  19335  symgextfo  19394  gsmsymgreqlem2  19403  gsmsymgreq  19404  pmtrdifel  19452  pmtrdifwrdellem3  19455  pmtrdifwrdel2  19458  psgnunilem2  19467  psgnunilem3  19468  odeq  19522  gexid  19553  gexlem2  19554  gexdvds  19556  isslw  19580  sylow2alem1  19589  sylow2alem2  19590  efgval  19689  efgrelexlemb  19722  efgcpbllemb  19727  abl1  19838  dmdprd  19972  dprd2da  20016  pgpfac1lem5  20053  isomnd  20095  ring1  20288  rngisomring  20444  lringuplu  20518  rhmimasubrnglem  20539  isrrg  20672  isabv  20785  islss  20926  lssacs  20959  reslmhm  21045  islbs  21069  pj1lmhm  21093  lbsacsbs  21152  rnglidlmcl  21212  rnglidl0  21225  zringlpir  21463  psgndiflemA  21597  ocvfval  21662  elocv  21664  iunocv  21677  frlmlbs  21793  islindf  21808  islinds2  21809  islindf2  21810  lindfrn  21817  lsslindf  21826  islindf4  21834  opsrval  22040  ply1coe  22279  cply1coe0bi  22283  mat0dimcrng  22451  mdetunilem1  22593  mdetunilem9  22601  cpmat  22690  cpmatel  22692  1elcpmat  22696  m2cpminvid2lem  22735  basgen2  22970  bastop1  22974  isclo  23068  ordtbaslem  23169  iscn  23216  cnpval  23217  iscnp  23218  iscnp3  23225  lmbr  23239  lmbr2  23240  lmbrf  23241  cnprest  23270  cnprest2  23271  t0sep  23305  isreg  23313  t1sep2  23350  tgcmp  23382  1stcclb  23425  1stcfb  23426  2ndc1stc  23432  1stcrest  23434  2ndcdisj  23437  islly  23449  isnlly  23450  lly1stc  23477  isref  23490  islocfin  23498  elkgen  23517  kgencn  23537  elpt  23553  elptr  23554  ptcnplem  23602  tx1stc  23631  cnmpt21  23652  kqt0lem  23717  isr0  23718  regr1lem2  23721  r0sep  23729  nrmr0reg  23730  flffbas  23976  cnflf  23983  cnflf2  23984  lmflf  23986  txflf  23987  fclsopni  23996  fclsnei  24000  fclsrest  24005  fcfnei  24016  cnfcf  24023  alexsubb  24027  alexsubALTlem3  24030  qustgplem  24102  tsmsfbas  24109  tsmsres  24125  tsmsf1o  24126  tsmsxplem1  24134  ustval  24184  isust  24185  ustincl  24189  ustdiag  24190  ustinvel  24191  ustexhalf  24192  ust0  24201  utopval  24213  ucnval  24257  isucn  24258  isucn2  24259  ucnima  24261  iscfilu  24268  ispsmet  24285  ismet  24304  isxmet  24305  imasdsf1olem  24354  imasf1oxmet  24356  imasf1omet  24357  metss  24489  met1stc  24502  prdsxmslem2  24510  txmetcnp  24528  metucn  24552  tngngp3  24637  nlmvscn  24668  nmoval  24696  nmolb  24698  qtopbaslem  24739  cncfval  24871  elcncf2  24873  mulc1cncf  24888  cncfmet  24892  evth  24942  lebnumlem3  24946  lebnum  24947  xlebnum  24948  ishtpy  24955  isphtpy  24964  pi1xfr  25038  pi1coghm  25044  isclmp  25080  ipcn  25229  lmmbr2  25242  lmmbr3  25243  lmmbrf  25245  cfilfval  25247  iscfil  25248  fmcfil  25255  caufval  25258  iscau  25259  iscau2  25260  iscau3  25261  iscau4  25262  iscauf  25263  caucfil  25266  cfilresi  25278  causs  25281  lmclim  25286  cmetcusp1  25336  minveclem4c  25408  minveclem2  25409  minveclem3b  25411  minveclem4  25415  minveclem6  25417  minveclem7  25418  ovolicc2lem3  25502  ismbl  25509  dyadmax  25581  dyadmbllem  25582  dyadmbl  25583  opnmbllem  25584  ismbf1  25607  ismbf  25611  mbfeqalem2  25625  mbflimsup  25649  mbfi1fseqlem6  25703  mbfi1flimlem  25705  itg2seq  25725  itg2monolem1  25733  isibl  25748  ply1divex  26118  fta1g  26151  dgrco  26256  plydivex  26280  fta1  26291  vieta1  26295  aannenlem1  26311  aannenlem2  26312  aalioulem2  26316  aalioulem3  26317  ulmval  26364  ulm2  26369  ulmi  26370  ulmres  26372  ulmshftlem  26373  ulmcaulem  26378  ulmcau  26379  ulmss  26381  ulmbdd  26382  ulmdvlem1  26384  ulmdvlem3  26386  pilem2  26436  pilem3  26437  cxpcn3  26731  dmarea  26940  rlimcnp  26948  scvxcvx  26969  lgamgulmlem2  27013  lgamgulmlem3  27014  lgamgulmlem5  27016  lgambdd  27020  lgamcvglem  27023  isppw2  27098  perfectlem2  27213  2sqlem6  27406  2sqlem10  27411  addsq2reu  27423  2sqreulem1  27429  2sqreunnlem1  27432  dchrisumlema  27471  dchrisumlem2  27473  dchrisumlem3  27474  pntpbnd  27571  pntibndlem3  27575  pntibnd  27576  pntleme  27591  pntlem3  27592  pntlemp  27593  pnt3  27595  ltsval  27631  nosupprefixmo  27684  noinfprefixmo  27685  nosupcbv  27686  nosupno  27687  nosupdm  27688  nosupfv  27690  nosupres  27691  nosupbnd1lem1  27692  nosupbnd1lem3  27694  nosupbnd1lem5  27696  noinfcbv  27701  noinfno  27702  noinfdm  27703  noinffv  27705  noinfres  27706  noinfbnd1lem3  27709  noinfbnd1lem5  27711  noetalem1  27725  noetalem2  27726  nocvxminlem  27766  brslts  27774  sltssnb  27781  conway  27791  etaslts  27805  lesrec  27811  eqcuts3  27816  madebdaylemlrcut  27911  madebday  27912  bdayle  27928  cofcutr  27936  cutmax  27946  cutmin  27947  lrrecfr  27955  addsprop  27988  negsunif  28067  addonbday  28291  onsfi  28368  n0subs  28375  bdayn0p1  28381  bdaypw2n0bndlem  28475  bdayfinbndlem2  28480  z12zsodd  28494  istrkgld  28547  axtg5seg  28553  tgcgr4  28619  perpln1  28798  perpln2  28799  isperp  28800  brbtwn2  28994  colinearalg  28999  axsegconlem1  29006  axsegcon  29016  ax5seglem4  29021  ax5seglem5  29022  axlowdim  29050  axeuclidlem  29051  axcontlem1  29053  axcontlem2  29054  axcontlem4  29056  axcontlem5  29057  axcontlem8  29060  axcontlem12  29064  elntg2  29074  uvtxusgr  29491  rgrx0ndm  29683  ewlksfval  29691  wksfval  29699  wwlks  29924  wlkiswwlks2  29964  clwwlk  30074  1conngr  30285  frgrwopregasn  30407  frgrwopregbsn  30408  frgrwopreglem5ALT  30413  frgrregord013  30486  isgrpo  30589  isgrpoi  30590  grpoideu  30601  grpoidinv2  30607  vciOLD  30653  isvclem  30669  cnidOLD  30674  isnvlem  30702  nvi  30706  lnoval  30844  islno  30845  isblo3i  30893  blo3i  30894  blocnilem  30896  ajfval  30901  ubthlem1  30962  ubthlem2  30963  ubthlem3  30964  ubth  30965  minvecolem2  30967  minvecolem3  30968  minvecolem4c  30971  minvecolem4  30972  minvecolem5  30973  minvecolem6  30974  minvecolem7  30975  h2hcau  31071  h2hlm  31072  hilid  31253  hcau  31276  hlimi  31280  hlim2  31284  ocel  31373  adjsym  31925  ellnop  31950  ellnfn  31975  hhcno  31996  hhcnf  31997  lnopeq  32101  elunop2  32105  lnophm  32111  lnconi  32125  lnopcnbd  32128  lnfncnbd  32149  imaelshi  32150  riesz3i  32154  riesz4i  32155  riesz4  32156  riesz1  32157  cnlnadjlem2  32160  cnlnadjlem5  32163  cnlnadjlem8  32166  cnlnadji  32168  nmopadjlei  32180  cnvbraval  32202  leopg  32214  leoppos  32218  mdbr  32386  dmdbr  32391  cdj3i  32533  disjunsn  32685  funcnv5mpt  32761  fgreu  32765  fcnvgreu  32766  xrge0infss  32854  wrdt2ind  33034  mgccole1  33071  mgccole2  33072  mgcmnt1  33073  mgcmnt2  33074  gsumhashmul  33149  isfxp  33250  fxpgaeq  33251  inftmrel  33262  isinftm  33263  archiabl  33280  isarchiofld  33281  elrgspnlem4  33327  0nellinds  33451  lindssn  33459  elrspunidl  33509  prmidl  33521  ismxidl  33543  1arithidom  33618  1arithufdlem3  33627  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  vietalem  33744  vieta  33745  crefeq  34011  zarcmplem  34047  esum2d  34259  sigaval  34277  issgon  34289  isrnmeas  34366  ismbfm  34417  mbfmcst  34425  elcarsg  34471  sitgval  34498  eulerpartlemd  34532  ballotleme  34663  tgoldbachgt  34829  bnj1185  34957  bnj1385  34996  bnj66  35024  bnj106  35032  bnj155  35043  bnj852  35085  bnj893  35092  bnj1228  35175  bnj1234  35177  bnj1463  35219  nummin  35258  rankfilimbi  35266  r1omhfb  35278  fineqvnttrclse  35290  r1omhfbregs  35303  gblacfnacd  35306  onvf1odlem4  35310  vonf1owev  35312  derangenlem  35375  subfacp1lem3  35386  subfacp1lem5  35388  subfacp1lem6  35389  subfacp1  35390  erdszelem8  35402  kur14  35420  cnpconn  35434  resconn  35450  cvmscbv  35462  iscvm  35463  cvmsi  35469  cvmsval  35470  cvmlift3lem2  35524  snmlval  35535  satfv1  35567  fmlasucdisj  35603  satffunlem1lem1  35606  satffunlem2lem1  35608  satfv1fvfmla1  35627  mclsssvlem  35766  mclsval  35767  mclsax  35773  mclsind  35774  dfon2lem9  35993  dfrdg2  35997  dfrdg3  35998  fwddifnval  36367  nn0prpwlem  36526  isfne  36543  isfne4  36544  isfne2  36546  isfne3  36547  neibastop3  36566  topmeet  36568  topjoin  36569  filnetlem4  36585  weiunlem  36667  weiunfrlem  36668  dfttc4lem1  36732  dfttc4  36734  elttcirr  36735  unblimceq0lem  36788  unblimceq0  36789  unbdqndv2  36793  taupilemrplb  37656  fin2so  37950  lindsadd  37956  matunitlindflem2  37960  ptrecube  37963  poimirlem2  37965  poimirlem3  37966  poimirlem4  37967  poimirlem24  37987  poimirlem25  37988  poimirlem26  37989  poimirlem27  37990  poimirlem28  37991  poimirlem29  37992  poimirlem30  37993  poimirlem32  37995  poimir  37996  heicant  37998  mblfinlem1  38000  mblfinlem2  38001  voliunnfl  38007  volsupnfl  38008  mbfresfi  38009  itg2addnc  38017  upixp  38072  indexdom  38077  filbcmb  38083  sdclem2  38085  fdc  38088  lmclim2  38101  caures  38103  istotbnd  38112  istotbnd3  38114  sstotbnd  38118  isbnd  38123  heibor  38164  bfp  38167  rrncmslem  38175  isgrpda  38298  idlval  38356  isidl  38357  0idl  38368  unichnidl  38374  pridl  38380  ismaxidl  38383  smprngopr  38395  igenval2  38409  prnc  38410  ispridlc  38413  scottexf  38511  scott0f  38512  disjsuc2  38757  riotasvd  39424  islfl  39528  eqlkr  39567  eqlkr3  39569  glbconN  39845  hlsuprexch  39849  ispsubsp  40213  ldilset  40577  isldil  40578  dilsetN  40621  isdilN  40622  trlset  40629  trlval  40630  cdleme27b  40836  cdleme29b  40843  cdleme31so  40847  cdleme31sn1  40849  cdleme31sn1c  40856  cdleme31fv  40858  cdleme40v  40937  istendo  41228  cdlemkid3N  41401  cdlemkid4  41402  cdlemkid5  41403  dihfval  41699  dihval  41700  islpolN  41951  hdmapffval  42294  hdmapfval  42295  hdmapval  42296  hdmapval2lem  42299  hgmapffval  42353  hgmapfval  42354  hgmapval  42355  hgmapvs  42359  isprimroot  42554  aks6d1c1p1  42568  hashscontpow1  42582  sticksstones2  42608  unitscyglem3  42658  exfinfldd  42664  qsalrel  42702  supinf  42703  sn-sup2  42958  fsuppind  43045  isnacs  43158  isnacs2  43160  nacsfix  43166  mzpclval  43179  elmzpcl  43180  rencldnfilem  43274  infmrgelbi  43332  pellfundre  43335  pellfundlb  43338  wepwsolem  43496  fnwe2lem2  43505  aomclem8  43515  dfac11  43516  gicabl  43553  islnr3  43569  hbtlem2  43578  hbtlem5  43582  onintunirab  43681  onsucf1lem  43723  cantnfresb  43778  safesnsupfilb  43871  rp-brsslt  43876  fiinfi  44026  clsk1independent  44499  ntrclsk13  44524  gneispacess2  44599  imo72b2lem0  44618  imo72b2lem2  44620  imo72b2lem1  44622  imo72b2  44625  scottelrankd  44700  mnuop23d  44719  ismnushort  44754  ralabsobidv  45425  0elaxnul  45436  pwclaxpow  45437  prclaxpr  45438  uniclaxun  45439  omssaxinf2  45441  modelac8prim  45445  wfac8prim  45455  permac8prim  45467  evth2f  45472  evthf  45484  fnchoice  45486  uzwo4  45510  wessf1ornlem  45641  disjinfi  45648  rnmptlb  45698  rnmptbdd  45700  rnmptbd2  45704  rnmptbd  45711  dstregt0  45741  upbdrech2  45767  rexabslelem  45872  rexabsle  45873  uzub  45885  infrpgernmpt  45919  mccl  46054  ellimcabssub0  46073  climf  46078  clim2f  46090  limsupre  46095  clim2cf  46104  clim0cf  46108  climf2  46120  clim2f2  46124  clim2d  46127  limsupref  46139  limsupbnd1f  46140  climinf2  46161  limsuppnf  46165  climinfmpt  46169  climinf3  46170  limsupubuzmpt  46173  limsupmnf  46175  limsupre2lem  46178  limsupre2  46179  limsupmnfuzlem  46180  limsupmnfuz  46181  limsupre2mpt  46184  limsupre3lem  46186  limsupre3  46187  limsupre3mpt  46188  limsupre3uz  46190  limsupreuz  46191  limsupreuzmpt  46193  climuz  46198  liminfreuzlem  46256  liminfreuz  46257  cnrefiisplem  46283  xlimmnfvlem1  46286  xlimmnfv  46288  xlimpnfvlem1  46290  xlimpnfv  46292  xlimmnfmpt  46297  xlimpnfmpt  46298  cncfshift  46328  cncfperiod  46333  fperdvper  46373  dvbdfbdioo  46384  ioodvbdlimc1lem2  46386  ioodvbdlimc2lem  46388  dvnprodlem3  46402  stoweidlem5  46459  stoweidlem9  46463  stoweidlem15  46469  stoweidlem16  46470  stoweidlem27  46481  stoweidlem28  46482  stoweidlem31  46485  stoweidlem34  46488  stoweidlem37  46491  stoweidlem46  46500  stoweidlem48  46502  stoweidlem51  46505  stoweidlem52  46506  stoweidlem59  46513  wallispilem3  46521  stirlinglem13  46540  fourierdlem2  46563  fourierdlem3  46564  fourierdlem16  46577  fourierdlem20  46581  fourierdlem21  46582  fourierdlem22  46583  fourierdlem25  46586  fourierdlem39  46600  fourierdlem42  46603  fourierdlem54  46614  fourierdlem64  46624  fourierdlem77  46637  fourierdlem83  46643  fourierdlem103  46663  fourierdlem104  46664  subsaliuncllem  46811  iundjiun  46914  meaiunincf  46937  caragenval  46947  isome  46948  caragenel  46949  omessle  46952  ovnlerp  47016  hoidmvlelem3  47051  hoidmvle  47054  issmflem  47181  issmfgt  47210  smfmullem2  47246  smfmullem4  47248  smfmul  47249  smfsuplem2  47266  smfsup  47268  smfinflem  47271  smfinf  47272  fsupdm  47296  finfdm  47300  cfsetsnfsetf  47526  cbvral2  47571  2reu8i  47581  2reuimp0  47582  dfdfat2  47596  iccpart  47896  iccpartigtl  47903  paireqne  47991  reupr  48002  perfectALTVlem2  48218  bgoldbachlt  48309  tgoldbachlt  48312  grimidvtxedg  48381  grimcnv  48384  grimco  48385  isuspgrim0  48390  gricushgr  48413  ushggricedg  48423  uhgrimisgrgric  48427  isubgr3stgr  48471  isgrlim  48478  isgrlim2  48479  uspgrlim  48488  grlicsym  48509  grlictr  48511  gpg5nbgrvtx03star  48576  gpg5nbgr3star  48577  pgnbgreunbgr  48621  upwlksfval  48631  nn0mnd  48675  uzlidlring  48731  ply1mulgsumlem1  48882  ply1mulgsumlem2  48883  linindslinci  48944  lindslinindsimp1  48953  lindslinindsimp2lem5  48958  lindslinindsimp2  48959  linds0  48961  lindsrng01  48964  snlindsntor  48967  lmod1  48988  ldepsnlinc  49004  bigoval  49045  elbigo2r  49049  nn0sumshdiglem2  49118  eenglngeehlnmlem1  49233  eenglngeehlnmlem2  49234  lubeldm2d  49453  glbeldm2d  49454  lubsscl  49455  glbsscl  49456  ipolubdm  49482  ipolub  49483  ipoglbdm  49485  ipoglb  49486  nelsubc3lem  49565  upfval2  49672  upfval3  49673  isthincd2lem2  49930  setc1onsubc  50097  cnelsubclem  50098  setrec1lem2  50183