Theorem ralbidv 2810

Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)

Hypothesis

Ref	Expression
ralbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
ralbidv	|- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem ralbidv

Step	Hyp	Ref	Expression
1		ralbidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	adantr 471	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	ralbidva 2809	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 189   e. wcel 1891   A.wral 2737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762

This theorem depends on definitions:  df-bi 190  df-an 377  df-ral 2742

This theorem is referenced by:  2ralbidv  2813  rexralbidv  2879  raleqbi1dv  2963  raleqbidv  2969  cbvral2v  2995  rspc2  3126  rspc3v  3130  reu6i  3197  reu7  3201  sbcralt  3308  raaan  3845  raaanv  3846  2ralsng  3976  r19.12snOLD  4007  2ralunsn  4157  elintg  4212  elintrabg  4217  eliin  4254  disjprg  4370  disjxun  4372  reusv2lem2  4578  reusv3  4584  poeq1  4736  somo  4767  frirr  4789  fr2nr  4790  frminex  4792  wereu2  4809  posn  4881  frsn  4883  ralxpf  4959  cnvpo  5353  fnmptfvd  5969  iinpreima  5994  dff4  6020  dff13f  6146  eusvobj2  6269  ofreq  6522  sorpssuni  6568  sorpssint  6569  fr3nr  6594  onssmin  6612  funcnvuni  6734  f1oweALT  6765  frxp  6894  wrecseq123  7016  wfrlem1  7022  wfrlem3a  7025  wfrlem15  7037  smoeq  7056  tfrlem12  7094  tz7.48lem  7145  elixp2  7513  undifixp  7545  xpf1o  7721  nneneq  7742  ac6sfi  7802  frfi  7803  fipreima  7867  indexfi  7869  marypha1lem  7934  marypha1  7935  supeq1  7946  supeq3  7950  supmo  7953  eqsup  7957  supub  7960  suplub  7961  sup0  7967  supmaxlemOLD  7969  supisoex  7977  eqinf  7987  infval  7989  infmo  7998  oieq1  8014  ordtypecbv  8019  ordtypelem3  8022  ordtypelem6  8025  ordtypelem7  8026  ordtypelem9  8028  wemaplem1  8048  wemaplem2  8049  zfregcl  8096  oemapval  8175  oemapvali  8176  cantnf  8185  wemapwe  8189  rankval3b  8284  unbndrank  8300  rankunb  8308  rankuni2b  8311  tcrank  8342  scottex  8343  scottexs  8345  scott0s  8346  bnd2  8351  dfac8clem  8450  ac5num  8454  acni  8463  acni2  8464  alephval3  8528  dfac4  8540  dfac5lem5  8545  dfac5  8546  dfac2a  8547  dfac2  8548  dfacacn  8558  kmlem2  8568  kmlem13  8579  cflem  8663  cflecard  8670  cfeq0  8673  cfsuc  8674  cfflb  8676  cofsmo  8686  cfsmolem  8687  cfcoflem  8689  coftr  8690  alephsing  8693  fin23lem11  8734  isfin3ds  8746  fin23lem17  8755  fin23lem39  8767  isf33lem  8783  isf34lem6  8797  fin1a2lem13  8829  hsmexlem4  8846  hsmex  8849  axcc2lem  8853  axcc3  8855  dcomex  8864  axdc2lem  8865  axdc3lem2  8868  axdc3lem3  8869  axdc3  8871  axdc4lem  8872  axcclem  8874  zorn2lem2  8914  zorn2lem7  8919  zorn2g  8920  zornn0g  8922  ttukeylem7  8932  axdclem2  8937  brdom3  8943  brdom7disj  8946  brdom6disj  8947  alephval2  8984  inar1  9187  axgroth6  9240  pinq  9339  nqereu  9341  prlem934  9445  supexpr  9466  supsrlem  9522  axpre-sup  9580  dedekind  9784  dedekindle  9785  fimaxre2  10541  fiminre  10544  lbreu  10545  sup2  10554  infm3  10557  supaddc  10563  supadd  10564  supmul1  10565  supmullem2  10567  supmul  10568  infmrclOLD  10582  nnsub  10637  uzwo  11212  nnwof  11215  uzinfmiOLD  11229  ublbneg  11238  lbzbi  11242  zsupss  11243  uzsupss  11246  uzwo3  11249  zmax  11251  rpnnen1lem1  11280  rpnnen1lem2  11281  rpnnen1lem3  11282  rpnnen1lem4  11283  rpnnen1lem5  11284  xrsupsslem  11582  xrinfmsslem  11583  xrsupss  11584  xrinfmss  11585  iccsupr  11717  supicc  11771  supiccub  11772  supicclub  11773  flval2  12043  flval3  12044  fsequb  12182  axdc4uzlem  12189  ssnn0fi  12191  fsuppmapnn0fiubex  12198  faclbnd4lem4  12475  bccl  12501  hashgt12el  12590  hashbc  12611  hashge2el2dif  12632  wrdind  12832  wrd2ind  12833  sqrlem3  13319  rexanre  13420  rexico  13427  cau4  13430  caubnd2  13431  caubnd  13432  clim  13569  rlim  13570  rlim2  13571  rlim2lt  13572  rlim3  13573  clim2  13579  clim2c  13580  clim0c  13582  rlim0  13583  rlim0lt  13584  ello12r  13592  ello1d  13598  lo1bdd2  13599  lo1bddrp  13600  elo12r  13603  rlimconst  13619  rlimresb  13640  rlimcld2  13653  climabs0  13660  rlimcn2  13665  reccn2  13671  cn1lem  13672  rlimo1  13691  o1rlimmul  13693  lo1add  13701  lo1mul  13702  isercoll  13742  caucvgrlem  13747  caucvgrlemOLD  13748  incexclem  13905  climcnds  13920  divrcnv  13921  ruclem12  14304  sqrt2irr  14312  gcdcllem1  14484  gcdcllem2  14485  lcmscllemOLD  14593  lcmsOLD  14595  lcmsledvdsOLD  14596  fissn0dvds  14600  dvdslcmf  14615  lcmfledvds  14616  lcmf  14617  lcmfunsnlem1  14621  lcmfunsnlem2lem1  14622  lcmfunsnlem  14625  lcmfdvds  14626  maxprmfct  14663  reumodprminv  14766  pc2dvds  14839  pcz  14841  prmpwdvds  14859  infpn2  14868  prmreclem1  14871  prmreclem2  14872  prmreclem3  14873  prmreclem5  14875  prmreclem6  14876  vdwlem6  14947  vdwlem8  14949  vdwlem13  14954  vdwnnlem1  14956  vdwnn  14959  ramz  14994  ramcl  14998  prmgaplcmlem1OLD  15023  prmordvdslcmsOLDOLD  15032  cshwrepswhash1  15084  prdsleval  15386  imasval  15422  imasvalOLD  15423  imasaddfnlem  15445  imasvscafn  15454  mrisval  15547  isacs  15568  isacs2  15570  isacs1i  15574  mreacs  15575  acsfn  15576  acsfn2  15580  iscatd  15590  catidex  15591  catideu  15592  cidval  15594  catidd  15597  comfeq  15622  catpropd  15625  ismon  15649  isfunc  15780  isnat  15863  isinito  15906  istermo  15907  isprs  16186  drsdirfi  16194  ispos  16203  lubfval  16235  lubeldm  16238  lubval  16241  lubprop  16243  lublecllem  16245  glbfval  16248  glbeldm  16251  glbval  16254  glbprop  16256  joinval2lem  16265  joinlem  16268  meetval2lem  16279  meetlem  16282  isglbd  16374  lubl  16377  lubun  16380  clatleglb  16383  poslubmo  16403  posglbmo  16404  poslubd  16405  ipodrsima  16422  isdlat  16450  mgm1  16511  mgmidmo  16513  ismgmid  16518  ismgmid2  16521  mgmidsssn0  16523  gsumvalx  16524  gsumress  16530  gsumval2  16534  sgrp1  16545  mndclOLD  16558  mndassOLD  16559  ismndd  16570  mnd1  16588  mnd1OLD  16589  mhmima  16621  mrcmndind  16624  gsumvallem2  16630  gsumwspan  16641  sgrp2rid2  16671  sgrp2rid2ex  16672  sgrp2nmndlem4  16673  isgrpinv  16727  mhmmnd  16819  issubg4  16847  0subg  16853  cycsubgcl  16854  isnsg2  16858  nsgacs  16864  elnmz  16867  ghmrn  16907  ghmnsgima  16917  isga  16956  orbsta  16978  cntzfval  16985  elcntz  16987  resscntz  16996  oppgsubg  17025  symgextfo  17074  gsmsymgreqlem2  17083  gsmsymgreq  17084  pmtrdifel  17132  pmtrdifwrdellem3  17135  pmtrdifwrdel2  17138  psgnunilem2  17147  psgnunilem3  17148  odeq  17210  gexid  17243  gexlem2  17244  gexdvds  17246  gexlem2OLD  17247  isslw  17271  pgpssslw  17277  sylow2alem1  17280  sylow2alem2  17281  efgval  17378  efgrelexlemb  17411  efgcpbllemb  17416  gexex  17502  abl1  17515  dmdprd  17641  dprd2da  17686  pgpfac1lem5  17723  ring1  17841  isabv  18058  islss  18169  lssacs  18201  reslmhm  18286  islbs  18310  pj1lmhm  18334  lbsacsbs  18390  isrrg  18523  opsrval  18709  ply1coe  18900  cply1coe0bi  18905  zringlpir  19069  zringlpirOLD  19070  psgndiflemA  19180  ocvfval  19240  elocv  19242  iunocv  19255  frlmlbs  19366  islindf  19381  islinds2  19382  islindf2  19383  lindfrn  19390  lsslindf  19399  islindf4  19407  mat0dimcrng  19506  mdetunilem1  19648  mdetunilem9  19656  cpmat  19744  cpmatel  19746  1elcpmat  19750  m2cpminvid2lem  19789  chfacffsupp  19891  chfacfscmulfsupp  19894  chfacfpmmulfsupp  19898  basgen2  20016  bastop1  20020  isclo  20114  ordtbaslem  20215  iscn  20262  cnpval  20263  iscnp  20264  iscnp3  20271  lmbr  20285  lmbr2  20286  lmbrf  20287  cnprest  20316  cnprest2  20317  t0sep  20351  isreg  20359  t1sep2  20396  tgcmp  20427  1stcclb  20470  1stcfb  20471  2ndc1stc  20477  1stcrest  20479  2ndcdisj  20482  islly  20494  isnlly  20495  lly1stc  20522  isref  20535  islocfin  20543  elkgen  20562  kgencn  20582  elpt  20598  elptr  20599  ptcnplem  20647  tx1stc  20676  cnmpt21  20697  kqt0lem  20762  isr0  20763  regr1lem2  20766  r0sep  20774  nrmr0reg  20775  flffbas  21021  cnflf  21028  cnflf2  21029  lmflf  21031  txflf  21032  fclsopni  21041  fclsnei  21045  fclsrest  21050  fcfnei  21061  cnfcf  21068  alexsubb  21072  alexsubALTlem3  21075  qustgplem  21146  tsmsfbas  21153  tsmsgsum  21164  tsmsres  21169  tsmsf1o  21170  tsmsxplem1  21178  tsmsxp  21180  ustval  21228  isust  21229  ustincl  21233  ustdiag  21234  ustinvel  21235  ustexhalf  21236  ust0  21245  utopval  21258  ucnval  21303  isucn  21304  isucn2  21305  ucnima  21307  iscfilu  21314  ispsmet  21331  ismet  21349  isxmet  21350  imasdsf1olem  21399  imasf1oxmet  21401  imasf1omet  21402  metss  21534  met1stc  21547  prdsxmslem2  21555  metcnpi3  21572  txmetcnp  21573  metucn  21597  nlmvscn  21701  nrginvrcnlem  21704  nmoval  21731  nmolb  21733  nmovalOLD  21750  nmolbOLD  21752  nghmcn  21777  qtopbaslem  21790  icccmplem2  21852  icccmplem3  21853  reconnlem2  21856  metdscn  21884  metdscnOLD  21899  cncfval  21931  elcncf2  21933  elcncf1di  21938  mulc1cncf  21948  cncfmet  21951  cnllycmp  21995  evth  21998  lebnumlem3  22002  lebnumlem3OLD  22005  lebnum  22006  xlebnum  22007  ishtpy  22014  isphtpy  22023  pi1xfr  22097  pi1coghm  22103  ipcn  22228  lmmbr2  22240  lmmbr3  22241  lmmbrf  22243  cfilfval  22245  iscfil  22246  fmcfil  22253  caufval  22256  iscau  22257  iscau2  22258  iscau3  22259  iscau4  22260  iscauf  22261  caucfil  22264  cfilresi  22276  causs  22279  lmclim  22283  cncmet  22301  cmetcusp1  22331  minveclem4c  22378  minveclem2  22379  minveclem3b  22381  minveclem4  22385  minveclem6  22387  minveclem7  22388  minveclem4cOLD  22390  minveclem2OLD  22391  minveclem3bOLD  22393  minveclem4OLD  22397  minveclem6OLD  22399  minveclem7OLD  22400  ivthlem2  22414  ivthlem3  22415  cniccbdd  22423  ovolunlem1  22461  ovoliunlem1  22466  ovoliun2  22470  ovolicc2lem3  22483  ismbl  22491  ioombl1lem4  22526  uniioombllem2  22552  uniioombllem2OLD  22553  uniioombllem6  22558  dyadmax  22568  dyadmbllem  22569  dyadmbl  22570  opnmbllem  22571  volcn  22576  ismbf1  22594  ismbf  22598  mbfeqalem  22610  mbfinf  22633  mbfinfOLD  22634  mbflimsup  22635  mbflimsupOLD  22636  itg1climres  22684  mbfi1fseqlem6  22690  mbfi1flimlem  22692  itg2seq  22712  itg2monolem1  22720  itg2i1fseq  22725  itg2i1fseq2  22726  itg2cnlem1  22731  itg2cnlem2  22732  isibl  22735  dveflem  22943  ply1divex  23099  fta1g  23130  plyeq0lem  23176  dgrco  23241  plydivex  23262  fta1  23273  vieta1  23277  aannenlem1  23296  aannenlem2  23297  aalioulem2  23301  aalioulem3  23302  ulmval  23347  ulm2  23352  ulmi  23353  ulmres  23355  ulmshftlem  23356  ulmcaulem  23361  ulmcau  23362  ulmss  23364  ulmbdd  23365  ulmdvlem1  23367  ulmdvlem3  23369  mtestbdd  23372  iblulm  23374  abelthlem8  23406  pilem2  23419  pilem2OLD  23420  pilem3  23421  pilem3OLD  23422  divlogrlim  23592  cxpcn3  23700  dmarea  23895  rlimcnp  23903  cxplim  23909  cxploglim  23915  scvxcvx  23923  emcllem6  23938  lgamgulmlem2  23967  lgamgulmlem3  23968  lgamgulmlem5  23970  lgambdd  23974  lgamcvglem  23977  ftalem1  24009  ftalem2  24010  ftalem3  24011  isppw2  24054  perfectlem2  24170  2sqlem6  24309  2sqlem10  24314  dchrisumlema  24338  dchrisumlem2  24340  dchrisumlem3  24341  dchrisum0  24370  pntpbnd  24438  pntibndlem3  24442  pntibnd  24443  pntleme  24458  pntlem3  24459  pntlemp  24460  pnt3  24462  istrkgld  24519  axtg5seg  24525  tgcgr4  24588  perpln1  24767  perpln2  24768  isperp  24769  brbtwn2  24947  colinearalg  24952  axsegconlem1  24959  axsegcon  24969  ax5seglem4  24974  ax5seglem5  24975  axlowdim  25003  axeuclidlem  25004  axcontlem1  25006  axcontlem2  25007  axcontlem4  25009  axcontlem5  25010  axcontlem8  25013  axcontlem12  25017  cusgra3v  25204  wlks  25259  wlkcompim  25266  wlkelwrd  25270  wlkntrllem3  25303  constr3trllem2  25391  1conngra  25415  wwlk  25421  clwwlk  25506  isrgrac  25674  rusgra0edg  25695  iseupa  25705  frgrawopreg1  25790  frgrawopreg2  25791  frgrareg  25857  frgraregord013  25858  isgrpo  25936  isgrpo2  25937  isgrpoi  25938  grpoideu  25949  grpoidinv2  25958  isgrp2d  25975  isgrpda  26037  exidu1  26066  cmpidelt  26069  cnid  26091  mulid  26096  ghgrpOLD  26108  isrngod  26119  rngoideu  26124  cnrngo  26143  vci  26179  isvclem  26208  isnvlem  26241  nvi  26245  nmcvcn  26343  lnoval  26405  islno  26406  isblo3i  26454  blo3i  26455  blocnilem  26457  blocni  26458  ajfval  26462  ubthlem1  26524  ubthlem2  26525  ubthlem3  26526  ubth  26527  minvecolem2  26529  minvecolem3  26530  minvecolem4c  26533  minvecolem4  26534  minvecolem5  26535  minvecolem6  26536  minvecolem7  26537  minvecolem2OLD  26539  minvecolem3OLD  26540  minvecolem4cOLD  26543  minvecolem4OLD  26544  minvecolem5OLD  26545  minvecolem6OLD  26546  minvecolem7OLD  26547  htthlem  26582  h2hcau  26644  h2hlm  26645  hilid  26826  hcau  26849  hlimi  26853  hlim2  26857  ocel  26946  adjsym  27498  ellnop  27523  ellnfn  27548  hhcno  27569  hhcnf  27570  0cnop  27644  0cnfn  27645  idcnop  27646  lnopeq  27674  elunop2  27678  lnophm  27684  lnconi  27698  lnopcnbd  27701  lnfncnbd  27722  imaelshi  27723  riesz3i  27727  riesz4i  27728  riesz4  27729  riesz1  27730  cnlnadjlem2  27733  cnlnadjlem5  27736  cnlnadjlem8  27739  cnlnadji  27741  nmopadjlei  27753  cnvbraval  27775  leopg  27787  leoppos  27791  mdbr  27959  dmdbr  27964  cdj3i  28106  rmoeqALT  28135  disjunsn  28214  funcnv5mpt  28280  fgreu  28282  fcnvgreu  28283  xrge0infss  28348  xrge0infssOLD  28349  resspos  28428  isomnd  28471  inftmrel  28504  isinftm  28505  archiabl  28522  rngurd  28558  isarchiofld  28587  crefeq  28679  rge0scvg  28762  qqhcn  28802  esumpcvgval  28906  esum2d  28921  sigaval  28939  issgon  28952  isrnmeas  29029  ismbfm  29080  isanmbfm  29084  mbfmcst  29087  elcarsg  29143  sitgval  29171  oddpwdc  29193  eulerpartlemd  29205  ballotleme  29335  signsw0g  29451  signswmnd  29452  bnj1185  29611  bnj1385  29650  bnj66  29677  bnj106  29685  bnj155  29696  bnj852  29738  bnj893  29745  bnj1228  29826  bnj1234  29828  bnj1463  29870  derangenlem  29900  subfacp1lem3  29911  subfacp1lem5  29913  subfacp1lem6  29914  subfacp1  29915  erdszelem8  29927  kur14  29945  cnpcon  29959  rescon  29975  cvmscbv  29987  iscvm  29988  cvmsi  29994  cvmsval  29995  cvmlift3lem2  30049  snmlval  30060  mclsssvlem  30206  mclsval  30207  mclsax  30213  mclsind  30214  ghomgrpilem1  30309  dfpo2  30401  dfon2lem9  30443  dfrdg2  30448  dfrdg3  30449  poseq  30497  soseq  30498  frrlem1  30520  sltval  30540  nocvxminlem  30585  nobndlem2  30588  nobndlem8  30594  nobndup  30595  nobnddown  30596  fwddifnval  30936  nn0prpwlem  30984  isfne  31001  isfne4  31002  isfne2  31004  isfne3  31005  neibastop3  31024  topmeet  31026  topjoin  31027  filnetlem4  31043  taupilemrplb  31723  csbwrecsg  31730  fin2so  31934  ptrecube  31942  poimirlem2  31944  poimirlem3  31945  poimirlem4  31946  poimirlem24  31966  poimirlem25  31967  poimirlem26  31968  poimirlem27  31969  poimirlem28  31970  poimirlem29  31971  poimirlem30  31972  poimirlem32  31974  poimir  31975  heicant  31977  mblfinlem1  31979  mblfinlem2  31980  mblfinlem3  31981  ismblfin  31983  voliunnfl  31986  volsupnfl  31987  mbfresfi  31989  itg2addnc  31998  ftc1anc  32027  f1opr  32053  upixp  32058  indexdom  32063  filbcmb  32069  sdclem2  32073  fdc  32076  lmclim2  32089  caures  32091  istotbnd  32103  istotbnd3  32105  sstotbnd  32109  isbnd  32114  heibor  32155  bfp  32158  rrncmslem  32166  exidres  32178  exidresid  32179  idlval  32248  isidl  32249  0idl  32260  unichnidl  32266  pridl  32272  ismaxidl  32275  smprngopr  32287  igenval2  32301  prnc  32302  ispridlc  32305  scottexf  32413  scott0f  32414  riotasvd  32530  islfl  32628  eqlkr  32667  eqlkr3  32669  glbconN  32944  hlsuprexch  32948  ispsubsp  33312  ldilset  33676  isldil  33677  dilsetN  33721  isdilN  33722  trlset  33729  trlval  33730  cdleme27b  33937  cdleme29b  33944  cdleme31so  33948  cdleme31sn1  33950  cdleme31sn1c  33957  cdleme31fv  33959  cdleme40v  34038  istendo  34329  cdlemkid3N  34502  cdlemkid4  34503  cdlemkid5  34504  dihfval  34801  dihval  34802  islpolN  35053  hdmapffval  35399  hdmapfval  35400  hdmapval  35401  hdmapval2lem  35404  hgmapffval  35458  hgmapfval  35459  hgmapval  35460  hgmapvs  35464  isnacs  35548  isnacs2  35550  nacsfix  35556  mzpclval  35569  elmzpcl  35570  rencldnfilem  35665  infmrgelbi  35726  infmrgelbiOLD  35727  pellfundre  35731  pellfundlb  35734  wepwsolem  35902  fnwe2lem2  35911  aomclem8  35921  dfac11  35922  gicabl  35959  islnr3  35976  hbtlem2  35985  hbtlem5  35989  fiinfi  36179  imo72b2lem0  36610  imo72b2lem2  36612  imo72b2lem1  36616  imo72b2  36620  evth2f  37333  ubelsupr  37338  evthf  37345  fnchoice  37347  uzwo4  37387  wessf1ornlem  37469  disjinfi  37478  dstregt0  37522  upbdrech2  37557  mccl  37720  mullimc  37738  ellimcabssub0  37739  limcdm0  37740  climf  37744  mullimcf  37745  constlimc  37746  idlimc  37748  clim2f  37758  limsupre  37763  limsupreOLD  37764  limcleqr  37767  addlimc  37771  0ellimcdiv  37772  clim2cf  37773  clim0cf  37777  cncfshift  37793  cncfperiod  37798  fperdvper  37832  dvdivbd  37837  dvbdfbdioo  37844  ioodvbdlimc1lem2  37846  ioodvbdlimc1lem2OLD  37848  ioodvbdlimc2lem  37850  ioodvbdlimc2lemOLD  37851  dvnprodlem3  37865  stoweidlem5  37922  stoweidlem9  37926  stoweidlem15  37932  stoweidlem16  37933  stoweidlem27  37944  stoweidlem28  37945  stoweidlem31  37949  stoweidlem34  37952  stoweidlem37  37955  stoweidlem46  37964  stoweidlem48  37966  stoweidlem51  37969  stoweidlem52  37970  stoweidlem59  37977  wallispilem3  37986  stirlinglem13  38005  fourierdlem2  38028  fourierdlem3  38029  fourierdlem16  38042  fourierdlem20  38046  fourierdlem21  38047  fourierdlem22  38048  fourierdlem25  38051  fourierdlem39  38066  fourierdlem42  38069  fourierdlem42OLD  38070  fourierdlem54  38081  fourierdlem64  38091  fourierdlem77  38104  fourierdlem83  38110  fourierdlem87  38114  fourierdlem103  38130  fourierdlem104  38131  issal  38232  sge0supre  38290  sge0rnbnd  38294  ismea  38350  iundjiun  38359  caragenval  38378  isome  38379  caragenel  38380  omessle  38383  ovnlerp  38447  hoidmvlelem1  38480  hoidmvlelem3  38482  hoidmvlelem4  38483  hoidmvle  38485  cbvral2  38684  raaan2  38687  2reu4a  38701  dfdfat2  38724  iccpart  38821  iccpartigtl  38828  perfectALTVlem2  38935  bgoldbachlt  38997  tgoldbachlt  39000  issn  39088  fpropnf1  39130  uvtxa01vtx0  39571  uvtxusgr  39577  iscusgredg  39593  rgrx0ndm  39710  ewlksfval  39720  1wlksfval  39726  wlksfval  39727  1wlkvtxedg  39755  1conngr  39987  mgmhmima  40127  rnghmval  40216  lidlmsgrp  40251  lidlrng  40252  zlidlring  40253  uzlidlring  40254  2zrngamnd  40266  ply1mulgsumlem1  40503  ply1mulgsumlem2  40504  linindslinci  40566  lindslinindsimp1  40575  lindslinindsimp2lem5  40580  lindslinindsimp2  40581  linds0  40583  lindsrng01  40586  snlindsntor  40589  lmod1  40610  ldepsnlinc  40626  bigoval  40685  elbigo2r  40689  nn0sumshdiglem2  40758