Theorem ralbidv 3163

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3052

This theorem is referenced by:  2ralbidv  3205  rexralbidv  3207  3ralbidv  3208  4ralbidv  3209  cbvral2vw  3224  cbvral4vw  3227  cbvral2v  3347  rspceaimv  3607  rspc2  3610  rspc2v  3612  rspc3v  3617  rspc4v  3621  reu6i  3711  reu7  3715  sbcralt  3847  reu8nf  3852  raaan  4492  raaanv  4493  raaan2  4496  2reu4lem  4497  reusngf  4650  2ralsng  4654  rexreusng  4655  reuprg0  4678  issn  4808  2ralunsn  4871  elintg  4930  elintrabg  4937  eliin  4972  disjprg  5115  disjxun  5117  brralrspcev  5179  reusv2lem2  5369  reusv3  5375  poeq1  5564  solin  5588  somo  5600  frirr  5630  fr2nr  5631  frminex  5633  wereu2  5651  posn  5740  frsn  5742  ralxpf  5826  cnvpo  6276  reu3op  6281  reuop  6282  dfpo2  6285  frpomin  6329  fnmptfvd  7030  iinpreima  7058  dff4  7090  dff13f  7247  fpropnf1  7259  f1ounsn  7264  eusvobj2  7395  ovanraleqv  7427  f1opr  7461  ofreq  7673  sorpssuni  7724  sorpssint  7725  fr3nr  7764  onssmin  7784  funcnvuni  7926  f1oweALT  7969  frxp  8123  frxp2  8141  xpord2indlem  8144  frxp3  8148  xpord3inddlem  8151  poseq  8155  soseq  8156  frecseq123  8279  csbfrecsg  8281  frrlem1  8283  frrlem13  8295  wrecseq123OLD  8312  wfrlem1OLD  8320  wfrlem3OLDa  8323  wfrlem15OLD  8335  smoeq  8362  tfrlem12  8401  tz7.48lem  8453  naddcllem  8686  naddov2  8689  naddunif  8703  naddasslem1  8704  naddasslem2  8705  elixp2  8913  undifixp  8946  xpf1o  9151  nneneq  9218  ac6sfi  9290  frfi  9291  fipreima  9368  indexfi  9370  marypha1lem  9443  marypha1  9444  supeq1  9455  supeq3  9459  supmo  9462  eqsup  9466  supub  9469  suplub  9470  sup0  9477  supisoex  9485  eqinf  9495  infval  9497  infmo  9507  oieq1  9524  ordtypecbv  9529  ordtypelem3  9532  ordtypelem6  9535  ordtypelem7  9536  ordtypelem9  9538  wemaplem1  9558  wemaplem2  9559  zfregcl  9606  oemapval  9695  oemapvali  9696  cantnf  9705  wemapwe  9709  ttrcleq  9721  ttrcltr  9728  ttrclss  9732  ttrclselem2  9738  rankval3b  9838  unbndrank  9854  rankunb  9862  rankuni2b  9865  tcrank  9896  scottex  9897  scottexs  9899  scott0s  9900  bnd2  9905  updjud  9946  dfac8clem  10044  ac5num  10048  acni  10057  acni2  10058  alephval3  10122  dfac4  10134  dfac5lem5  10139  dfac5  10141  dfac2a  10142  dfac2b  10143  dfacacn  10154  kmlem2  10164  kmlem13  10175  cflem  10257  cflemOLD  10258  cflecard  10265  cfeq0  10268  cfsuc  10269  cfflb  10271  cofsmo  10281  cfsmolem  10282  cfcoflem  10284  coftr  10285  alephsing  10288  fin23lem11  10329  isfin3ds  10341  fin23lem17  10350  fin23lem39  10362  isf33lem  10378  isf34lem6  10392  fin1a2lem13  10424  hsmexlem4  10441  hsmex  10444  axcc2lem  10448  axcc3  10450  dcomex  10459  axdc2lem  10460  axdc3lem2  10463  axdc3lem3  10464  axdc3  10466  axdc4lem  10467  axcclem  10469  zorn2lem2  10509  zorn2lem7  10514  zorn2g  10515  zornn0g  10517  ttukeylem7  10527  axdclem2  10532  brdom3  10540  brdom7disj  10543  brdom6disj  10544  alephval2  10584  inar1  10787  axgroth6  10840  pinq  10939  nqereu  10941  prlem934  11045  supexpr  11066  supsrlem  11123  axpre-sup  11181  dedekind  11396  dedekindle  11397  fiminre2  12188  lbreu  12190  sup2  12196  infm3  12199  nnsub  12282  uzwo  12925  nnwof  12928  ublbneg  12947  lbzbi  12950  zsupss  12951  uzsupss  12954  uzwo3  12957  zmax  12959  rpnnen1lem1  12992  rpnnen1lem3  12993  rpnnen1lem4  12994  rpnnen1lem5  12995  xrsupsslem  13321  xrinfmsslem  13322  xrsupss  13323  xrinfmss  13324  flval2  13829  axdc4uzlem  13999  ssnn0fi  14001  fsuppmapnn0fiubex  14008  faclbnd4lem4  14312  bccl  14338  hashgt12el  14438  hashbc  14469  hashge2el2dif  14496  wrdind  14738  wrd2ind  14739  rexanre  15363  rexico  15370  cau4  15373  reusq0  15479  clim  15508  rlim  15509  rlim2  15510  clim2  15518  clim2c  15519  clim0c  15521  rlim0  15522  rlim0lt  15523  ello12r  15531  ello1d  15537  elo12r  15542  rlimresb  15579  rlimcld2  15592  climabs0  15599  rlimo1  15631  lo1add  15641  lo1mul  15642  isercoll  15682  incexclem  15850  sqrt2irr  16265  gcdcllem1  16516  gcdcllem2  16517  dfgcd2  16563  fissn0dvds  16636  dvdslcmf  16648  lcmfledvds  16649  lcmf  16650  lcmfunsnlem1  16654  lcmfunsnlem2lem1  16655  lcmfunsnlem  16658  lcmfdvds  16659  reumodprminv  16822  pc2dvds  16897  pcz  16899  prmpwdvds  16922  infpn2  16931  prmreclem2  16935  prmreclem3  16936  prmreclem5  16938  prmreclem6  16939  vdwlem6  17004  vdwlem8  17006  vdwlem13  17011  vdwnnlem1  17013  vdwnn  17016  ramcl  17047  cshwrepswhash1  17120  prdsleval  17489  imasval  17523  imasaddfnlem  17540  imasvscafn  17549  mrisval  17640  isacs  17661  isacs2  17663  isacs1i  17667  mreacs  17668  acsfn  17669  acsfn2  17673  iscatd  17683  catidex  17684  catideu  17685  cidval  17687  catidd  17690  comfeq  17716  catpropd  17719  ismon  17744  isfunc  17875  isnat  17961  isinito  18007  istermo  18008  isprs  18306  drsdirfi  18315  ispos  18324  lubfval  18358  lubeldm  18361  lubval  18364  lubprop  18366  lublecllem  18368  glbfval  18371  glbeldm  18374  glbval  18377  glbprop  18379  joinval2lem  18388  joinlem  18391  meetval2lem  18402  meetlem  18405  poslubmo  18419  posglbmo  18420  poslubd  18421  isglbd  18517  lubl  18520  lubun  18523  clatleglb  18526  isdlat  18530  ipodrsima  18549  mgm1  18634  gsumval2  18662  mgmhmima  18691  sgrp1  18705  mhmimalem  18800  mndind  18804  gsumwspan  18822  efmndmnd  18865  smndex1mnd  18886  sgrp2rid2  18902  sgrp2rid2ex  18903  sgrp2nmndlem4  18904  pwmnd  18913  dfgrp2  18943  isgrpinv  18974  grpidinv  18979  dfgrp3lem  19019  issubg4  19126  0subgOLD  19133  isnsg2  19137  nsgacs  19143  elnmz  19144  cycsubgcl  19187  ghmrn  19210  ghmnsgima  19221  isga  19272  orbsta  19294  cntzfval  19301  elcntz  19303  resscntz  19314  oppgsubg  19344  symgextfo  19401  gsmsymgreqlem2  19410  gsmsymgreq  19411  pmtrdifel  19459  pmtrdifwrdellem3  19462  pmtrdifwrdel2  19465  psgnunilem2  19474  psgnunilem3  19475  odeq  19529  gexid  19560  gexlem2  19561  gexdvds  19563  isslw  19587  sylow2alem1  19596  sylow2alem2  19597  efgval  19696  efgrelexlemb  19729  efgcpbllemb  19734  abl1  19845  dmdprd  19979  dprd2da  20023  pgpfac1lem5  20060  ring1  20268  rngisomring  20425  lringuplu  20502  rhmimasubrnglem  20523  isrrg  20656  isabv  20769  islss  20889  lssacs  20922  reslmhm  21008  islbs  21032  pj1lmhm  21056  lbsacsbs  21115  rnglidlmcl  21175  rnglidl0  21188  zringlpir  21426  psgndiflemA  21559  ocvfval  21624  elocv  21626  iunocv  21639  frlmlbs  21755  islindf  21770  islinds2  21771  islindf2  21772  lindfrn  21779  lsslindf  21788  islindf4  21796  opsrval  22002  ply1coe  22234  cply1coe0bi  22238  mat0dimcrng  22406  mdetunilem1  22548  mdetunilem9  22556  cpmat  22645  cpmatel  22647  1elcpmat  22651  m2cpminvid2lem  22690  basgen2  22925  bastop1  22929  isclo  23023  ordtbaslem  23124  iscn  23171  cnpval  23172  iscnp  23173  iscnp3  23180  lmbr  23194  lmbr2  23195  lmbrf  23196  cnprest  23225  cnprest2  23226  t0sep  23260  isreg  23268  t1sep2  23305  tgcmp  23337  1stcclb  23380  1stcfb  23381  2ndc1stc  23387  1stcrest  23389  2ndcdisj  23392  islly  23404  isnlly  23405  lly1stc  23432  isref  23445  islocfin  23453  elkgen  23472  kgencn  23492  elpt  23508  elptr  23509  ptcnplem  23557  tx1stc  23586  cnmpt21  23607  kqt0lem  23672  isr0  23673  regr1lem2  23676  r0sep  23684  nrmr0reg  23685  flffbas  23931  cnflf  23938  cnflf2  23939  lmflf  23941  txflf  23942  fclsopni  23951  fclsnei  23955  fclsrest  23960  fcfnei  23971  cnfcf  23978  alexsubb  23982  alexsubALTlem3  23985  qustgplem  24057  tsmsfbas  24064  tsmsres  24080  tsmsf1o  24081  tsmsxplem1  24089  ustval  24139  isust  24140  ustincl  24144  ustdiag  24145  ustinvel  24146  ustexhalf  24147  ust0  24156  utopval  24169  ucnval  24213  isucn  24214  isucn2  24215  ucnima  24217  iscfilu  24224  ispsmet  24241  ismet  24260  isxmet  24261  imasdsf1olem  24310  imasf1oxmet  24312  imasf1omet  24313  metss  24445  met1stc  24458  prdsxmslem2  24466  txmetcnp  24484  metucn  24508  tngngp3  24593  nlmvscn  24624  nmoval  24652  nmolb  24654  qtopbaslem  24695  cncfval  24830  elcncf2  24832  mulc1cncf  24847  cncfmet  24851  evth  24907  lebnumlem3  24911  lebnum  24912  xlebnum  24913  ishtpy  24920  isphtpy  24929  pi1xfr  25004  pi1coghm  25010  isclmp  25046  ipcn  25196  lmmbr2  25209  lmmbr3  25210  lmmbrf  25212  cfilfval  25214  iscfil  25215  fmcfil  25222  caufval  25225  iscau  25226  iscau2  25227  iscau3  25228  iscau4  25229  iscauf  25230  caucfil  25233  cfilresi  25245  causs  25248  lmclim  25253  cmetcusp1  25303  minveclem4c  25375  minveclem2  25376  minveclem3b  25378  minveclem4  25382  minveclem6  25384  minveclem7  25385  ovolicc2lem3  25470  ismbl  25477  dyadmax  25549  dyadmbllem  25550  dyadmbl  25551  opnmbllem  25552  ismbf1  25575  ismbf  25579  mbfeqalem2  25593  mbflimsup  25617  mbfi1fseqlem6  25671  mbfi1flimlem  25673  itg2seq  25693  itg2monolem1  25701  isibl  25716  ply1divex  26092  fta1g  26125  dgrco  26231  plydivex  26255  fta1  26266  vieta1  26270  aannenlem1  26286  aannenlem2  26287  aalioulem2  26291  aalioulem3  26292  ulmval  26339  ulm2  26344  ulmi  26345  ulmres  26347  ulmshftlem  26348  ulmcaulem  26353  ulmcau  26354  ulmss  26356  ulmbdd  26357  ulmdvlem1  26359  ulmdvlem3  26361  pilem2  26412  pilem3  26413  cxpcn3  26708  dmarea  26917  rlimcnp  26925  scvxcvx  26946  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem5  26993  lgambdd  26997  lgamcvglem  27000  isppw2  27075  perfectlem2  27191  2sqlem6  27384  2sqlem10  27389  addsq2reu  27401  2sqreulem1  27407  2sqreunnlem1  27410  dchrisumlema  27449  dchrisumlem2  27451  dchrisumlem3  27452  pntpbnd  27549  pntibndlem3  27553  pntibnd  27554  pntleme  27569  pntlem3  27570  pntlemp  27571  pnt3  27573  sltval  27609  nosupprefixmo  27662  noinfprefixmo  27663  nosupcbv  27664  nosupno  27665  nosupdm  27666  nosupfv  27668  nosupres  27669  nosupbnd1lem1  27670  nosupbnd1lem3  27672  nosupbnd1lem5  27674  noinfcbv  27679  noinfno  27680  noinfdm  27681  noinffv  27683  noinfres  27684  noinfbnd1lem3  27687  noinfbnd1lem5  27689  noetalem1  27703  noetalem2  27704  nocvxminlem  27739  brsslt  27747  conway  27761  etasslt  27775  slerec  27781  madebdaylemlrcut  27854  madebday  27855  cofcutr  27875  cutmax  27885  cutmin  27886  lrrecfr  27893  addsprop  27926  negsunif  28004  n0subs  28277  zs12bday  28341  istrkgld  28384  axtg5seg  28390  tgcgr4  28456  perpln1  28635  perpln2  28636  isperp  28637  brbtwn2  28830  colinearalg  28835  axsegconlem1  28842  axsegcon  28852  ax5seglem4  28857  ax5seglem5  28858  axlowdim  28886  axeuclidlem  28887  axcontlem1  28889  axcontlem2  28890  axcontlem4  28892  axcontlem5  28893  axcontlem8  28896  axcontlem12  28900  elntg2  28910  uvtxusgr  29327  rgrx0ndm  29519  ewlksfval  29527  wksfval  29535  wwlks  29763  wlkiswwlks2  29803  clwwlk  29910  1conngr  30121  frgrwopregasn  30243  frgrwopregbsn  30244  frgrwopreglem5ALT  30249  frgrregord013  30322  isgrpo  30424  isgrpoi  30425  grpoideu  30436  grpoidinv2  30442  vciOLD  30488  isvclem  30504  cnidOLD  30509  isnvlem  30537  nvi  30541  lnoval  30679  islno  30680  isblo3i  30728  blo3i  30729  blocnilem  30731  ajfval  30736  ubthlem1  30797  ubthlem2  30798  ubthlem3  30799  ubth  30800  minvecolem2  30802  minvecolem3  30803  minvecolem4c  30806  minvecolem4  30807  minvecolem5  30808  minvecolem6  30809  minvecolem7  30810  h2hcau  30906  h2hlm  30907  hilid  31088  hcau  31111  hlimi  31115  hlim2  31119  ocel  31208  adjsym  31760  ellnop  31785  ellnfn  31810  hhcno  31831  hhcnf  31832  lnopeq  31936  elunop2  31940  lnophm  31946  lnconi  31960  lnopcnbd  31963  lnfncnbd  31984  imaelshi  31985  riesz3i  31989  riesz4i  31990  riesz4  31991  riesz1  31992  cnlnadjlem2  31995  cnlnadjlem5  31998  cnlnadjlem8  32001  cnlnadji  32003  nmopadjlei  32015  cnvbraval  32037  leopg  32049  leoppos  32053  mdbr  32221  dmdbr  32226  cdj3i  32368  disjunsn  32521  funcnv5mpt  32592  fgreu  32596  fcnvgreu  32597  xrge0infss  32683  wrdt2ind  32875  resspos  32892  mgccole1  32916  mgccole2  32917  mgcmnt1  32918  mgcmnt2  32919  gsumhashmul  33001  isomnd  33015  inftmrel  33124  isinftm  33125  archiabl  33142  elrgspnlem4  33186  isarchiofld  33285  0nellinds  33331  lindssn  33339  elrspunidl  33389  prmidl  33401  ismxidl  33423  1arithidom  33498  1arithufdlem3  33507  evl1deg1  33535  evl1deg2  33536  evl1deg3  33537  crefeq  33822  zarcmplem  33858  esum2d  34070  sigaval  34088  issgon  34100  isrnmeas  34177  ismbfm  34228  mbfmcst  34237  elcarsg  34283  sitgval  34310  eulerpartlemd  34344  ballotleme  34475  tgoldbachgt  34641  bnj1185  34770  bnj1385  34809  bnj66  34837  bnj106  34845  bnj155  34856  bnj852  34898  bnj893  34905  bnj1228  34988  bnj1234  34990  bnj1463  35032  nummin  35068  gblacfnacd  35076  derangenlem  35139  subfacp1lem3  35150  subfacp1lem5  35152  subfacp1lem6  35153  subfacp1  35154  erdszelem8  35166  kur14  35184  cnpconn  35198  resconn  35214  cvmscbv  35226  iscvm  35227  cvmsi  35233  cvmsval  35234  cvmlift3lem2  35288  snmlval  35299  satfv1  35331  fmlasucdisj  35367  satffunlem1lem1  35370  satffunlem2lem1  35372  satfv1fvfmla1  35391  mclsssvlem  35530  mclsval  35531  mclsax  35537  mclsind  35538  dfon2lem9  35755  dfrdg2  35759  dfrdg3  35760  fwddifnval  36127  nn0prpwlem  36286  isfne  36303  isfne4  36304  isfne2  36306  isfne3  36307  neibastop3  36326  topmeet  36328  topjoin  36329  filnetlem4  36345  weiunlem2  36427  weiunfrlem  36428  unblimceq0lem  36470  unblimceq0  36471  unbdqndv2  36475  taupilemrplb  37284  fin2so  37577  lindsadd  37583  matunitlindflem2  37587  ptrecube  37590  poimirlem2  37592  poimirlem3  37593  poimirlem4  37594  poimirlem24  37614  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimirlem28  37618  poimirlem29  37619  poimirlem30  37620  poimirlem32  37622  poimir  37623  heicant  37625  mblfinlem1  37627  mblfinlem2  37628  voliunnfl  37634  volsupnfl  37635  mbfresfi  37636  itg2addnc  37644  upixp  37699  indexdom  37704  filbcmb  37710  sdclem2  37712  fdc  37715  lmclim2  37728  caures  37730  istotbnd  37739  istotbnd3  37741  sstotbnd  37745  isbnd  37750  heibor  37791  bfp  37794  rrncmslem  37802  isgrpda  37925  idlval  37983  isidl  37984  0idl  37995  unichnidl  38001  pridl  38007  ismaxidl  38010  smprngopr  38022  igenval2  38036  prnc  38037  ispridlc  38040  scottexf  38138  scott0f  38139  disjsuc2  38355  riotasvd  38920  islfl  39024  eqlkr  39063  eqlkr3  39065  glbconN  39341  glbconNOLD  39342  hlsuprexch  39346  ispsubsp  39710  ldilset  40074  isldil  40075  dilsetN  40118  isdilN  40119  trlset  40126  trlval  40127  cdleme27b  40333  cdleme29b  40340  cdleme31so  40344  cdleme31sn1  40346  cdleme31sn1c  40353  cdleme31fv  40355  cdleme40v  40434  istendo  40725  cdlemkid3N  40898  cdlemkid4  40899  cdlemkid5  40900  dihfval  41196  dihval  41197  islpolN  41448  hdmapffval  41791  hdmapfval  41792  hdmapval  41793  hdmapval2lem  41796  hgmapffval  41850  hgmapfval  41851  hgmapval  41852  hgmapvs  41856  isprimroot  42052  aks6d1c1p1  42066  hashscontpow1  42080  sticksstones2  42106  unitscyglem3  42156  exfinfldd  42162  qsalrel  42238  supinf  42240  sn-sup2  42461  fsuppind  42560  isnacs  42674  isnacs2  42676  nacsfix  42682  mzpclval  42695  elmzpcl  42696  rencldnfilem  42790  infmrgelbi  42848  pellfundre  42851  pellfundlb  42854  wepwsolem  43013  fnwe2lem2  43022  aomclem8  43032  dfac11  43033  gicabl  43070  islnr3  43086  hbtlem2  43095  hbtlem5  43099  onintunirab  43198  onsucf1lem  43240  cantnfresb  43295  safesnsupfilb  43389  rp-brsslt  43394  fiinfi  43544  clsk1independent  44017  ntrclsk13  44042  gneispacess2  44117  imo72b2lem0  44136  imo72b2lem2  44138  imo72b2lem1  44140  imo72b2  44143  scottelrankd  44219  mnuop23d  44238  ismnushort  44273  ralabsobidv  44945  0elaxnul  44956  pwclaxpow  44957  prclaxpr  44958  uniclaxun  44959  omssaxinf2  44961  modelac8prim  44965  wfac8prim  44975  evth2f  44987  evthf  44999  fnchoice  45001  uzwo4  45025  wessf1ornlem  45157  disjinfi  45164  rnmptlb  45215  rnmptbdd  45217  rnmptbd2  45221  rnmptbd  45228  dstregt0  45258  upbdrech2  45285  rexabslelem  45393  rexabsle  45394  uzub  45406  infrpgernmpt  45440  mccl  45575  ellimcabssub0  45594  climf  45599  clim2f  45613  limsupre  45618  clim2cf  45627  clim0cf  45631  climf2  45643  clim2f2  45647  clim2d  45650  limsupref  45662  limsupbnd1f  45663  climinf2  45684  limsuppnf  45688  climinfmpt  45692  climinf3  45693  limsupubuzmpt  45696  limsupmnf  45698  limsupre2lem  45701  limsupre2  45702  limsupmnfuzlem  45703  limsupmnfuz  45704  limsupre2mpt  45707  limsupre3lem  45709  limsupre3  45710  limsupre3mpt  45711  limsupre3uz  45713  limsupreuz  45714  limsupreuzmpt  45716  climuz  45721  liminfreuzlem  45779  liminfreuz  45780  cnrefiisplem  45806  xlimmnfvlem1  45809  xlimmnfv  45811  xlimpnfvlem1  45813  xlimpnfv  45815  xlimmnfmpt  45820  xlimpnfmpt  45821  cncfshift  45851  cncfperiod  45856  fperdvper  45896  dvbdfbdioo  45907  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnprodlem3  45925  stoweidlem5  45982  stoweidlem9  45986  stoweidlem15  45992  stoweidlem16  45993  stoweidlem27  46004  stoweidlem28  46005  stoweidlem31  46008  stoweidlem34  46011  stoweidlem37  46014  stoweidlem46  46023  stoweidlem48  46025  stoweidlem51  46028  stoweidlem52  46029  stoweidlem59  46036  wallispilem3  46044  stirlinglem13  46063  fourierdlem2  46086  fourierdlem3  46087  fourierdlem16  46100  fourierdlem20  46104  fourierdlem21  46105  fourierdlem22  46106  fourierdlem25  46109  fourierdlem39  46123  fourierdlem42  46126  fourierdlem54  46137  fourierdlem64  46147  fourierdlem77  46160  fourierdlem83  46166  fourierdlem103  46186  fourierdlem104  46187  subsaliuncllem  46334  iundjiun  46437  meaiunincf  46460  caragenval  46470  isome  46471  caragenel  46472  omessle  46475  ovnlerp  46539  hoidmvlelem3  46574  hoidmvle  46577  issmflem  46704  issmfgt  46733  smfmullem2  46769  smfmullem4  46771  smfmul  46772  smfsuplem2  46789  smfsup  46791  smfinflem  46794  smfinf  46795  fsupdm  46819  finfdm  46823  cfsetsnfsetf  47035  cbvral2  47080  2reu8i  47090  2reuimp0  47091  dfdfat2  47105  iccpart  47378  iccpartigtl  47385  paireqne  47473  reupr  47484  perfectALTVlem2  47684  bgoldbachlt  47775  tgoldbachlt  47778  grimidvtxedg  47846  grimcnv  47849  grimco  47850  isuspgrim0  47855  gricushgr  47878  ushggricedg  47888  uhgrimisgrgric  47892  isubgr3stgr  47935  isgrlim  47942  isgrlim2  47943  uspgrlim  47952  grlicsym  47966  grlictr  47968  gpg5nbgrvtx03star  48030  gpg5nbgr3star  48031  upwlksfval  48058  nn0mnd  48102  uzlidlring  48158  ply1mulgsumlem1  48310  ply1mulgsumlem2  48311  linindslinci  48372  lindslinindsimp1  48381  lindslinindsimp2lem5  48386  lindslinindsimp2  48387  linds0  48389  lindsrng01  48392  snlindsntor  48395  lmod1  48416  ldepsnlinc  48432  bigoval  48477  elbigo2r  48481  nn0sumshdiglem2  48550  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  lubeldm2d  48880  glbeldm2d  48881  lubsscl  48882  glbsscl  48883  ipolubdm  48909  ipolub  48910  ipoglbdm  48912  ipoglb  48913  nelsubc3lem  48985  upfval2  49060  upfval3  49061  isthincd2lem2  49269  setc1onsubc  49427  cnelsubclem  49428  setrec1lem2  49500