Theorem ralbidv 3158

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  ∀wral 3050

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 3051

This theorem is referenced by:  2ralbidv  3199  rexralbidv  3201  3ralbidv  3202  4ralbidv  3203  cbvral2vw  3217  cbvral4vw  3220  cbvral2v  3337  rspceaimv  3581  rspc2  3584  rspc2v  3586  rspc3v  3591  rspc4v  3595  reu6i  3685  reu7  3689  sbcralt  3821  reu8nf  3826  raaan  4470  raaanv  4471  raaan2  4474  2reu4lem  4475  reusngf  4630  2ralsng  4634  rexreusng  4635  reuprg0  4658  issn  4787  2ralunsn  4850  elintg  4909  elintrabg  4915  eliin  4950  disjprg  5093  disjxun  5095  brralrspcev  5157  reusv2lem2  5343  reusv3  5349  poeq1  5534  solin  5558  somo  5570  frirr  5599  fr2nr  5600  frminex  5602  wereu2  5620  posn  5709  frsn  5711  ralxpf  5794  cnvpo  6244  reu3op  6249  reuop  6250  dfpo2  6253  frpomin  6297  fnmptfvd  6986  iinpreima  7014  dff4  7046  dff13f  7201  fpropnf1  7213  f1ounsn  7218  eusvobj2  7350  ovanraleqv  7382  f1opr  7414  ofreq  7626  sorpssuni  7677  sorpssint  7678  fr3nr  7717  onssmin  7737  funcnvuni  7874  f1oweALT  7916  frxp  8068  frxp2  8086  xpord2indlem  8089  frxp3  8093  xpord3inddlem  8096  poseq  8100  soseq  8101  frecseq123  8224  csbfrecsg  8226  frrlem1  8228  frrlem13  8240  smoeq  8282  tfrlem12  8320  tz7.48lem  8372  naddcllem  8604  naddov2  8607  naddunif  8621  naddasslem1  8622  naddasslem2  8623  elixp2  8841  undifixp  8874  xpf1o  9069  nneneq  9132  ac6sfi  9186  frfi  9187  fipreima  9260  indexfi  9262  marypha1lem  9338  marypha1  9339  supeq1  9350  supeq3  9354  supmo  9357  eqsup  9361  supub  9364  suplub  9365  sup0  9372  supisoex  9380  eqinf  9390  infval  9392  infmo  9402  oieq1  9419  ordtypecbv  9424  ordtypelem3  9427  ordtypelem6  9430  ordtypelem7  9431  ordtypelem9  9433  wemaplem1  9453  wemaplem2  9454  zfregcl  9501  zfregclOLD  9502  oemapval  9594  oemapvali  9595  cantnf  9604  wemapwe  9608  ttrcleq  9620  ttrcltr  9627  ttrclss  9631  ttrclselem2  9637  rankval3b  9740  unbndrank  9756  rankunb  9764  rankuni2b  9767  tcrank  9798  scottex  9799  scottexs  9801  scott0s  9802  bnd2  9807  updjud  9848  dfac8clem  9944  ac5num  9948  acni  9957  acni2  9958  alephval3  10022  dfac4  10034  dfac5lem5  10039  dfac5  10041  dfac2a  10042  dfac2b  10043  dfacacn  10054  kmlem2  10064  kmlem13  10075  cflem  10157  cflemOLD  10158  cflecard  10165  cfeq0  10168  cfsuc  10169  cfflb  10171  cofsmo  10181  cfsmolem  10182  cfcoflem  10184  coftr  10185  alephsing  10188  fin23lem11  10229  isfin3ds  10241  fin23lem17  10250  fin23lem39  10262  isf33lem  10278  isf34lem6  10292  fin1a2lem13  10324  hsmexlem4  10341  hsmex  10344  axcc2lem  10348  axcc3  10350  dcomex  10359  axdc2lem  10360  axdc3lem2  10363  axdc3lem3  10364  axdc3  10366  axdc4lem  10367  axcclem  10369  zorn2lem2  10409  zorn2lem7  10414  zorn2g  10415  zornn0g  10417  ttukeylem7  10427  axdclem2  10432  brdom3  10440  brdom7disj  10443  brdom6disj  10444  alephval2  10485  inar1  10688  axgroth6  10741  pinq  10840  nqereu  10842  prlem934  10946  supexpr  10967  supsrlem  11024  axpre-sup  11082  dedekind  11298  dedekindle  11299  fiminre2  12092  lbreu  12094  sup2  12100  infm3  12103  nnsub  12191  uzwo  12826  nnwof  12829  ublbneg  12848  lbzbi  12851  zsupss  12852  uzsupss  12855  uzwo3  12858  zmax  12860  rpnnen1lem1  12893  rpnnen1lem3  12894  rpnnen1lem4  12895  rpnnen1lem5  12896  xrsupsslem  13224  xrinfmsslem  13225  xrsupss  13226  xrinfmss  13227  flval2  13736  axdc4uzlem  13908  ssnn0fi  13910  fsuppmapnn0fiubex  13917  faclbnd4lem4  14221  bccl  14247  hashgt12el  14347  hashbc  14378  hashge2el2dif  14405  wrdind  14647  wrd2ind  14648  rexanre  15272  rexico  15279  cau4  15282  reusq0  15390  clim  15419  rlim  15420  rlim2  15421  clim2  15429  clim2c  15430  clim0c  15432  rlim0  15433  rlim0lt  15434  ello12r  15442  ello1d  15448  elo12r  15453  rlimresb  15490  rlimcld2  15503  climabs0  15510  rlimo1  15542  lo1add  15552  lo1mul  15553  isercoll  15593  incexclem  15761  sqrt2irr  16176  gcdcllem1  16428  gcdcllem2  16429  dfgcd2  16475  fissn0dvds  16548  dvdslcmf  16560  lcmfledvds  16561  lcmf  16562  lcmfunsnlem1  16566  lcmfunsnlem2lem1  16567  lcmfunsnlem  16570  lcmfdvds  16571  reumodprminv  16734  pc2dvds  16809  pcz  16811  prmpwdvds  16834  infpn2  16843  prmreclem2  16847  prmreclem3  16848  prmreclem5  16850  prmreclem6  16851  vdwlem6  16916  vdwlem8  16918  vdwlem13  16923  vdwnnlem1  16925  vdwnn  16928  ramcl  16959  cshwrepswhash1  17032  prdsleval  17399  imasval  17434  imasaddfnlem  17451  imasvscafn  17460  mrisval  17555  isacs  17576  isacs2  17578  isacs1i  17582  mreacs  17583  acsfn  17584  acsfn2  17588  iscatd  17598  catidex  17599  catideu  17600  cidval  17602  catidd  17605  comfeq  17631  catpropd  17634  ismon  17659  isfunc  17790  isnat  17876  isinito  17922  istermo  17923  isprs  18221  drsdirfi  18230  ispos  18239  lubfval  18273  lubeldm  18276  lubval  18279  lubprop  18281  lublecllem  18283  glbfval  18286  glbeldm  18289  glbval  18292  glbprop  18294  joinval2lem  18303  joinlem  18306  meetval2lem  18317  meetlem  18320  poslubmo  18334  posglbmo  18335  poslubd  18336  resspos  18354  isglbd  18434  lubl  18437  lubun  18440  clatleglb  18443  isdlat  18447  ipodrsima  18466  chneq1  18537  mgm1  18585  gsumval2  18613  mgmhmima  18642  sgrp1  18656  mhmimalem  18751  mndind  18755  gsumwspan  18773  efmndmnd  18816  smndex1mnd  18837  sgrp2rid2  18853  sgrp2rid2ex  18854  sgrp2nmndlem4  18855  pwmnd  18864  dfgrp2  18894  isgrpinv  18925  grpidinv  18930  dfgrp3lem  18970  issubg4  19077  isnsg2  19087  nsgacs  19093  elnmz  19094  cycsubgcl  19137  ghmrn  19160  ghmnsgima  19171  isga  19222  orbsta  19244  cntzfval  19251  elcntz  19253  resscntz  19264  oppgsubg  19294  symgextfo  19353  gsmsymgreqlem2  19362  gsmsymgreq  19363  pmtrdifel  19411  pmtrdifwrdellem3  19414  pmtrdifwrdel2  19417  psgnunilem2  19426  psgnunilem3  19427  odeq  19481  gexid  19512  gexlem2  19513  gexdvds  19515  isslw  19539  sylow2alem1  19548  sylow2alem2  19549  efgval  19648  efgrelexlemb  19681  efgcpbllemb  19686  abl1  19797  dmdprd  19931  dprd2da  19975  pgpfac1lem5  20012  isomnd  20054  ring1  20247  rngisomring  20405  lringuplu  20479  rhmimasubrnglem  20500  isrrg  20633  isabv  20746  islss  20887  lssacs  20920  reslmhm  21006  islbs  21030  pj1lmhm  21054  lbsacsbs  21113  rnglidlmcl  21173  rnglidl0  21186  zringlpir  21424  psgndiflemA  21558  ocvfval  21623  elocv  21625  iunocv  21638  frlmlbs  21754  islindf  21769  islinds2  21770  islindf2  21771  lindfrn  21778  lsslindf  21787  islindf4  21795  opsrval  22003  ply1coe  22244  cply1coe0bi  22248  mat0dimcrng  22416  mdetunilem1  22558  mdetunilem9  22566  cpmat  22655  cpmatel  22657  1elcpmat  22661  m2cpminvid2lem  22700  basgen2  22935  bastop1  22939  isclo  23033  ordtbaslem  23134  iscn  23181  cnpval  23182  iscnp  23183  iscnp3  23190  lmbr  23204  lmbr2  23205  lmbrf  23206  cnprest  23235  cnprest2  23236  t0sep  23270  isreg  23278  t1sep2  23315  tgcmp  23347  1stcclb  23390  1stcfb  23391  2ndc1stc  23397  1stcrest  23399  2ndcdisj  23402  islly  23414  isnlly  23415  lly1stc  23442  isref  23455  islocfin  23463  elkgen  23482  kgencn  23502  elpt  23518  elptr  23519  ptcnplem  23567  tx1stc  23596  cnmpt21  23617  kqt0lem  23682  isr0  23683  regr1lem2  23686  r0sep  23694  nrmr0reg  23695  flffbas  23941  cnflf  23948  cnflf2  23949  lmflf  23951  txflf  23952  fclsopni  23961  fclsnei  23965  fclsrest  23970  fcfnei  23981  cnfcf  23988  alexsubb  23992  alexsubALTlem3  23995  qustgplem  24067  tsmsfbas  24074  tsmsres  24090  tsmsf1o  24091  tsmsxplem1  24099  ustval  24149  isust  24150  ustincl  24154  ustdiag  24155  ustinvel  24156  ustexhalf  24157  ust0  24166  utopval  24178  ucnval  24222  isucn  24223  isucn2  24224  ucnima  24226  iscfilu  24233  ispsmet  24250  ismet  24269  isxmet  24270  imasdsf1olem  24319  imasf1oxmet  24321  imasf1omet  24322  metss  24454  met1stc  24467  prdsxmslem2  24475  txmetcnp  24493  metucn  24517  tngngp3  24602  nlmvscn  24633  nmoval  24661  nmolb  24663  qtopbaslem  24704  cncfval  24839  elcncf2  24841  mulc1cncf  24856  cncfmet  24860  evth  24916  lebnumlem3  24920  lebnum  24921  xlebnum  24922  ishtpy  24929  isphtpy  24938  pi1xfr  25013  pi1coghm  25019  isclmp  25055  ipcn  25204  lmmbr2  25217  lmmbr3  25218  lmmbrf  25220  cfilfval  25222  iscfil  25223  fmcfil  25230  caufval  25233  iscau  25234  iscau2  25235  iscau3  25236  iscau4  25237  iscauf  25238  caucfil  25241  cfilresi  25253  causs  25256  lmclim  25261  cmetcusp1  25311  minveclem4c  25383  minveclem2  25384  minveclem3b  25386  minveclem4  25390  minveclem6  25392  minveclem7  25393  ovolicc2lem3  25478  ismbl  25485  dyadmax  25557  dyadmbllem  25558  dyadmbl  25559  opnmbllem  25560  ismbf1  25583  ismbf  25587  mbfeqalem2  25601  mbflimsup  25625  mbfi1fseqlem6  25679  mbfi1flimlem  25681  itg2seq  25701  itg2monolem1  25709  isibl  25724  ply1divex  26100  fta1g  26133  dgrco  26239  plydivex  26263  fta1  26274  vieta1  26278  aannenlem1  26294  aannenlem2  26295  aalioulem2  26299  aalioulem3  26300  ulmval  26347  ulm2  26352  ulmi  26353  ulmres  26355  ulmshftlem  26356  ulmcaulem  26361  ulmcau  26362  ulmss  26364  ulmbdd  26365  ulmdvlem1  26367  ulmdvlem3  26369  pilem2  26420  pilem3  26421  cxpcn3  26716  dmarea  26925  rlimcnp  26933  scvxcvx  26954  lgamgulmlem2  26998  lgamgulmlem3  26999  lgamgulmlem5  27001  lgambdd  27005  lgamcvglem  27008  isppw2  27083  perfectlem2  27199  2sqlem6  27392  2sqlem10  27397  addsq2reu  27409  2sqreulem1  27415  2sqreunnlem1  27418  dchrisumlema  27457  dchrisumlem2  27459  dchrisumlem3  27460  pntpbnd  27557  pntibndlem3  27561  pntibnd  27562  pntleme  27577  pntlem3  27578  pntlemp  27579  pnt3  27581  sltval  27617  nosupprefixmo  27670  noinfprefixmo  27671  nosupcbv  27672  nosupno  27673  nosupdm  27674  nosupfv  27676  nosupres  27677  nosupbnd1lem1  27678  nosupbnd1lem3  27680  nosupbnd1lem5  27682  noinfcbv  27687  noinfno  27688  noinfdm  27689  noinffv  27691  noinfres  27692  noinfbnd1lem3  27695  noinfbnd1lem5  27697  noetalem1  27711  noetalem2  27712  nocvxminlem  27752  brsslt  27760  ssltsnb  27767  conway  27775  etasslt  27789  slerec  27795  eqscut3  27800  madebdaylemlrcut  27879  madebday  27880  bdayle  27896  cofcutr  27904  cutmax  27914  cutmin  27915  lrrecfr  27923  addsprop  27956  negsunif  28035  addsonbday  28258  onsfi  28334  n0subs  28340  bdayn0p1  28346  bdaypw2n0sbndlem  28440  bdayfinbndlem2  28445  zs12zodd  28459  istrkgld  28512  axtg5seg  28518  tgcgr4  28584  perpln1  28763  perpln2  28764  isperp  28765  brbtwn2  28959  colinearalg  28964  axsegconlem1  28971  axsegcon  28981  ax5seglem4  28986  ax5seglem5  28987  axlowdim  29015  axeuclidlem  29016  axcontlem1  29018  axcontlem2  29019  axcontlem4  29021  axcontlem5  29022  axcontlem8  29025  axcontlem12  29029  elntg2  29039  uvtxusgr  29456  rgrx0ndm  29648  ewlksfval  29656  wksfval  29664  wwlks  29889  wlkiswwlks2  29929  clwwlk  30039  1conngr  30250  frgrwopregasn  30372  frgrwopregbsn  30373  frgrwopreglem5ALT  30378  frgrregord013  30451  isgrpo  30553  isgrpoi  30554  grpoideu  30565  grpoidinv2  30571  vciOLD  30617  isvclem  30633  cnidOLD  30638  isnvlem  30666  nvi  30670  lnoval  30808  islno  30809  isblo3i  30857  blo3i  30858  blocnilem  30860  ajfval  30865  ubthlem1  30926  ubthlem2  30927  ubthlem3  30928  ubth  30929  minvecolem2  30931  minvecolem3  30932  minvecolem4c  30935  minvecolem4  30936  minvecolem5  30937  minvecolem6  30938  minvecolem7  30939  h2hcau  31035  h2hlm  31036  hilid  31217  hcau  31240  hlimi  31244  hlim2  31248  ocel  31337  adjsym  31889  ellnop  31914  ellnfn  31939  hhcno  31960  hhcnf  31961  lnopeq  32065  elunop2  32069  lnophm  32075  lnconi  32089  lnopcnbd  32092  lnfncnbd  32113  imaelshi  32114  riesz3i  32118  riesz4i  32119  riesz4  32120  riesz1  32121  cnlnadjlem2  32124  cnlnadjlem5  32127  cnlnadjlem8  32130  cnlnadji  32132  nmopadjlei  32144  cnvbraval  32166  leopg  32178  leoppos  32182  mdbr  32350  dmdbr  32355  cdj3i  32497  disjunsn  32649  funcnv5mpt  32725  fgreu  32729  fcnvgreu  32730  xrge0infss  32819  wrdt2ind  33014  mgccole1  33051  mgccole2  33052  mgcmnt1  33053  mgcmnt2  33054  gsumhashmul  33129  isfxp  33229  fxpgaeq  33230  inftmrel  33241  isinftm  33242  archiabl  33259  isarchiofld  33260  elrgspnlem4  33306  0nellinds  33430  lindssn  33438  elrspunidl  33488  prmidl  33500  ismxidl  33522  1arithidom  33597  1arithufdlem3  33606  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  vietalem  33714  vieta  33715  crefeq  33981  zarcmplem  34017  esum2d  34229  sigaval  34247  issgon  34259  isrnmeas  34336  ismbfm  34387  mbfmcst  34395  elcarsg  34441  sitgval  34468  eulerpartlemd  34502  ballotleme  34633  tgoldbachgt  34799  bnj1185  34928  bnj1385  34967  bnj66  34995  bnj106  35003  bnj155  35014  bnj852  35056  bnj893  35063  bnj1228  35146  bnj1234  35148  bnj1463  35190  nummin  35228  rankfilimbi  35236  r1omhfb  35247  fineqvnttrclse  35259  r1omhfbregs  35272  gblacfnacd  35275  onvf1odlem4  35279  vonf1owev  35281  derangenlem  35344  subfacp1lem3  35355  subfacp1lem5  35357  subfacp1lem6  35358  subfacp1  35359  erdszelem8  35371  kur14  35389  cnpconn  35403  resconn  35419  cvmscbv  35431  iscvm  35432  cvmsi  35438  cvmsval  35439  cvmlift3lem2  35493  snmlval  35504  satfv1  35536  fmlasucdisj  35572  satffunlem1lem1  35575  satffunlem2lem1  35577  satfv1fvfmla1  35596  mclsssvlem  35735  mclsval  35736  mclsax  35742  mclsind  35743  dfon2lem9  35962  dfrdg2  35966  dfrdg3  35967  fwddifnval  36336  nn0prpwlem  36495  isfne  36512  isfne4  36513  isfne2  36515  isfne3  36516  neibastop3  36535  topmeet  36537  topjoin  36538  filnetlem4  36554  weiunlem2  36636  weiunfrlem  36637  unblimceq0lem  36679  unblimceq0  36680  unbdqndv2  36684  taupilemrplb  37494  fin2so  37777  lindsadd  37783  matunitlindflem2  37787  ptrecube  37790  poimirlem2  37792  poimirlem3  37793  poimirlem4  37794  poimirlem24  37814  poimirlem25  37815  poimirlem26  37816  poimirlem27  37817  poimirlem28  37818  poimirlem29  37819  poimirlem30  37820  poimirlem32  37822  poimir  37823  heicant  37825  mblfinlem1  37827  mblfinlem2  37828  voliunnfl  37834  volsupnfl  37835  mbfresfi  37836  itg2addnc  37844  upixp  37899  indexdom  37904  filbcmb  37910  sdclem2  37912  fdc  37915  lmclim2  37928  caures  37930  istotbnd  37939  istotbnd3  37941  sstotbnd  37945  isbnd  37950  heibor  37991  bfp  37994  rrncmslem  38002  isgrpda  38125  idlval  38183  isidl  38184  0idl  38195  unichnidl  38201  pridl  38207  ismaxidl  38210  smprngopr  38222  igenval2  38236  prnc  38237  ispridlc  38240  scottexf  38338  scott0f  38339  disjsuc2  38584  riotasvd  39251  islfl  39355  eqlkr  39394  eqlkr3  39396  glbconN  39672  hlsuprexch  39676  ispsubsp  40040  ldilset  40404  isldil  40405  dilsetN  40448  isdilN  40449  trlset  40456  trlval  40457  cdleme27b  40663  cdleme29b  40670  cdleme31so  40674  cdleme31sn1  40676  cdleme31sn1c  40683  cdleme31fv  40685  cdleme40v  40764  istendo  41055  cdlemkid3N  41228  cdlemkid4  41229  cdlemkid5  41230  dihfval  41526  dihval  41527  islpolN  41778  hdmapffval  42121  hdmapfval  42122  hdmapval  42123  hdmapval2lem  42126  hgmapffval  42180  hgmapfval  42181  hgmapval  42182  hgmapvs  42186  isprimroot  42382  aks6d1c1p1  42396  hashscontpow1  42410  sticksstones2  42436  unitscyglem3  42486  exfinfldd  42492  qsalrel  42533  supinf  42534  sn-sup2  42783  fsuppind  42870  isnacs  42983  isnacs2  42985  nacsfix  42991  mzpclval  43004  elmzpcl  43005  rencldnfilem  43099  infmrgelbi  43157  pellfundre  43160  pellfundlb  43163  wepwsolem  43321  fnwe2lem2  43330  aomclem8  43340  dfac11  43341  gicabl  43378  islnr3  43394  hbtlem2  43403  hbtlem5  43407  onintunirab  43506  onsucf1lem  43548  cantnfresb  43603  safesnsupfilb  43696  rp-brsslt  43701  fiinfi  43851  clsk1independent  44324  ntrclsk13  44349  gneispacess2  44424  imo72b2lem0  44443  imo72b2lem2  44445  imo72b2lem1  44447  imo72b2  44450  scottelrankd  44525  mnuop23d  44544  ismnushort  44579  ralabsobidv  45250  0elaxnul  45261  pwclaxpow  45262  prclaxpr  45263  uniclaxun  45264  omssaxinf2  45266  modelac8prim  45270  wfac8prim  45280  permac8prim  45292  evth2f  45297  evthf  45309  fnchoice  45311  uzwo4  45335  wessf1ornlem  45466  disjinfi  45473  rnmptlb  45524  rnmptbdd  45526  rnmptbd2  45530  rnmptbd  45537  dstregt0  45567  upbdrech2  45593  rexabslelem  45699  rexabsle  45700  uzub  45712  infrpgernmpt  45746  mccl  45881  ellimcabssub0  45900  climf  45905  clim2f  45917  limsupre  45922  clim2cf  45931  clim0cf  45935  climf2  45947  clim2f2  45951  clim2d  45954  limsupref  45966  limsupbnd1f  45967  climinf2  45988  limsuppnf  45992  climinfmpt  45996  climinf3  45997  limsupubuzmpt  46000  limsupmnf  46002  limsupre2lem  46005  limsupre2  46006  limsupmnfuzlem  46007  limsupmnfuz  46008  limsupre2mpt  46011  limsupre3lem  46013  limsupre3  46014  limsupre3mpt  46015  limsupre3uz  46017  limsupreuz  46018  limsupreuzmpt  46020  climuz  46025  liminfreuzlem  46083  liminfreuz  46084  cnrefiisplem  46110  xlimmnfvlem1  46113  xlimmnfv  46115  xlimpnfvlem1  46117  xlimpnfv  46119  xlimmnfmpt  46124  xlimpnfmpt  46125  cncfshift  46155  cncfperiod  46160  fperdvper  46200  dvbdfbdioo  46211  ioodvbdlimc1lem2  46213  ioodvbdlimc2lem  46215  dvnprodlem3  46229  stoweidlem5  46286  stoweidlem9  46290  stoweidlem15  46296  stoweidlem16  46297  stoweidlem27  46308  stoweidlem28  46309  stoweidlem31  46312  stoweidlem34  46315  stoweidlem37  46318  stoweidlem46  46327  stoweidlem48  46329  stoweidlem51  46332  stoweidlem52  46333  stoweidlem59  46340  wallispilem3  46348  stirlinglem13  46367  fourierdlem2  46390  fourierdlem3  46391  fourierdlem16  46404  fourierdlem20  46408  fourierdlem21  46409  fourierdlem22  46410  fourierdlem25  46413  fourierdlem39  46427  fourierdlem42  46430  fourierdlem54  46441  fourierdlem64  46451  fourierdlem77  46464  fourierdlem83  46470  fourierdlem103  46490  fourierdlem104  46491  subsaliuncllem  46638  iundjiun  46741  meaiunincf  46764  caragenval  46774  isome  46775  caragenel  46776  omessle  46779  ovnlerp  46843  hoidmvlelem3  46878  hoidmvle  46881  issmflem  47008  issmfgt  47037  smfmullem2  47073  smfmullem4  47075  smfmul  47076  smfsuplem2  47093  smfsup  47095  smfinflem  47098  smfinf  47099  fsupdm  47123  finfdm  47127  cfsetsnfsetf  47341  cbvral2  47386  2reu8i  47396  2reuimp0  47397  dfdfat2  47411  iccpart  47699  iccpartigtl  47706  paireqne  47794  reupr  47805  perfectALTVlem2  48005  bgoldbachlt  48096  tgoldbachlt  48099  grimidvtxedg  48168  grimcnv  48171  grimco  48172  isuspgrim0  48177  gricushgr  48200  ushggricedg  48210  uhgrimisgrgric  48214  isubgr3stgr  48258  isgrlim  48265  isgrlim2  48266  uspgrlim  48275  grlicsym  48296  grlictr  48298  gpg5nbgrvtx03star  48363  gpg5nbgr3star  48364  pgnbgreunbgr  48408  upwlksfval  48418  nn0mnd  48462  uzlidlring  48518  ply1mulgsumlem1  48669  ply1mulgsumlem2  48670  linindslinci  48731  lindslinindsimp1  48740  lindslinindsimp2lem5  48745  lindslinindsimp2  48746  linds0  48748  lindsrng01  48751  snlindsntor  48754  lmod1  48775  ldepsnlinc  48791  bigoval  48832  elbigo2r  48836  nn0sumshdiglem2  48905  eenglngeehlnmlem1  49020  eenglngeehlnmlem2  49021  lubeldm2d  49240  glbeldm2d  49241  lubsscl  49242  glbsscl  49243  ipolubdm  49269  ipolub  49270  ipoglbdm  49272  ipoglb  49273  nelsubc3lem  49352  upfval2  49459  upfval3  49460  isthincd2lem2  49717  setc1onsubc  49884  cnelsubclem  49885  setrec1lem2  49970