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  3340  rspceaimv  3584  rspc2  3587  rspc2v  3589  rspc3v  3594  rspc4v  3598  reu6i  3688  reu7  3692  sbcralt  3824  reu8nf  3829  raaan  4473  raaanv  4474  raaan2  4477  2reu4lem  4478  reusngf  4633  2ralsng  4637  rexreusng  4638  reuprg0  4661  issn  4790  2ralunsn  4853  elintg  4912  elintrabg  4918  eliin  4953  disjprg  5096  disjxun  5098  brralrspcev  5160  reusv2lem2  5348  reusv3  5354  poeq1  5545  solin  5569  somo  5581  frirr  5610  fr2nr  5611  frminex  5613  wereu2  5631  posn  5720  frsn  5722  ralxpf  5805  cnvpo  6255  reu3op  6260  reuop  6261  dfpo2  6264  frpomin  6308  fnmptfvd  6997  iinpreima  7025  dff4  7057  dff13f  7213  fpropnf1  7225  f1ounsn  7230  eusvobj2  7362  ovanraleqv  7394  f1opr  7426  ofreq  7638  sorpssuni  7689  sorpssint  7690  fr3nr  7729  onssmin  7749  funcnvuni  7886  f1oweALT  7928  frxp  8080  frxp2  8098  xpord2indlem  8101  frxp3  8105  xpord3inddlem  8108  poseq  8112  soseq  8113  frecseq123  8236  csbfrecsg  8238  frrlem1  8240  frrlem13  8252  smoeq  8294  tfrlem12  8332  tz7.48lem  8384  naddcllem  8616  naddov2  8619  naddunif  8633  naddasslem1  8634  naddasslem2  8635  elixp2  8853  undifixp  8886  xpf1o  9081  nneneq  9144  ac6sfi  9198  frfi  9199  fipreima  9272  indexfi  9274  marypha1lem  9350  marypha1  9351  supeq1  9362  supeq3  9366  supmo  9369  eqsup  9373  supub  9376  suplub  9377  sup0  9384  supisoex  9392  eqinf  9402  infval  9404  infmo  9414  oieq1  9431  ordtypecbv  9436  ordtypelem3  9439  ordtypelem6  9442  ordtypelem7  9443  ordtypelem9  9445  wemaplem1  9465  wemaplem2  9466  zfregcl  9513  zfregclOLD  9514  oemapval  9606  oemapvali  9607  cantnf  9616  wemapwe  9620  ttrcleq  9632  ttrcltr  9639  ttrclss  9643  ttrclselem2  9649  rankval3b  9752  unbndrank  9768  rankunb  9776  rankuni2b  9779  tcrank  9810  scottex  9811  scottexs  9813  scott0s  9814  bnd2  9819  updjud  9860  dfac8clem  9956  ac5num  9960  acni  9969  acni2  9970  alephval3  10034  dfac4  10046  dfac5lem5  10051  dfac5  10053  dfac2a  10054  dfac2b  10055  dfacacn  10066  kmlem2  10076  kmlem13  10087  cflem  10169  cflemOLD  10170  cflecard  10177  cfeq0  10180  cfsuc  10181  cfflb  10183  cofsmo  10193  cfsmolem  10194  cfcoflem  10196  coftr  10197  alephsing  10200  fin23lem11  10241  isfin3ds  10253  fin23lem17  10262  fin23lem39  10274  isf33lem  10290  isf34lem6  10304  fin1a2lem13  10336  hsmexlem4  10353  hsmex  10356  axcc2lem  10360  axcc3  10362  dcomex  10371  axdc2lem  10372  axdc3lem2  10375  axdc3lem3  10376  axdc3  10378  axdc4lem  10379  axcclem  10381  zorn2lem2  10421  zorn2lem7  10426  zorn2g  10427  zornn0g  10429  ttukeylem7  10439  axdclem2  10444  brdom3  10452  brdom7disj  10455  brdom6disj  10456  alephval2  10497  inar1  10700  axgroth6  10753  pinq  10852  nqereu  10854  prlem934  10958  supexpr  10979  supsrlem  11036  axpre-sup  11094  dedekind  11310  dedekindle  11311  fiminre2  12104  lbreu  12106  sup2  12112  infm3  12115  nnsub  12203  uzwo  12838  nnwof  12841  ublbneg  12860  lbzbi  12863  zsupss  12864  uzsupss  12867  uzwo3  12870  zmax  12872  rpnnen1lem1  12905  rpnnen1lem3  12906  rpnnen1lem4  12907  rpnnen1lem5  12908  xrsupsslem  13236  xrinfmsslem  13237  xrsupss  13238  xrinfmss  13239  flval2  13748  axdc4uzlem  13920  ssnn0fi  13922  fsuppmapnn0fiubex  13929  faclbnd4lem4  14233  bccl  14259  hashgt12el  14359  hashbc  14390  hashge2el2dif  14417  wrdind  14659  wrd2ind  14660  rexanre  15284  rexico  15291  cau4  15294  reusq0  15402  clim  15431  rlim  15432  rlim2  15433  clim2  15441  clim2c  15442  clim0c  15444  rlim0  15445  rlim0lt  15446  ello12r  15454  ello1d  15460  elo12r  15465  rlimresb  15502  rlimcld2  15515  climabs0  15522  rlimo1  15554  lo1add  15564  lo1mul  15565  isercoll  15605  incexclem  15773  sqrt2irr  16188  gcdcllem1  16440  gcdcllem2  16441  dfgcd2  16487  fissn0dvds  16560  dvdslcmf  16572  lcmfledvds  16573  lcmf  16574  lcmfunsnlem1  16578  lcmfunsnlem2lem1  16579  lcmfunsnlem  16582  lcmfdvds  16583  reumodprminv  16746  pc2dvds  16821  pcz  16823  prmpwdvds  16846  infpn2  16855  prmreclem2  16859  prmreclem3  16860  prmreclem5  16862  prmreclem6  16863  vdwlem6  16928  vdwlem8  16930  vdwlem13  16935  vdwnnlem1  16937  vdwnn  16940  ramcl  16971  cshwrepswhash1  17044  prdsleval  17411  imasval  17446  imasaddfnlem  17463  imasvscafn  17472  mrisval  17567  isacs  17588  isacs2  17590  isacs1i  17594  mreacs  17595  acsfn  17596  acsfn2  17600  iscatd  17610  catidex  17611  catideu  17612  cidval  17614  catidd  17617  comfeq  17643  catpropd  17646  ismon  17671  isfunc  17802  isnat  17888  isinito  17934  istermo  17935  isprs  18233  drsdirfi  18242  ispos  18251  lubfval  18285  lubeldm  18288  lubval  18291  lubprop  18293  lublecllem  18295  glbfval  18298  glbeldm  18301  glbval  18304  glbprop  18306  joinval2lem  18315  joinlem  18318  meetval2lem  18329  meetlem  18332  poslubmo  18346  posglbmo  18347  poslubd  18348  resspos  18366  isglbd  18446  lubl  18449  lubun  18452  clatleglb  18455  isdlat  18459  ipodrsima  18478  chneq1  18549  mgm1  18597  gsumval2  18625  mgmhmima  18654  sgrp1  18668  mhmimalem  18763  mndind  18767  gsumwspan  18785  efmndmnd  18828  smndex1mnd  18852  sgrp2rid2  18868  sgrp2rid2ex  18869  sgrp2nmndlem4  18870  pwmnd  18879  dfgrp2  18909  isgrpinv  18940  grpidinv  18945  dfgrp3lem  18985  issubg4  19092  isnsg2  19102  nsgacs  19108  elnmz  19109  cycsubgcl  19152  ghmrn  19175  ghmnsgima  19186  isga  19237  orbsta  19259  cntzfval  19266  elcntz  19268  resscntz  19279  oppgsubg  19309  symgextfo  19368  gsmsymgreqlem2  19377  gsmsymgreq  19378  pmtrdifel  19426  pmtrdifwrdellem3  19429  pmtrdifwrdel2  19432  psgnunilem2  19441  psgnunilem3  19442  odeq  19496  gexid  19527  gexlem2  19528  gexdvds  19530  isslw  19554  sylow2alem1  19563  sylow2alem2  19564  efgval  19663  efgrelexlemb  19696  efgcpbllemb  19701  abl1  19812  dmdprd  19946  dprd2da  19990  pgpfac1lem5  20027  isomnd  20069  ring1  20262  rngisomring  20420  lringuplu  20494  rhmimasubrnglem  20515  isrrg  20648  isabv  20761  islss  20902  lssacs  20935  reslmhm  21021  islbs  21045  pj1lmhm  21069  lbsacsbs  21128  rnglidlmcl  21188  rnglidl0  21201  zringlpir  21439  psgndiflemA  21573  ocvfval  21638  elocv  21640  iunocv  21653  frlmlbs  21769  islindf  21784  islinds2  21785  islindf2  21786  lindfrn  21793  lsslindf  21802  islindf4  21810  opsrval  22018  ply1coe  22259  cply1coe0bi  22263  mat0dimcrng  22431  mdetunilem1  22573  mdetunilem9  22581  cpmat  22670  cpmatel  22672  1elcpmat  22676  m2cpminvid2lem  22715  basgen2  22950  bastop1  22954  isclo  23048  ordtbaslem  23149  iscn  23196  cnpval  23197  iscnp  23198  iscnp3  23205  lmbr  23219  lmbr2  23220  lmbrf  23221  cnprest  23250  cnprest2  23251  t0sep  23285  isreg  23293  t1sep2  23330  tgcmp  23362  1stcclb  23405  1stcfb  23406  2ndc1stc  23412  1stcrest  23414  2ndcdisj  23417  islly  23429  isnlly  23430  lly1stc  23457  isref  23470  islocfin  23478  elkgen  23497  kgencn  23517  elpt  23533  elptr  23534  ptcnplem  23582  tx1stc  23611  cnmpt21  23632  kqt0lem  23697  isr0  23698  regr1lem2  23701  r0sep  23709  nrmr0reg  23710  flffbas  23956  cnflf  23963  cnflf2  23964  lmflf  23966  txflf  23967  fclsopni  23976  fclsnei  23980  fclsrest  23985  fcfnei  23996  cnfcf  24003  alexsubb  24007  alexsubALTlem3  24010  qustgplem  24082  tsmsfbas  24089  tsmsres  24105  tsmsf1o  24106  tsmsxplem1  24114  ustval  24164  isust  24165  ustincl  24169  ustdiag  24170  ustinvel  24171  ustexhalf  24172  ust0  24181  utopval  24193  ucnval  24237  isucn  24238  isucn2  24239  ucnima  24241  iscfilu  24248  ispsmet  24265  ismet  24284  isxmet  24285  imasdsf1olem  24334  imasf1oxmet  24336  imasf1omet  24337  metss  24469  met1stc  24482  prdsxmslem2  24490  txmetcnp  24508  metucn  24532  tngngp3  24617  nlmvscn  24648  nmoval  24676  nmolb  24678  qtopbaslem  24719  cncfval  24854  elcncf2  24856  mulc1cncf  24871  cncfmet  24875  evth  24931  lebnumlem3  24935  lebnum  24936  xlebnum  24937  ishtpy  24944  isphtpy  24953  pi1xfr  25028  pi1coghm  25034  isclmp  25070  ipcn  25219  lmmbr2  25232  lmmbr3  25233  lmmbrf  25235  cfilfval  25237  iscfil  25238  fmcfil  25245  caufval  25248  iscau  25249  iscau2  25250  iscau3  25251  iscau4  25252  iscauf  25253  caucfil  25256  cfilresi  25268  causs  25271  lmclim  25276  cmetcusp1  25326  minveclem4c  25398  minveclem2  25399  minveclem3b  25401  minveclem4  25405  minveclem6  25407  minveclem7  25408  ovolicc2lem3  25493  ismbl  25500  dyadmax  25572  dyadmbllem  25573  dyadmbl  25574  opnmbllem  25575  ismbf1  25598  ismbf  25602  mbfeqalem2  25616  mbflimsup  25640  mbfi1fseqlem6  25694  mbfi1flimlem  25696  itg2seq  25716  itg2monolem1  25724  isibl  25739  ply1divex  26115  fta1g  26148  dgrco  26254  plydivex  26278  fta1  26289  vieta1  26293  aannenlem1  26309  aannenlem2  26310  aalioulem2  26314  aalioulem3  26315  ulmval  26362  ulm2  26367  ulmi  26368  ulmres  26370  ulmshftlem  26371  ulmcaulem  26376  ulmcau  26377  ulmss  26379  ulmbdd  26380  ulmdvlem1  26382  ulmdvlem3  26384  pilem2  26435  pilem3  26436  cxpcn3  26731  dmarea  26940  rlimcnp  26948  scvxcvx  26969  lgamgulmlem2  27013  lgamgulmlem3  27014  lgamgulmlem5  27016  lgambdd  27020  lgamcvglem  27023  isppw2  27098  perfectlem2  27214  2sqlem6  27407  2sqlem10  27412  addsq2reu  27424  2sqreulem1  27430  2sqreunnlem1  27433  dchrisumlema  27472  dchrisumlem2  27474  dchrisumlem3  27475  pntpbnd  27572  pntibndlem3  27576  pntibnd  27577  pntleme  27592  pntlem3  27593  pntlemp  27594  pnt3  27596  ltsval  27632  nosupprefixmo  27685  noinfprefixmo  27686  nosupcbv  27687  nosupno  27688  nosupdm  27689  nosupfv  27691  nosupres  27692  nosupbnd1lem1  27693  nosupbnd1lem3  27695  nosupbnd1lem5  27697  noinfcbv  27702  noinfno  27703  noinfdm  27704  noinffv  27706  noinfres  27707  noinfbnd1lem3  27710  noinfbnd1lem5  27712  noetalem1  27726  noetalem2  27727  nocvxminlem  27767  brslts  27775  sltssnb  27782  conway  27792  etaslts  27806  lesrec  27812  eqcuts3  27817  madebdaylemlrcut  27912  madebday  27913  bdayle  27929  cofcutr  27937  cutmax  27947  cutmin  27948  lrrecfr  27956  addsprop  27989  negsunif  28068  addonbday  28292  onsfi  28369  n0subs  28376  bdayn0p1  28382  bdaypw2n0bndlem  28476  bdayfinbndlem2  28481  z12zsodd  28495  istrkgld  28548  axtg5seg  28555  tgcgr4  28621  perpln1  28800  perpln2  28801  isperp  28802  brbtwn2  28996  colinearalg  29001  axsegconlem1  29008  axsegcon  29018  ax5seglem4  29023  ax5seglem5  29024  axlowdim  29052  axeuclidlem  29053  axcontlem1  29055  axcontlem2  29056  axcontlem4  29058  axcontlem5  29059  axcontlem8  29062  axcontlem12  29066  elntg2  29076  uvtxusgr  29493  rgrx0ndm  29685  ewlksfval  29693  wksfval  29701  wwlks  29926  wlkiswwlks2  29966  clwwlk  30076  1conngr  30287  frgrwopregasn  30409  frgrwopregbsn  30410  frgrwopreglem5ALT  30415  frgrregord013  30488  isgrpo  30591  isgrpoi  30592  grpoideu  30603  grpoidinv2  30609  vciOLD  30655  isvclem  30671  cnidOLD  30676  isnvlem  30704  nvi  30708  lnoval  30846  islno  30847  isblo3i  30895  blo3i  30896  blocnilem  30898  ajfval  30903  ubthlem1  30964  ubthlem2  30965  ubthlem3  30966  ubth  30967  minvecolem2  30969  minvecolem3  30970  minvecolem4c  30973  minvecolem4  30974  minvecolem5  30975  minvecolem6  30976  minvecolem7  30977  h2hcau  31073  h2hlm  31074  hilid  31255  hcau  31278  hlimi  31282  hlim2  31286  ocel  31375  adjsym  31927  ellnop  31952  ellnfn  31977  hhcno  31998  hhcnf  31999  lnopeq  32103  elunop2  32107  lnophm  32113  lnconi  32127  lnopcnbd  32130  lnfncnbd  32151  imaelshi  32152  riesz3i  32156  riesz4i  32157  riesz4  32158  riesz1  32159  cnlnadjlem2  32162  cnlnadjlem5  32165  cnlnadjlem8  32168  cnlnadji  32170  nmopadjlei  32182  cnvbraval  32204  leopg  32216  leoppos  32220  mdbr  32388  dmdbr  32393  cdj3i  32535  disjunsn  32687  funcnv5mpt  32763  fgreu  32767  fcnvgreu  32768  xrge0infss  32857  wrdt2ind  33052  mgccole1  33089  mgccole2  33090  mgcmnt1  33091  mgcmnt2  33092  gsumhashmul  33167  isfxp  33268  fxpgaeq  33269  inftmrel  33280  isinftm  33281  archiabl  33298  isarchiofld  33299  elrgspnlem4  33345  0nellinds  33469  lindssn  33477  elrspunidl  33527  prmidl  33539  ismxidl  33561  1arithidom  33636  1arithufdlem3  33645  evl1deg1  33675  evl1deg2  33676  evl1deg3  33677  vietalem  33762  vieta  33763  crefeq  34029  zarcmplem  34065  esum2d  34277  sigaval  34295  issgon  34307  isrnmeas  34384  ismbfm  34435  mbfmcst  34443  elcarsg  34489  sitgval  34516  eulerpartlemd  34550  ballotleme  34681  tgoldbachgt  34847  bnj1185  34975  bnj1385  35014  bnj66  35042  bnj106  35050  bnj155  35061  bnj852  35103  bnj893  35110  bnj1228  35193  bnj1234  35195  bnj1463  35237  nummin  35276  rankfilimbi  35284  r1omhfb  35296  fineqvnttrclse  35308  r1omhfbregs  35321  gblacfnacd  35324  onvf1odlem4  35328  vonf1owev  35330  derangenlem  35393  subfacp1lem3  35404  subfacp1lem5  35406  subfacp1lem6  35407  subfacp1  35408  erdszelem8  35420  kur14  35438  cnpconn  35452  resconn  35468  cvmscbv  35480  iscvm  35481  cvmsi  35487  cvmsval  35488  cvmlift3lem2  35542  snmlval  35553  satfv1  35585  fmlasucdisj  35621  satffunlem1lem1  35624  satffunlem2lem1  35626  satfv1fvfmla1  35645  mclsssvlem  35784  mclsval  35785  mclsax  35791  mclsind  35792  dfon2lem9  36011  dfrdg2  36015  dfrdg3  36016  fwddifnval  36385  nn0prpwlem  36544  isfne  36561  isfne4  36562  isfne2  36564  isfne3  36565  neibastop3  36584  topmeet  36586  topjoin  36587  filnetlem4  36603  weiunlem  36685  weiunfrlem  36686  unblimceq0lem  36734  unblimceq0  36735  unbdqndv2  36739  taupilemrplb  37602  fin2so  37887  lindsadd  37893  matunitlindflem2  37897  ptrecube  37900  poimirlem2  37902  poimirlem3  37903  poimirlem4  37904  poimirlem24  37924  poimirlem25  37925  poimirlem26  37926  poimirlem27  37927  poimirlem28  37928  poimirlem29  37929  poimirlem30  37930  poimirlem32  37932  poimir  37933  heicant  37935  mblfinlem1  37937  mblfinlem2  37938  voliunnfl  37944  volsupnfl  37945  mbfresfi  37946  itg2addnc  37954  upixp  38009  indexdom  38014  filbcmb  38020  sdclem2  38022  fdc  38025  lmclim2  38038  caures  38040  istotbnd  38049  istotbnd3  38051  sstotbnd  38055  isbnd  38060  heibor  38101  bfp  38104  rrncmslem  38112  isgrpda  38235  idlval  38293  isidl  38294  0idl  38305  unichnidl  38311  pridl  38317  ismaxidl  38320  smprngopr  38332  igenval2  38346  prnc  38347  ispridlc  38350  scottexf  38448  scott0f  38449  disjsuc2  38694  riotasvd  39361  islfl  39465  eqlkr  39504  eqlkr3  39506  glbconN  39782  hlsuprexch  39786  ispsubsp  40150  ldilset  40514  isldil  40515  dilsetN  40558  isdilN  40559  trlset  40566  trlval  40567  cdleme27b  40773  cdleme29b  40780  cdleme31so  40784  cdleme31sn1  40786  cdleme31sn1c  40793  cdleme31fv  40795  cdleme40v  40874  istendo  41165  cdlemkid3N  41338  cdlemkid4  41339  cdlemkid5  41340  dihfval  41636  dihval  41637  islpolN  41888  hdmapffval  42231  hdmapfval  42232  hdmapval  42233  hdmapval2lem  42236  hgmapffval  42290  hgmapfval  42291  hgmapval  42292  hgmapvs  42296  isprimroot  42492  aks6d1c1p1  42506  hashscontpow1  42520  sticksstones2  42546  unitscyglem3  42596  exfinfldd  42602  qsalrel  42640  supinf  42641  sn-sup2  42890  fsuppind  42977  isnacs  43090  isnacs2  43092  nacsfix  43098  mzpclval  43111  elmzpcl  43112  rencldnfilem  43206  infmrgelbi  43264  pellfundre  43267  pellfundlb  43270  wepwsolem  43428  fnwe2lem2  43437  aomclem8  43447  dfac11  43448  gicabl  43485  islnr3  43501  hbtlem2  43510  hbtlem5  43514  onintunirab  43613  onsucf1lem  43655  cantnfresb  43710  safesnsupfilb  43803  rp-brsslt  43808  fiinfi  43958  clsk1independent  44431  ntrclsk13  44456  gneispacess2  44531  imo72b2lem0  44550  imo72b2lem2  44552  imo72b2lem1  44554  imo72b2  44557  scottelrankd  44632  mnuop23d  44651  ismnushort  44686  ralabsobidv  45357  0elaxnul  45368  pwclaxpow  45369  prclaxpr  45370  uniclaxun  45371  omssaxinf2  45373  modelac8prim  45377  wfac8prim  45387  permac8prim  45399  evth2f  45404  evthf  45416  fnchoice  45418  uzwo4  45442  wessf1ornlem  45573  disjinfi  45580  rnmptlb  45630  rnmptbdd  45632  rnmptbd2  45636  rnmptbd  45643  dstregt0  45673  upbdrech2  45699  rexabslelem  45805  rexabsle  45806  uzub  45818  infrpgernmpt  45852  mccl  45987  ellimcabssub0  46006  climf  46011  clim2f  46023  limsupre  46028  clim2cf  46037  clim0cf  46041  climf2  46053  clim2f2  46057  clim2d  46060  limsupref  46072  limsupbnd1f  46073  climinf2  46094  limsuppnf  46098  climinfmpt  46102  climinf3  46103  limsupubuzmpt  46106  limsupmnf  46108  limsupre2lem  46111  limsupre2  46112  limsupmnfuzlem  46113  limsupmnfuz  46114  limsupre2mpt  46117  limsupre3lem  46119  limsupre3  46120  limsupre3mpt  46121  limsupre3uz  46123  limsupreuz  46124  limsupreuzmpt  46126  climuz  46131  liminfreuzlem  46189  liminfreuz  46190  cnrefiisplem  46216  xlimmnfvlem1  46219  xlimmnfv  46221  xlimpnfvlem1  46223  xlimpnfv  46225  xlimmnfmpt  46230  xlimpnfmpt  46231  cncfshift  46261  cncfperiod  46266  fperdvper  46306  dvbdfbdioo  46317  ioodvbdlimc1lem2  46319  ioodvbdlimc2lem  46321  dvnprodlem3  46335  stoweidlem5  46392  stoweidlem9  46396  stoweidlem15  46402  stoweidlem16  46403  stoweidlem27  46414  stoweidlem28  46415  stoweidlem31  46418  stoweidlem34  46421  stoweidlem37  46424  stoweidlem46  46433  stoweidlem48  46435  stoweidlem51  46438  stoweidlem52  46439  stoweidlem59  46446  wallispilem3  46454  stirlinglem13  46473  fourierdlem2  46496  fourierdlem3  46497  fourierdlem16  46510  fourierdlem20  46514  fourierdlem21  46515  fourierdlem22  46516  fourierdlem25  46519  fourierdlem39  46533  fourierdlem42  46536  fourierdlem54  46547  fourierdlem64  46557  fourierdlem77  46570  fourierdlem83  46576  fourierdlem103  46596  fourierdlem104  46597  subsaliuncllem  46744  iundjiun  46847  meaiunincf  46870  caragenval  46880  isome  46881  caragenel  46882  omessle  46885  ovnlerp  46949  hoidmvlelem3  46984  hoidmvle  46987  issmflem  47114  issmfgt  47143  smfmullem2  47179  smfmullem4  47181  smfmul  47182  smfsuplem2  47199  smfsup  47201  smfinflem  47204  smfinf  47205  fsupdm  47229  finfdm  47233  cfsetsnfsetf  47447  cbvral2  47492  2reu8i  47502  2reuimp0  47503  dfdfat2  47517  iccpart  47805  iccpartigtl  47812  paireqne  47900  reupr  47911  perfectALTVlem2  48111  bgoldbachlt  48202  tgoldbachlt  48205  grimidvtxedg  48274  grimcnv  48277  grimco  48278  isuspgrim0  48283  gricushgr  48306  ushggricedg  48316  uhgrimisgrgric  48320  isubgr3stgr  48364  isgrlim  48371  isgrlim2  48372  uspgrlim  48381  grlicsym  48402  grlictr  48404  gpg5nbgrvtx03star  48469  gpg5nbgr3star  48470  pgnbgreunbgr  48514  upwlksfval  48524  nn0mnd  48568  uzlidlring  48624  ply1mulgsumlem1  48775  ply1mulgsumlem2  48776  linindslinci  48837  lindslinindsimp1  48846  lindslinindsimp2lem5  48851  lindslinindsimp2  48852  linds0  48854  lindsrng01  48857  snlindsntor  48860  lmod1  48881  ldepsnlinc  48897  bigoval  48938  elbigo2r  48942  nn0sumshdiglem2  49011  eenglngeehlnmlem1  49126  eenglngeehlnmlem2  49127  lubeldm2d  49346  glbeldm2d  49347  lubsscl  49348  glbsscl  49349  ipolubdm  49375  ipolub  49376  ipoglbdm  49378  ipoglb  49379  nelsubc3lem  49458  upfval2  49565  upfval3  49566  isthincd2lem2  49823  setc1onsubc  49990  cnelsubclem  49991  setrec1lem2  50076