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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2144  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932

This theorem depends on definitions:  df-bi 209  df-an 400  df-ral 3079

This theorem is referenced by:  2ralbidv  3228  rexralbidv  3230  3ralbidv  3231  4ralbidv  3232  cbvral2vw  3246  cbvral4vw  3249  cbvral2v  3357  rspceaimv  3589  rspc2  3592  rspc2v  3594  rspc3v  3599  rspc4v  3603  reu6i  3693  reu7  3697  sbcralt  3827  reu8nf  3832  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  5098  disjxun  5100  brralrspcev  5162  reusv2lem2  5358  reusv3  5364  poeq1  5560  solin  5584  somo  5596  frirr  5625  fr2nr  5626  frminex  5628  wereu2  5646  posn  5735  frsn  5737  ralxpf  5820  cnvpo  6276  reu3op  6281  reuop  6282  dfpo2  6285  frpomin  6329  fnmptfvd  7024  iinpreima  7052  dff4  7084  dff13f  7241  fpropnf1  7253  f1ounsn  7258  eusvobj2  7390  ovanraleqv  7422  f1opr  7454  ofreq  7666  sorpssuni  7717  sorpssint  7718  fr3nr  7757  onssmin  7777  funcnvuni  7915  f1oweALT  7955  frxp  8108  frxp2  8126  xpord2indlem  8129  frxp3  8133  xpord3inddlem  8136  poseq  8140  soseq  8141  frecseq123  8265  csbfrecsg  8267  frrlem1  8269  frrlem13  8281  smoeq  8323  tfrlem12  8362  tz7.48lem  8414  naddcllem  8648  naddov2  8651  naddunif  8666  naddasslem1  8667  naddasslem2  8668  elixp2  8885  undifixp  8918  xpf1o  9113  nneneq  9176  ac6sfi  9230  frfi  9231  fipreima  9303  indexfi  9305  marypha1lem  9381  marypha1  9382  supeq1  9393  supeq3  9397  supmo  9400  eqsup  9404  supub  9407  suplub  9408  sup0  9415  supisoex  9423  eqinf  9433  infval  9435  infmo  9445  oieq1  9462  ordtypecbv  9467  ordtypelem3  9470  ordtypelem6  9473  ordtypelem7  9474  ordtypelem9  9476  wemaplem1  9496  wemaplem2  9497  zfregcl  9544  zfregclOLD  9545  oemapval  9640  oemapvali  9641  cantnf  9650  wemapwe  9654  ttrcleq  9666  ttrcltr  9673  ttrclss  9677  ttrclselem2  9683  rankval3b  9786  unbndrank  9802  rankunb  9810  rankuni2b  9813  tcrank  9844  scottex  9845  scottexs  9847  scott0s  9848  bnd2  9853  updjud  9894  dfac8clem  9990  ac5num  9994  acni  10003  acni2  10004  alephval3  10068  dfac4  10080  dfac5lem5  10085  dfac5  10087  dfac2a  10088  dfac2b  10089  dfacacn  10100  kmlem2  10110  kmlem13  10121  cflem  10203  cflemOLD  10204  cflecard  10211  cfeq0  10215  cfsuc  10216  cfflb  10218  cofsmo  10228  cfsmolem  10229  cfcoflem  10231  coftr  10232  alephsing  10235  fin23lem11  10276  isfin3ds  10288  fin23lem17  10297  fin23lem39  10309  isf33lem  10325  isf34lem6  10339  fin1a2lem13  10371  hsmexlem4  10388  hsmex  10391  axcc2lem  10395  axcc3  10397  dcomex  10406  axdc2lem  10407  axdc3lem2  10410  axdc3lem3  10411  axdc3  10413  axdc4lem  10414  axcclem  10416  zorn2lem2  10456  zorn2lem7  10461  zorn2g  10462  zornn0g  10464  ttukeylem7  10474  axdclem2  10479  brdom3  10487  brdom7disj  10490  brdom6disj  10491  alephval2  10532  inar1  10735  axgroth6  10788  pinq  10887  nqereu  10889  prlem934  10993  supexpr  11014  supsrlem  11071  axpre-sup  11129  dedekind  11348  dedekindle  11349  fiminre2  12142  lbreu  12144  sup2  12150  infm3  12153  nnsub  12259  uzwo  12914  nnwof  12917  ublbneg  12936  lbzbi  12939  zsupss  12940  uzsupss  12943  uzwo3  12946  zmax  12948  rpnnen1lem1  12981  rpnnen1lem3  12982  rpnnen1lem4  12983  rpnnen1lem5  12984  xrsupsslem  13312  xrinfmsslem  13313  xrsupss  13314  xrinfmss  13315  flval2  13826  axdc4uzlem  13998  ssnn0fi  14000  fsuppmapnn0fiubex  14007  faclbnd4lem4  14311  bccl  14337  hashgt12el  14437  hashbc  14468  hashge2el2dif  14495  wrdind  14737  wrd2ind  14738  rexanre  15376  rexico  15383  cau4  15386  reusq0  15494  clim  15523  rlim  15524  rlim2  15525  clim2  15533  clim2c  15534  clim0c  15536  rlim0  15537  rlim0lt  15538  ello12r  15546  ello1d  15552  elo12r  15557  rlimresb  15594  rlimcld2  15607  climabs0  15614  rlimo1  15646  lo1add  15656  lo1mul  15657  isercoll  15697  incexclem  15868  sqrt2irr  16283  gcdcllem1  16535  gcdcllem2  16536  dfgcd2  16582  fissn0dvds  16655  dvdslcmf  16667  lcmfledvds  16668  lcmf  16669  lcmfunsnlem1  16673  lcmfunsnlem2lem1  16674  lcmfunsnlem  16677  lcmfdvds  16678  reumodprminv  16842  pc2dvds  16917  pcz  16919  prmpwdvds  16942  infpn2  16951  prmreclem2  16955  prmreclem3  16956  prmreclem5  16958  prmreclem6  16959  vdwlem6  17024  vdwlem8  17026  vdwlem13  17031  vdwnnlem1  17033  vdwnn  17036  ramcl  17067  cshwrepswhash1  17140  prdsleval  17508  imasval  17543  imasaddfnlem  17560  imasvscafn  17569  mrisval  17664  isacs  17685  isacs2  17687  isacs1i  17691  mreacs  17692  acsfn  17693  acsfn2  17697  iscatd  17707  catidex  17708  catideu  17709  cidval  17711  catidd  17714  comfeq  17740  catpropd  17743  ismon  17768  isfunc  17899  isnat  17985  isinito  18031  istermo  18032  isprs  18330  drsdirfi  18339  ispos  18348  lubfval  18382  lubeldm  18385  lubval  18388  lubprop  18390  lublecllem  18392  glbfval  18395  glbeldm  18398  glbval  18401  glbprop  18403  joinval2lem  18412  joinlem  18415  meetval2lem  18426  meetlem  18429  poslubmo  18443  posglbmo  18444  poslubd  18445  resspos  18463  isglbd  18543  lubl  18546  lubun  18549  clatleglb  18552  isdlat  18556  ipodrsima  18575  chneq1  18646  mgm1  18694  gsumval2  18722  mgmhmima  18751  sgrp1  18765  mhmimalem  18860  mndind  18864  gsumwspan  18882  efmndmnd  18925  smndex1mnd  18949  sgrp2rid2  18965  sgrp2rid2ex  18966  sgrp2nmndlem4  18967  pwmnd  18976  dfgrp2  19006  isgrpinv  19037  grpidinv  19042  dfgrp3lem  19082  issubg4  19189  isnsg2  19199  nsgacs  19205  elnmz  19206  cycsubgcl  19249  ghmrn  19271  ghmnsgima  19282  isga  19333  orbsta  19355  cntzfval  19362  elcntz  19364  resscntz  19375  oppgsubg  19405  symgextfo  19464  gsmsymgreqlem2  19473  gsmsymgreq  19474  pmtrdifel  19522  pmtrdifwrdellem3  19525  pmtrdifwrdel2  19528  psgnunilem2  19537  psgnunilem3  19538  odeq  19592  gexid  19623  gexlem2  19624  gexdvds  19626  isslw  19650  sylow2alem1  19659  sylow2alem2  19660  efgval  19759  efgrelexlemb  19792  efgcpbllemb  19797  abl1  19908  dmdprd  20042  dprd2da  20086  pgpfac1lem5  20123  isomnd  20165  ring1  20362  rngisomring  20518  lringuplu  20596  rhmimasubrnglem  20617  isrrg  20750  isabv  20862  islss  21003  lssacs  21036  reslmhm  21121  islbs  21145  pj1lmhm  21169  lbsacsbs  21228  rnglidlmcl  21288  rnglidl0  21301  zringlpir  21521  psgndiflemA  21655  ocvfval  21720  elocv  21722  iunocv  21735  frlmlbs  21851  islindf  21866  islinds2  21867  islindf2  21868  lindfrn  21875  lsslindf  21884  islindf4  21892  opsrval  22101  ply1coe  22363  cply1coe0bi  22367  mat0dimcrng  22532  mdetunilem1  22674  mdetunilem9  22682  cpmat  22771  cpmatel  22773  1elcpmat  22777  m2cpminvid2lem  22816  basgen2  23051  bastop1  23055  isclo  23149  ordtbaslem  23250  iscn  23297  cnpval  23298  iscnp  23299  iscnp3  23306  lmbr  23320  lmbr2  23321  lmbrf  23322  cnprest  23351  cnprest2  23352  t0sep  23386  isreg  23394  t1sep2  23431  tgcmp  23463  1stcclb  23506  1stcfb  23507  2ndc1stc  23513  1stcrest  23515  2ndcdisj  23518  islly  23530  isnlly  23531  lly1stc  23558  isref  23571  islocfin  23579  elkgen  23598  kgencn  23618  elpt  23634  elptr  23635  ptcnplem  23683  tx1stc  23712  cnmpt21  23733  kqt0lem  23798  isr0  23799  regr1lem2  23802  r0sep  23810  nrmr0reg  23811  flffbas  24057  cnflf  24064  cnflf2  24065  lmflf  24067  txflf  24068  fclsopni  24077  fclsnei  24081  fclsrest  24086  fcfnei  24097  cnfcf  24104  alexsubb  24108  alexsubALTlem3  24111  qustgplem  24183  tsmsfbas  24190  tsmsres  24206  tsmsf1o  24207  tsmsxplem1  24215  ustval  24265  isust  24266  ustincl  24270  ustdiag  24271  ustinvel  24272  ustexhalf  24273  ust0  24282  utopval  24294  ucnval  24338  isucn  24339  isucn2  24340  ucnima  24342  iscfilu  24349  ispsmet  24366  ismet  24385  isxmet  24386  imasdsf1olem  24435  imasf1oxmet  24437  imasf1omet  24438  metss  24570  met1stc  24583  prdsxmslem2  24591  txmetcnp  24609  metucn  24633  tngngp3  24718  nlmvscn  24749  nmoval  24777  nmolb  24779  qtopbaslem  24820  cncfval  24952  elcncf2  24954  mulc1cncf  24969  cncfmet  24973  evth  25023  lebnumlem3  25027  lebnum  25028  xlebnum  25029  ishtpy  25036  isphtpy  25045  pi1xfr  25119  pi1coghm  25125  isclmp  25161  ipcn  25310  lmmbr2  25323  lmmbr3  25324  lmmbrf  25326  cfilfval  25328  iscfil  25329  fmcfil  25336  caufval  25339  iscau  25340  iscau2  25341  iscau3  25342  iscau4  25343  iscauf  25344  caucfil  25347  cfilresi  25359  causs  25362  lmclim  25367  cmetcusp1  25417  minveclem4c  25489  minveclem2  25490  minveclem3b  25492  minveclem4  25496  minveclem6  25498  minveclem7  25499  ovolicc2lem3  25583  ismbl  25590  dyadmax  25662  dyadmbllem  25663  dyadmbl  25664  opnmbllem  25665  ismbf1  25688  ismbf  25692  mbfeqalem2  25706  mbflimsup  25730  mbfi1fseqlem6  25784  mbfi1flimlem  25786  itg2seq  25806  itg2monolem1  25814  isibl  25829  ply1divex  26199  fta1g  26232  dgrco  26337  plydivex  26363  fta1  26374  vieta1  26378  aannenlem1  26394  aannenlem2  26395  aalioulem2  26399  aalioulem3  26400  ulmval  26445  ulm2  26450  ulmi  26451  ulmres  26453  ulmshftlem  26454  ulmcaulem  26459  ulmcau  26460  ulmss  26462  ulmbdd  26463  ulmdvlem1  26465  ulmdvlem3  26467  pilem2  26517  pilem3  26518  cxpcn3  26815  dmarea  27024  rlimcnp  27032  scvxcvx  27052  lgamgulmlem2  27096  lgamgulmlem3  27097  lgamgulmlem5  27099  lgambdd  27103  lgamcvglem  27106  isppw2  27181  perfectlem2  27296  2sqlem6  27489  2sqlem10  27494  addsq2reu  27506  2sqreulem1  27512  2sqreunnlem1  27515  dchrisumlema  27554  dchrisumlem2  27556  dchrisumlem3  27557  pntpbnd  27654  pntibndlem3  27658  pntibnd  27659  pntleme  27674  pntlem3  27675  pntlemp  27676  pnt3  27678  ltsval  27713  nosupprefixmo  27766  noinfprefixmo  27767  nosupcbv  27768  nosupno  27769  nosupdm  27770  nosupfv  27772  nosupres  27773  nosupbnd1lem1  27774  nosupbnd1lem3  27776  nosupbnd1lem5  27778  noinfcbv  27783  noinfno  27784  noinfdm  27785  noinffv  27787  noinfres  27788  noinfbnd1lem3  27791  noinfbnd1lem5  27793  noetalem1  27807  noetalem2  27808  nocvxminlem  27849  brslts  27857  sltssnb  27864  conway  27874  etaslts  27888  lesrec  27894  eqcuts3  27899  madebdaylemlrcut  27994  madebday  27995  bdayle  28011  cofcutr  28019  cutmax  28029  cutmin  28030  lrrecfr  28038  addsprop  28071  negsunif  28150  addonbday  28374  onsfi  28451  n0subs  28458  bdayn0p1  28464  bdaypw2n0bndlem  28558  bdayfinbndlem2  28563  z12zsodd  28577  istrkgld  28630  axtg5seg  28636  tgcgr4  28702  perpln1  28885  perpln2  28886  isperp  28887  brbtwn2  29108  colinearalg  29113  axsegconlem1  29120  axsegcon  29130  ax5seglem4  29135  ax5seglem5  29136  axlowdim  29164  axeuclidlem  29165  axcontlem1  29167  axcontlem2  29168  axcontlem4  29170  axcontlem5  29171  axcontlem8  29174  axcontlem12  29178  elntg2  29188  uvtxusgr  29605  rgrx0ndm  29796  ewlksfval  29804  wksfval  29812  wwlks  30037  wlkiswwlks2  30077  clwwlk  30187  1conngr  30398  frgrwopregasn  30520  frgrwopregbsn  30521  frgrwopreglem5ALT  30526  frgrregord013  30599  isgrpo  30702  isgrpoi  30703  grpoideu  30714  grpoidinv2  30720  vciOLD  30766  isvclem  30782  cnidOLD  30787  isnvlem  30815  nvi  30819  lnoval  30957  islno  30958  isblo3i  31006  blo3i  31007  blocnilem  31009  ajfval  31014  ubthlem1  31075  ubthlem2  31076  ubthlem3  31077  ubth  31078  minvecolem2  31080  minvecolem3  31081  minvecolem4c  31084  minvecolem4  31085  minvecolem5  31086  minvecolem6  31087  minvecolem7  31088  h2hcau  31184  h2hlm  31185  hilid  31366  hcau  31389  hlimi  31393  hlim2  31397  ocel  31486  adjsym  32038  ellnop  32063  ellnfn  32088  hhcno  32109  hhcnf  32110  lnopeq  32214  elunop2  32218  lnophm  32224  lnconi  32238  lnopcnbd  32241  lnfncnbd  32262  imaelshi  32263  riesz3i  32267  riesz4i  32268  riesz4  32269  riesz1  32270  cnlnadjlem2  32273  cnlnadjlem5  32276  cnlnadjlem8  32279  cnlnadji  32281  nmopadjlei  32293  cnvbraval  32315  leopg  32327  leoppos  32331  mdbr  32499  dmdbr  32504  cdj3i  32646  disjunsn  32796  funcnv5mpt  32871  fgreu  32875  fcnvgreu  32876  xrge0infss  32964  wrdt2ind  33133  mgccole1  33170  mgccole2  33171  mgcmnt1  33172  mgcmnt2  33173  gsumhashmul  33249  isfxp  33350  fxpgaeq  33351  inftmrel  33362  isinftm  33363  archiabl  33380  isarchiofld  33381  elrgspnlem4  33428  0nellinds  33558  lindssn  33566  elrspunidl  33616  prmidl  33628  ismxidl  33652  1arithidom  33735  1arithufdlem3  33744  evl1deg1  33774  evl1deg2  33775  evl1deg3  33776  vietalem  33878  vieta  33879  crefeq  34144  zarcmplem  34180  esum2d  34392  sigaval  34410  issgon  34422  isrnmeas  34499  ismbfm  34550  mbfmcst  34558  elcarsg  34604  sitgval  34631  eulerpartlemd  34665  ballotleme  34796  tgoldbachgt  34959  bnj1185  35090  bnj1385  35129  bnj66  35157  bnj106  35165  bnj155  35176  bnj852  35218  bnj893  35225  bnj1228  35308  bnj1234  35310  bnj1463  35352  nummin  35391  rankfilimbi  35401  r1omhfb  35412  fineqvnttrclse  35424  r1omhfbregs  35437  gblacfnacd  35449  onvf1odlem4  35453  vonf1wev  35455  vonf1owevOLD  35457  derangenlem  35526  subfacp1lem3  35537  subfacp1lem5  35539  subfacp1lem6  35540  subfacp1  35541  erdszelem8  35553  kur14  35571  cnpconn  35585  resconn  35601  cvmscbv  35613  iscvm  35614  cvmsi  35620  cvmsval  35621  cvmlift3lem2  35675  snmlval  35686  satfv1  35718  fmlasucdisj  35754  satffunlem1lem1  35757  satffunlem2lem1  35759  satfv1fvfmla1  35778  mclsssvlem  35917  mclsval  35918  mclsax  35924  mclsind  35925  dfon2lem9  36144  dfrdg2  36148  dfrdg3  36149  fwddifnval  36518  nmulprop  36545  nn0prpwlem  36687  isfne  36704  isfne4  36705  isfne2  36707  isfne3  36708  neibastop3  36727  topmeet  36729  topjoin  36730  filnetlem4  36746  weiunlem  36828  weiunfrlem  36829  dfttc4lem1  36893  dfttc4  36895  elttcirr  36896  unblimceq0lem  36949  unblimceq0  36950  unbdqndv2  36954  taupilemrplb  37817  fin2so  38111  lindsadd  38117  matunitlindflem2  38121  ptrecube  38124  poimirlem2  38126  poimirlem3  38127  poimirlem4  38128  poimirlem24  38148  poimirlem25  38149  poimirlem26  38150  poimirlem27  38151  poimirlem28  38152  poimirlem29  38153  poimirlem30  38154  poimirlem32  38156  poimir  38157  heicant  38159  mblfinlem1  38161  mblfinlem2  38162  voliunnfl  38168  volsupnfl  38169  mbfresfi  38170  itg2addnc  38178  upixp  38233  indexdom  38238  filbcmb  38244  sdclem2  38246  fdc  38249  lmclim2  38262  caures  38264  istotbnd  38273  istotbnd3  38275  sstotbnd  38279  isbnd  38284  heibor  38325  bfp  38328  rrncmslem  38336  isgrpda  38459  idlval  38517  isidl  38518  0idl  38529  unichnidl  38535  pridl  38541  ismaxidl  38544  smprngopr  38556  igenval2  38570  prnc  38571  ispridlc  38574  scottexf  38672  scott0f  38673  disjsuc2  38918  riotasvd  39585  islfl  39689  eqlkr  39728  eqlkr3  39730  glbconN  40006  hlsuprexch  40010  ispsubsp  40374  ldilset  40738  isldil  40739  dilsetN  40782  isdilN  40783  trlset  40790  trlval  40791  cdleme27b  40997  cdleme29b  41004  cdleme31so  41008  cdleme31sn1  41010  cdleme31sn1c  41017  cdleme31fv  41019  cdleme40v  41098  istendo  41389  cdlemkid3N  41562  cdlemkid4  41563  cdlemkid5  41564  dihfval  41860  dihval  41861  islpolN  42112  hdmapffval  42455  hdmapfval  42456  hdmapval  42457  hdmapval2lem  42460  hgmapffval  42514  hgmapfval  42515  hgmapval  42516  hgmapvs  42520  isprimroot  42715  aks6d1c1p1  42729  hashscontpow1  42743  sticksstones2  42769  unitscyglem3  42819  exfinfldd  42825  qsalrel  42862  supinf  42863  sn-sup2  43118  fsuppind  43177  isnacs  43290  isnacs2  43292  nacsfix  43298  mzpclval  43311  elmzpcl  43312  rencldnfilem  43402  infmrgelbi  43460  pellfundre  43463  pellfundlb  43466  wepwsolem  43624  fnwe2lem2  43633  aomclem8  43643  dfac11  43644  gicabl  43681  islnr3  43697  hbtlem2  43706  hbtlem5  43710  onintunirab  43809  onsucf1lem  43851  cantnfresb  43906  safesnsupfilb  43999  rp-brsslt  44004  fiinfi  44154  clsk1independent  44627  ntrclsk13  44652  gneispacess2  44727  imo72b2lem0  44746  imo72b2lem2  44748  imo72b2lem1  44750  imo72b2  44753  scottelrankd  44828  mnuop23d  44847  ismnushort  44882  ralabsobidv  45553  0elaxnul  45564  pwclaxpow  45565  prclaxpr  45566  uniclaxun  45567  omssaxinf2  45569  modelac8prim  45573  wfac8prim  45583  permac8prim  45595  evth2f  45600  evthf  45612  fnchoice  45614  uzwo4  45638  wessf1ornlem  45768  disjinfi  45775  rnmptlb  45823  rnmptbdd  45825  rnmptbd2  45829  rnmptbd  45836  dstregt0  45866  upbdrech2  45892  rexabslelem  45997  rexabsle  45998  uzub  46010  infrpgernmpt  46044  mccl  46179  ellimcabssub0  46198  climf  46203  clim2f  46215  limsupre  46220  clim2cf  46229  clim0cf  46233  climf2  46245  clim2f2  46249  clim2d  46252  limsupref  46264  limsupbnd1f  46265  climinf2  46286  limsuppnf  46290  climinfmpt  46294  climinf3  46295  limsupubuzmpt  46298  limsupmnf  46300  limsupre2lem  46303  limsupre2  46304  limsupmnfuzlem  46305  limsupmnfuz  46306  limsupre2mpt  46309  limsupre3lem  46311  limsupre3  46312  limsupre3mpt  46313  limsupre3uz  46315  limsupreuz  46316  limsupreuzmpt  46318  climuz  46323  liminfreuzlem  46381  liminfreuz  46382  cnrefiisplem  46408  xlimmnfvlem1  46411  xlimmnfv  46413  xlimpnfvlem1  46415  xlimpnfv  46417  xlimmnfmpt  46422  xlimpnfmpt  46423  cncfshift  46453  cncfperiod  46458  fperdvper  46498  dvbdfbdioo  46509  ioodvbdlimc1lem2  46511  ioodvbdlimc2lem  46513  dvnprodlem3  46527  stoweidlem5  46584  stoweidlem9  46588  stoweidlem15  46594  stoweidlem16  46595  stoweidlem27  46606  stoweidlem28  46607  stoweidlem31  46610  stoweidlem34  46613  stoweidlem37  46616  stoweidlem46  46625  stoweidlem48  46627  stoweidlem51  46630  stoweidlem52  46631  stoweidlem59  46638  wallispilem3  46646  stirlinglem13  46665  fourierdlem2  46688  fourierdlem3  46689  fourierdlem16  46702  fourierdlem20  46706  fourierdlem21  46707  fourierdlem22  46708  fourierdlem25  46711  fourierdlem39  46725  fourierdlem42  46728  fourierdlem54  46739  fourierdlem64  46749  fourierdlem77  46762  fourierdlem83  46768  fourierdlem103  46788  fourierdlem104  46789  subsaliuncllem  46936  iundjiun  47039  meaiunincf  47062  caragenval  47072  isome  47073  caragenel  47074  omessle  47077  ovnlerp  47141  hoidmvlelem3  47176  hoidmvle  47179  issmflem  47306  issmfgt  47335  smfmullem2  47371  smfmullem4  47373  smfmul  47374  smfsuplem2  47391  smfsup  47393  smfinflem  47396  smfinf  47397  fsupdm  47421  finfdm  47425  cfsetsnfsetf  47657  cbvral2  47702  2reu8i  47712  2reuimp0  47713  dfdfat2  47727  iccpart  48027  iccpartigtl  48034  paireqne  48122  reupr  48133  perfectALTVlem2  48349  bgoldbachlt  48440  tgoldbachlt  48443  grimidvtxedg  48512  grimcnv  48515  grimco  48516  isuspgrim0  48521  gricushgr  48544  ushggricedg  48554  uhgrimisgrgric  48558  isubgr3stgr  48602  isgrlim  48609  isgrlim2  48610  uspgrlim  48619  grlicsym  48640  grlictr  48642  gpg5nbgrvtx03star  48707  gpg5nbgr3star  48708  pgnbgreunbgr  48752  upwlksfval  48762  nn0mnd  48806  uzlidlring  48862  ply1mulgsumlem1  49013  ply1mulgsumlem2  49014  linindslinci  49075  lindslinindsimp1  49084  lindslinindsimp2lem5  49089  lindslinindsimp2  49090  linds0  49092  lindsrng01  49095  snlindsntor  49098  lmod1  49119  ldepsnlinc  49135  bigoval  49176  elbigo2r  49180  nn0sumshdiglem2  49249  eenglngeehlnmlem1  49364  eenglngeehlnmlem2  49365  lubeldm2d  49584  glbeldm2d  49585  lubsscl  49586  glbsscl  49587  ipolubdm  49613  ipolub  49614  ipoglbdm  49616  ipoglb  49617  nelsubc3lem  49696  upfval2  49803  upfval3  49804  isthincd2lem2  50061  setc1onsubc  50228  cnelsubclem  50229  setrec1lem2  50314