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  5336  reusv3  5342  poeq1  5535  solin  5559  somo  5571  frirr  5600  fr2nr  5601  frminex  5603  wereu2  5621  posn  5710  frsn  5712  ralxpf  5795  cnvpo  6245  reu3op  6250  reuop  6251  dfpo2  6254  frpomin  6298  fnmptfvd  6987  iinpreima  7015  dff4  7047  dff13f  7203  fpropnf1  7215  f1ounsn  7220  eusvobj2  7352  ovanraleqv  7384  f1opr  7416  ofreq  7628  sorpssuni  7679  sorpssint  7680  fr3nr  7719  onssmin  7739  funcnvuni  7876  f1oweALT  7918  frxp  8069  frxp2  8087  xpord2indlem  8090  frxp3  8094  xpord3inddlem  8097  poseq  8101  soseq  8102  frecseq123  8225  csbfrecsg  8227  frrlem1  8229  frrlem13  8241  smoeq  8283  tfrlem12  8321  tz7.48lem  8373  naddcllem  8605  naddov2  8608  naddunif  8622  naddasslem1  8623  naddasslem2  8624  elixp2  8842  undifixp  8875  xpf1o  9070  nneneq  9133  ac6sfi  9187  frfi  9188  fipreima  9261  indexfi  9263  marypha1lem  9339  marypha1  9340  supeq1  9351  supeq3  9355  supmo  9358  eqsup  9362  supub  9365  suplub  9366  sup0  9373  supisoex  9381  eqinf  9391  infval  9393  infmo  9403  oieq1  9420  ordtypecbv  9425  ordtypelem3  9428  ordtypelem6  9431  ordtypelem7  9432  ordtypelem9  9434  wemaplem1  9454  wemaplem2  9455  zfregcl  9502  zfregclOLD  9503  oemapval  9595  oemapvali  9596  cantnf  9605  wemapwe  9609  ttrcleq  9621  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  rankval3b  9741  unbndrank  9757  rankunb  9765  rankuni2b  9768  tcrank  9799  scottex  9800  scottexs  9802  scott0s  9803  bnd2  9808  updjud  9849  dfac8clem  9945  ac5num  9949  acni  9958  acni2  9959  alephval3  10023  dfac4  10035  dfac5lem5  10040  dfac5  10042  dfac2a  10043  dfac2b  10044  dfacacn  10055  kmlem2  10065  kmlem13  10076  cflem  10158  cflemOLD  10159  cflecard  10166  cfeq0  10169  cfsuc  10170  cfflb  10172  cofsmo  10182  cfsmolem  10183  cfcoflem  10185  coftr  10186  alephsing  10189  fin23lem11  10230  isfin3ds  10242  fin23lem17  10251  fin23lem39  10263  isf33lem  10279  isf34lem6  10293  fin1a2lem13  10325  hsmexlem4  10342  hsmex  10345  axcc2lem  10349  axcc3  10351  dcomex  10360  axdc2lem  10361  axdc3lem2  10364  axdc3lem3  10365  axdc3  10367  axdc4lem  10368  axcclem  10370  zorn2lem2  10410  zorn2lem7  10415  zorn2g  10416  zornn0g  10418  ttukeylem7  10428  axdclem2  10433  brdom3  10441  brdom7disj  10444  brdom6disj  10445  alephval2  10486  inar1  10689  axgroth6  10742  pinq  10841  nqereu  10843  prlem934  10947  supexpr  10968  supsrlem  11025  axpre-sup  11083  dedekind  11300  dedekindle  11301  fiminre2  12095  lbreu  12097  sup2  12103  infm3  12106  nnsub  12212  uzwo  12852  nnwof  12855  ublbneg  12874  lbzbi  12877  zsupss  12878  uzsupss  12881  uzwo3  12884  zmax  12886  rpnnen1lem1  12919  rpnnen1lem3  12920  rpnnen1lem4  12921  rpnnen1lem5  12922  xrsupsslem  13250  xrinfmsslem  13251  xrsupss  13252  xrinfmss  13253  flval2  13764  axdc4uzlem  13936  ssnn0fi  13938  fsuppmapnn0fiubex  13945  faclbnd4lem4  14249  bccl  14275  hashgt12el  14375  hashbc  14406  hashge2el2dif  14433  wrdind  14675  wrd2ind  14676  rexanre  15300  rexico  15307  cau4  15310  reusq0  15418  clim  15447  rlim  15448  rlim2  15449  clim2  15457  clim2c  15458  clim0c  15460  rlim0  15461  rlim0lt  15462  ello12r  15470  ello1d  15476  elo12r  15481  rlimresb  15518  rlimcld2  15531  climabs0  15538  rlimo1  15570  lo1add  15580  lo1mul  15581  isercoll  15621  incexclem  15792  sqrt2irr  16207  gcdcllem1  16459  gcdcllem2  16460  dfgcd2  16506  fissn0dvds  16579  dvdslcmf  16591  lcmfledvds  16592  lcmf  16593  lcmfunsnlem1  16597  lcmfunsnlem2lem1  16598  lcmfunsnlem  16601  lcmfdvds  16602  reumodprminv  16766  pc2dvds  16841  pcz  16843  prmpwdvds  16866  infpn2  16875  prmreclem2  16879  prmreclem3  16880  prmreclem5  16882  prmreclem6  16883  vdwlem6  16948  vdwlem8  16950  vdwlem13  16955  vdwnnlem1  16957  vdwnn  16960  ramcl  16991  cshwrepswhash1  17064  prdsleval  17431  imasval  17466  imasaddfnlem  17483  imasvscafn  17492  mrisval  17587  isacs  17608  isacs2  17610  isacs1i  17614  mreacs  17615  acsfn  17616  acsfn2  17620  iscatd  17630  catidex  17631  catideu  17632  cidval  17634  catidd  17637  comfeq  17663  catpropd  17666  ismon  17691  isfunc  17822  isnat  17908  isinito  17954  istermo  17955  isprs  18253  drsdirfi  18262  ispos  18271  lubfval  18305  lubeldm  18308  lubval  18311  lubprop  18313  lublecllem  18315  glbfval  18318  glbeldm  18321  glbval  18324  glbprop  18326  joinval2lem  18335  joinlem  18338  meetval2lem  18349  meetlem  18352  poslubmo  18366  posglbmo  18367  poslubd  18368  resspos  18386  isglbd  18466  lubl  18469  lubun  18472  clatleglb  18475  isdlat  18479  ipodrsima  18498  chneq1  18569  mgm1  18617  gsumval2  18645  mgmhmima  18674  sgrp1  18688  mhmimalem  18783  mndind  18787  gsumwspan  18805  efmndmnd  18848  smndex1mnd  18872  sgrp2rid2  18888  sgrp2rid2ex  18889  sgrp2nmndlem4  18890  pwmnd  18899  dfgrp2  18929  isgrpinv  18960  grpidinv  18965  dfgrp3lem  19005  issubg4  19112  isnsg2  19122  nsgacs  19128  elnmz  19129  cycsubgcl  19172  ghmrn  19195  ghmnsgima  19206  isga  19257  orbsta  19279  cntzfval  19286  elcntz  19288  resscntz  19299  oppgsubg  19329  symgextfo  19388  gsmsymgreqlem2  19397  gsmsymgreq  19398  pmtrdifel  19446  pmtrdifwrdellem3  19449  pmtrdifwrdel2  19452  psgnunilem2  19461  psgnunilem3  19462  odeq  19516  gexid  19547  gexlem2  19548  gexdvds  19550  isslw  19574  sylow2alem1  19583  sylow2alem2  19584  efgval  19683  efgrelexlemb  19716  efgcpbllemb  19721  abl1  19832  dmdprd  19966  dprd2da  20010  pgpfac1lem5  20047  isomnd  20089  ring1  20282  rngisomring  20438  lringuplu  20512  rhmimasubrnglem  20533  isrrg  20666  isabv  20779  islss  20920  lssacs  20953  reslmhm  21039  islbs  21063  pj1lmhm  21087  lbsacsbs  21146  rnglidlmcl  21206  rnglidl0  21219  zringlpir  21457  psgndiflemA  21591  ocvfval  21656  elocv  21658  iunocv  21671  frlmlbs  21787  islindf  21802  islinds2  21803  islindf2  21804  lindfrn  21811  lsslindf  21820  islindf4  21828  opsrval  22034  ply1coe  22273  cply1coe0bi  22277  mat0dimcrng  22445  mdetunilem1  22587  mdetunilem9  22595  cpmat  22684  cpmatel  22686  1elcpmat  22690  m2cpminvid2lem  22729  basgen2  22964  bastop1  22968  isclo  23062  ordtbaslem  23163  iscn  23210  cnpval  23211  iscnp  23212  iscnp3  23219  lmbr  23233  lmbr2  23234  lmbrf  23235  cnprest  23264  cnprest2  23265  t0sep  23299  isreg  23307  t1sep2  23344  tgcmp  23376  1stcclb  23419  1stcfb  23420  2ndc1stc  23426  1stcrest  23428  2ndcdisj  23431  islly  23443  isnlly  23444  lly1stc  23471  isref  23484  islocfin  23492  elkgen  23511  kgencn  23531  elpt  23547  elptr  23548  ptcnplem  23596  tx1stc  23625  cnmpt21  23646  kqt0lem  23711  isr0  23712  regr1lem2  23715  r0sep  23723  nrmr0reg  23724  flffbas  23970  cnflf  23977  cnflf2  23978  lmflf  23980  txflf  23981  fclsopni  23990  fclsnei  23994  fclsrest  23999  fcfnei  24010  cnfcf  24017  alexsubb  24021  alexsubALTlem3  24024  qustgplem  24096  tsmsfbas  24103  tsmsres  24119  tsmsf1o  24120  tsmsxplem1  24128  ustval  24178  isust  24179  ustincl  24183  ustdiag  24184  ustinvel  24185  ustexhalf  24186  ust0  24195  utopval  24207  ucnval  24251  isucn  24252  isucn2  24253  ucnima  24255  iscfilu  24262  ispsmet  24279  ismet  24298  isxmet  24299  imasdsf1olem  24348  imasf1oxmet  24350  imasf1omet  24351  metss  24483  met1stc  24496  prdsxmslem2  24504  txmetcnp  24522  metucn  24546  tngngp3  24631  nlmvscn  24662  nmoval  24690  nmolb  24692  qtopbaslem  24733  cncfval  24865  elcncf2  24867  mulc1cncf  24882  cncfmet  24886  evth  24936  lebnumlem3  24940  lebnum  24941  xlebnum  24942  ishtpy  24949  isphtpy  24958  pi1xfr  25032  pi1coghm  25038  isclmp  25074  ipcn  25223  lmmbr2  25236  lmmbr3  25237  lmmbrf  25239  cfilfval  25241  iscfil  25242  fmcfil  25249  caufval  25252  iscau  25253  iscau2  25254  iscau3  25255  iscau4  25256  iscauf  25257  caucfil  25260  cfilresi  25272  causs  25275  lmclim  25280  cmetcusp1  25330  minveclem4c  25402  minveclem2  25403  minveclem3b  25405  minveclem4  25409  minveclem6  25411  minveclem7  25412  ovolicc2lem3  25496  ismbl  25503  dyadmax  25575  dyadmbllem  25576  dyadmbl  25577  opnmbllem  25578  ismbf1  25601  ismbf  25605  mbfeqalem2  25619  mbflimsup  25643  mbfi1fseqlem6  25697  mbfi1flimlem  25699  itg2seq  25719  itg2monolem1  25727  isibl  25742  ply1divex  26112  fta1g  26145  dgrco  26250  plydivex  26274  fta1  26285  vieta1  26289  aannenlem1  26305  aannenlem2  26306  aalioulem2  26310  aalioulem3  26311  ulmval  26358  ulm2  26363  ulmi  26364  ulmres  26366  ulmshftlem  26367  ulmcaulem  26372  ulmcau  26373  ulmss  26375  ulmbdd  26376  ulmdvlem1  26378  ulmdvlem3  26380  pilem2  26430  pilem3  26431  cxpcn3  26725  dmarea  26934  rlimcnp  26942  scvxcvx  26963  lgamgulmlem2  27007  lgamgulmlem3  27008  lgamgulmlem5  27010  lgambdd  27014  lgamcvglem  27017  isppw2  27092  perfectlem2  27207  2sqlem6  27400  2sqlem10  27405  addsq2reu  27417  2sqreulem1  27423  2sqreunnlem1  27426  dchrisumlema  27465  dchrisumlem2  27467  dchrisumlem3  27468  pntpbnd  27565  pntibndlem3  27569  pntibnd  27570  pntleme  27585  pntlem3  27586  pntlemp  27587  pnt3  27589  ltsval  27625  nosupprefixmo  27678  noinfprefixmo  27679  nosupcbv  27680  nosupno  27681  nosupdm  27682  nosupfv  27684  nosupres  27685  nosupbnd1lem1  27686  nosupbnd1lem3  27688  nosupbnd1lem5  27690  noinfcbv  27695  noinfno  27696  noinfdm  27697  noinffv  27699  noinfres  27700  noinfbnd1lem3  27703  noinfbnd1lem5  27705  noetalem1  27719  noetalem2  27720  nocvxminlem  27760  brslts  27768  sltssnb  27775  conway  27785  etaslts  27799  lesrec  27805  eqcuts3  27810  madebdaylemlrcut  27905  madebday  27906  bdayle  27922  cofcutr  27930  cutmax  27940  cutmin  27941  lrrecfr  27949  addsprop  27982  negsunif  28061  addonbday  28285  onsfi  28362  n0subs  28369  bdayn0p1  28375  bdaypw2n0bndlem  28469  bdayfinbndlem2  28474  z12zsodd  28488  istrkgld  28541  axtg5seg  28547  tgcgr4  28613  perpln1  28792  perpln2  28793  isperp  28794  brbtwn2  28988  colinearalg  28993  axsegconlem1  29000  axsegcon  29010  ax5seglem4  29015  ax5seglem5  29016  axlowdim  29044  axeuclidlem  29045  axcontlem1  29047  axcontlem2  29048  axcontlem4  29050  axcontlem5  29051  axcontlem8  29054  axcontlem12  29058  elntg2  29068  uvtxusgr  29485  rgrx0ndm  29677  ewlksfval  29685  wksfval  29693  wwlks  29918  wlkiswwlks2  29958  clwwlk  30068  1conngr  30279  frgrwopregasn  30401  frgrwopregbsn  30402  frgrwopreglem5ALT  30407  frgrregord013  30480  isgrpo  30583  isgrpoi  30584  grpoideu  30595  grpoidinv2  30601  vciOLD  30647  isvclem  30663  cnidOLD  30668  isnvlem  30696  nvi  30700  lnoval  30838  islno  30839  isblo3i  30887  blo3i  30888  blocnilem  30890  ajfval  30895  ubthlem1  30956  ubthlem2  30957  ubthlem3  30958  ubth  30959  minvecolem2  30961  minvecolem3  30962  minvecolem4c  30965  minvecolem4  30966  minvecolem5  30967  minvecolem6  30968  minvecolem7  30969  h2hcau  31065  h2hlm  31066  hilid  31247  hcau  31270  hlimi  31274  hlim2  31278  ocel  31367  adjsym  31919  ellnop  31944  ellnfn  31969  hhcno  31990  hhcnf  31991  lnopeq  32095  elunop2  32099  lnophm  32105  lnconi  32119  lnopcnbd  32122  lnfncnbd  32143  imaelshi  32144  riesz3i  32148  riesz4i  32149  riesz4  32150  riesz1  32151  cnlnadjlem2  32154  cnlnadjlem5  32157  cnlnadjlem8  32160  cnlnadji  32162  nmopadjlei  32174  cnvbraval  32196  leopg  32208  leoppos  32212  mdbr  32380  dmdbr  32385  cdj3i  32527  disjunsn  32679  funcnv5mpt  32755  fgreu  32759  fcnvgreu  32760  xrge0infss  32848  wrdt2ind  33028  mgccole1  33065  mgccole2  33066  mgcmnt1  33067  mgcmnt2  33068  gsumhashmul  33143  isfxp  33244  fxpgaeq  33245  inftmrel  33256  isinftm  33257  archiabl  33274  isarchiofld  33275  elrgspnlem4  33321  0nellinds  33445  lindssn  33453  elrspunidl  33503  prmidl  33515  ismxidl  33537  1arithidom  33612  1arithufdlem3  33621  evl1deg1  33651  evl1deg2  33652  evl1deg3  33653  vietalem  33738  vieta  33739  crefeq  34005  zarcmplem  34041  esum2d  34253  sigaval  34271  issgon  34283  isrnmeas  34360  ismbfm  34411  mbfmcst  34419  elcarsg  34465  sitgval  34492  eulerpartlemd  34526  ballotleme  34657  tgoldbachgt  34823  bnj1185  34951  bnj1385  34990  bnj66  35018  bnj106  35026  bnj155  35037  bnj852  35079  bnj893  35086  bnj1228  35169  bnj1234  35171  bnj1463  35213  nummin  35252  rankfilimbi  35260  r1omhfb  35272  fineqvnttrclse  35284  r1omhfbregs  35297  gblacfnacd  35300  onvf1odlem4  35304  vonf1owev  35306  derangenlem  35369  subfacp1lem3  35380  subfacp1lem5  35382  subfacp1lem6  35383  subfacp1  35384  erdszelem8  35396  kur14  35414  cnpconn  35428  resconn  35444  cvmscbv  35456  iscvm  35457  cvmsi  35463  cvmsval  35464  cvmlift3lem2  35518  snmlval  35529  satfv1  35561  fmlasucdisj  35597  satffunlem1lem1  35600  satffunlem2lem1  35602  satfv1fvfmla1  35621  mclsssvlem  35760  mclsval  35761  mclsax  35767  mclsind  35768  dfon2lem9  35987  dfrdg2  35991  dfrdg3  35992  fwddifnval  36361  nn0prpwlem  36520  isfne  36537  isfne4  36538  isfne2  36540  isfne3  36541  neibastop3  36560  topmeet  36562  topjoin  36563  filnetlem4  36579  weiunlem  36661  weiunfrlem  36662  dfttc4lem1  36726  dfttc4  36728  elttcirr  36729  unblimceq0lem  36782  unblimceq0  36783  unbdqndv2  36787  taupilemrplb  37650  fin2so  37942  lindsadd  37948  matunitlindflem2  37952  ptrecube  37955  poimirlem2  37957  poimirlem3  37958  poimirlem4  37959  poimirlem24  37979  poimirlem25  37980  poimirlem26  37981  poimirlem27  37982  poimirlem28  37983  poimirlem29  37984  poimirlem30  37985  poimirlem32  37987  poimir  37988  heicant  37990  mblfinlem1  37992  mblfinlem2  37993  voliunnfl  37999  volsupnfl  38000  mbfresfi  38001  itg2addnc  38009  upixp  38064  indexdom  38069  filbcmb  38075  sdclem2  38077  fdc  38080  lmclim2  38093  caures  38095  istotbnd  38104  istotbnd3  38106  sstotbnd  38110  isbnd  38115  heibor  38156  bfp  38159  rrncmslem  38167  isgrpda  38290  idlval  38348  isidl  38349  0idl  38360  unichnidl  38366  pridl  38372  ismaxidl  38375  smprngopr  38387  igenval2  38401  prnc  38402  ispridlc  38405  scottexf  38503  scott0f  38504  disjsuc2  38749  riotasvd  39416  islfl  39520  eqlkr  39559  eqlkr3  39561  glbconN  39837  hlsuprexch  39841  ispsubsp  40205  ldilset  40569  isldil  40570  dilsetN  40613  isdilN  40614  trlset  40621  trlval  40622  cdleme27b  40828  cdleme29b  40835  cdleme31so  40839  cdleme31sn1  40841  cdleme31sn1c  40848  cdleme31fv  40850  cdleme40v  40929  istendo  41220  cdlemkid3N  41393  cdlemkid4  41394  cdlemkid5  41395  dihfval  41691  dihval  41692  islpolN  41943  hdmapffval  42286  hdmapfval  42287  hdmapval  42288  hdmapval2lem  42291  hgmapffval  42345  hgmapfval  42346  hgmapval  42347  hgmapvs  42351  isprimroot  42546  aks6d1c1p1  42560  hashscontpow1  42574  sticksstones2  42600  unitscyglem3  42650  exfinfldd  42656  qsalrel  42694  supinf  42695  sn-sup2  42950  fsuppind  43037  isnacs  43150  isnacs2  43152  nacsfix  43158  mzpclval  43171  elmzpcl  43172  rencldnfilem  43266  infmrgelbi  43324  pellfundre  43327  pellfundlb  43330  wepwsolem  43488  fnwe2lem2  43497  aomclem8  43507  dfac11  43508  gicabl  43545  islnr3  43561  hbtlem2  43570  hbtlem5  43574  onintunirab  43673  onsucf1lem  43715  cantnfresb  43770  safesnsupfilb  43863  rp-brsslt  43868  fiinfi  44018  clsk1independent  44491  ntrclsk13  44516  gneispacess2  44591  imo72b2lem0  44610  imo72b2lem2  44612  imo72b2lem1  44614  imo72b2  44617  scottelrankd  44692  mnuop23d  44711  ismnushort  44746  ralabsobidv  45417  0elaxnul  45428  pwclaxpow  45429  prclaxpr  45430  uniclaxun  45431  omssaxinf2  45433  modelac8prim  45437  wfac8prim  45447  permac8prim  45459  evth2f  45464  evthf  45476  fnchoice  45478  uzwo4  45502  wessf1ornlem  45633  disjinfi  45640  rnmptlb  45690  rnmptbdd  45692  rnmptbd2  45696  rnmptbd  45703  dstregt0  45733  upbdrech2  45759  rexabslelem  45864  rexabsle  45865  uzub  45877  infrpgernmpt  45911  mccl  46046  ellimcabssub0  46065  climf  46070  clim2f  46082  limsupre  46087  clim2cf  46096  clim0cf  46100  climf2  46112  clim2f2  46116  clim2d  46119  limsupref  46131  limsupbnd1f  46132  climinf2  46153  limsuppnf  46157  climinfmpt  46161  climinf3  46162  limsupubuzmpt  46165  limsupmnf  46167  limsupre2lem  46170  limsupre2  46171  limsupmnfuzlem  46172  limsupmnfuz  46173  limsupre2mpt  46176  limsupre3lem  46178  limsupre3  46179  limsupre3mpt  46180  limsupre3uz  46182  limsupreuz  46183  limsupreuzmpt  46185  climuz  46190  liminfreuzlem  46248  liminfreuz  46249  cnrefiisplem  46275  xlimmnfvlem1  46278  xlimmnfv  46280  xlimpnfvlem1  46282  xlimpnfv  46284  xlimmnfmpt  46289  xlimpnfmpt  46290  cncfshift  46320  cncfperiod  46325  fperdvper  46365  dvbdfbdioo  46376  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnprodlem3  46394  stoweidlem5  46451  stoweidlem9  46455  stoweidlem15  46461  stoweidlem16  46462  stoweidlem27  46473  stoweidlem28  46474  stoweidlem31  46477  stoweidlem34  46480  stoweidlem37  46483  stoweidlem46  46492  stoweidlem48  46494  stoweidlem51  46497  stoweidlem52  46498  stoweidlem59  46505  wallispilem3  46513  stirlinglem13  46532  fourierdlem2  46555  fourierdlem3  46556  fourierdlem16  46569  fourierdlem20  46573  fourierdlem21  46574  fourierdlem22  46575  fourierdlem25  46578  fourierdlem39  46592  fourierdlem42  46595  fourierdlem54  46606  fourierdlem64  46616  fourierdlem77  46629  fourierdlem83  46635  fourierdlem103  46655  fourierdlem104  46656  subsaliuncllem  46803  iundjiun  46906  meaiunincf  46929  caragenval  46939  isome  46940  caragenel  46941  omessle  46944  ovnlerp  47008  hoidmvlelem3  47043  hoidmvle  47046  issmflem  47173  issmfgt  47202  smfmullem2  47238  smfmullem4  47240  smfmul  47241  smfsuplem2  47258  smfsup  47260  smfinflem  47263  smfinf  47264  fsupdm  47288  finfdm  47292  cfsetsnfsetf  47518  cbvral2  47563  2reu8i  47573  2reuimp0  47574  dfdfat2  47588  iccpart  47888  iccpartigtl  47895  paireqne  47983  reupr  47994  perfectALTVlem2  48210  bgoldbachlt  48301  tgoldbachlt  48304  grimidvtxedg  48373  grimcnv  48376  grimco  48377  isuspgrim0  48382  gricushgr  48405  ushggricedg  48415  uhgrimisgrgric  48419  isubgr3stgr  48463  isgrlim  48470  isgrlim2  48471  uspgrlim  48480  grlicsym  48501  grlictr  48503  gpg5nbgrvtx03star  48568  gpg5nbgr3star  48569  pgnbgreunbgr  48613  upwlksfval  48623  nn0mnd  48667  uzlidlring  48723  ply1mulgsumlem1  48874  ply1mulgsumlem2  48875  linindslinci  48936  lindslinindsimp1  48945  lindslinindsimp2lem5  48950  lindslinindsimp2  48951  linds0  48953  lindsrng01  48956  snlindsntor  48959  lmod1  48980  ldepsnlinc  48996  bigoval  49037  elbigo2r  49041  nn0sumshdiglem2  49110  eenglngeehlnmlem1  49225  eenglngeehlnmlem2  49226  lubeldm2d  49445  glbeldm2d  49446  lubsscl  49447  glbsscl  49448  ipolubdm  49474  ipolub  49475  ipoglbdm  49477  ipoglb  49478  nelsubc3lem  49557  upfval2  49664  upfval3  49665  isthincd2lem2  49922  setc1onsubc  50089  cnelsubclem  50090  setrec1lem2  50175