Theorem ralbidv 3172

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2099  ∀wral 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3057

This theorem is referenced by:  2ralbidv  3213  rexralbidv  3215  3ralbidv  3216  4ralbidv  3217  cbvral2vw  3233  cbvral4vw  3236  cbvral2v  3359  rspceaimv  3613  rspc2  3616  rspc2v  3618  rspc3v  3623  rspc4v  3626  reu6i  3721  reu7  3725  sbcralt  3862  reu8nf  3867  raaan  4516  raaanv  4517  raaan2  4520  2reu4lem  4521  reusngf  4672  2ralsng  4676  rexreusng  4679  reuprg0  4702  issn  4829  2ralunsn  4891  elintg  4952  elintrabg  4959  eliin  4996  disjprgw  5137  disjprg  5138  disjxun  5140  brralrspcev  5202  reusv2lem2  5393  reusv3  5399  poeq1  5587  solin  5609  somo  5621  frirr  5649  fr2nr  5650  frminex  5652  wereu2  5669  posn  5757  frsn  5759  ralxpf  5843  cnvpo  6285  reu3op  6290  reuop  6291  dfpo2  6294  frpomin  6340  fnmptfvd  7044  iinpreima  7072  dff4  7105  dff13f  7260  fpropnf1  7271  eusvobj2  7406  ovanraleqv  7438  f1opr  7470  ofreq  7683  sorpssuni  7731  sorpssint  7732  fr3nr  7768  onssmin  7789  funcnvuni  7933  f1oweALT  7970  frxp  8125  frxp2  8143  xpord2indlem  8146  frxp3  8150  xpord3inddlem  8153  poseq  8157  soseq  8158  frecseq123  8281  csbfrecsg  8283  frrlem1  8285  frrlem13  8297  wrecseq123OLD  8314  wfrlem1OLD  8322  wfrlem3OLDa  8325  wfrlem15OLD  8337  smoeq  8364  tfrlem12  8403  tz7.48lem  8455  naddcllem  8690  naddov2  8693  naddunif  8707  naddasslem1  8708  naddasslem2  8709  elixp2  8911  undifixp  8944  xpf1o  9155  nneneq  9225  nneneqOLD  9237  ac6sfi  9303  frfi  9304  fipreima  9374  indexfi  9376  marypha1lem  9448  marypha1  9449  supeq1  9460  supeq3  9464  supmo  9467  eqsup  9471  supub  9474  suplub  9475  sup0  9481  supisoex  9489  eqinf  9499  infval  9501  infmo  9510  oieq1  9527  ordtypecbv  9532  ordtypelem3  9535  ordtypelem6  9538  ordtypelem7  9539  ordtypelem9  9541  wemaplem1  9561  wemaplem2  9562  zfregcl  9609  oemapval  9698  oemapvali  9699  cantnf  9708  wemapwe  9712  ttrcleq  9724  ttrcltr  9731  ttrclss  9735  ttrclselem2  9741  rankval3b  9841  unbndrank  9857  rankunb  9865  rankuni2b  9868  tcrank  9899  scottex  9900  scottexs  9902  scott0s  9903  bnd2  9908  updjud  9949  dfac8clem  10047  ac5num  10051  acni  10060  acni2  10061  alephval3  10125  dfac4  10137  dfac5lem5  10142  dfac5  10143  dfac2a  10144  dfac2b  10145  dfacacn  10156  kmlem2  10166  kmlem13  10177  cflem  10261  cflecard  10268  cfeq0  10271  cfsuc  10272  cfflb  10274  cofsmo  10284  cfsmolem  10285  cfcoflem  10287  coftr  10288  alephsing  10291  fin23lem11  10332  isfin3ds  10344  fin23lem17  10353  fin23lem39  10365  isf33lem  10381  isf34lem6  10395  fin1a2lem13  10427  hsmexlem4  10444  hsmex  10447  axcc2lem  10451  axcc3  10453  dcomex  10462  axdc2lem  10463  axdc3lem2  10466  axdc3lem3  10467  axdc3  10469  axdc4lem  10470  axcclem  10472  zorn2lem2  10512  zorn2lem7  10517  zorn2g  10518  zornn0g  10520  ttukeylem7  10530  axdclem2  10535  brdom3  10543  brdom7disj  10546  brdom6disj  10547  alephval2  10587  inar1  10790  axgroth6  10843  pinq  10942  nqereu  10944  prlem934  11048  supexpr  11069  supsrlem  11126  axpre-sup  11184  dedekind  11399  dedekindle  11400  fiminre2  12184  lbreu  12186  sup2  12192  infm3  12195  nnsub  12278  uzwo  12917  nnwof  12920  ublbneg  12939  lbzbi  12942  zsupss  12943  uzsupss  12946  uzwo3  12949  zmax  12951  rpnnen1lem1  12984  rpnnen1lem3  12985  rpnnen1lem4  12986  rpnnen1lem5  12987  xrsupsslem  13310  xrinfmsslem  13311  xrsupss  13312  xrinfmss  13313  flval2  13803  axdc4uzlem  13972  ssnn0fi  13974  fsuppmapnn0fiubex  13981  faclbnd4lem4  14279  bccl  14305  hashgt12el  14405  hashbc  14436  hashge2el2dif  14465  wrdind  14696  wrd2ind  14697  rexanre  15317  rexico  15324  cau4  15327  reusq0  15433  clim  15462  rlim  15463  rlim2  15464  clim2  15472  clim2c  15473  clim0c  15475  rlim0  15476  rlim0lt  15477  ello12r  15485  ello1d  15491  elo12r  15496  rlimresb  15533  rlimcld2  15546  climabs0  15553  rlimo1  15585  lo1add  15595  lo1mul  15596  isercoll  15638  incexclem  15806  sqrt2irr  16217  gcdcllem1  16465  gcdcllem2  16466  dfgcd2  16513  fissn0dvds  16581  dvdslcmf  16593  lcmfledvds  16594  lcmf  16595  lcmfunsnlem1  16599  lcmfunsnlem2lem1  16600  lcmfunsnlem  16603  lcmfdvds  16604  reumodprminv  16764  pc2dvds  16839  pcz  16841  prmpwdvds  16864  infpn2  16873  prmreclem2  16877  prmreclem3  16878  prmreclem5  16880  prmreclem6  16881  vdwlem6  16946  vdwlem8  16948  vdwlem13  16953  vdwnnlem1  16955  vdwnn  16958  ramcl  16989  cshwrepswhash1  17063  prdsleval  17450  imasval  17484  imasaddfnlem  17501  imasvscafn  17510  mrisval  17601  isacs  17622  isacs2  17624  isacs1i  17628  mreacs  17629  acsfn  17630  acsfn2  17634  iscatd  17644  catidex  17645  catideu  17646  cidval  17648  catidd  17651  comfeq  17677  catpropd  17680  ismon  17707  isfunc  17841  isnat  17928  isinito  17976  istermo  17977  isprs  18280  drsdirfi  18288  ispos  18297  lubfval  18333  lubeldm  18336  lubval  18339  lubprop  18341  lublecllem  18343  glbfval  18346  glbeldm  18349  glbval  18352  glbprop  18354  joinval2lem  18363  joinlem  18366  meetval2lem  18377  meetlem  18380  poslubmo  18394  posglbmo  18395  poslubd  18396  isglbd  18492  lubl  18495  lubun  18498  clatleglb  18501  isdlat  18505  ipodrsima  18524  mgm1  18609  gsumval2  18637  mgmhmima  18666  sgrp1  18680  mhmimalem  18767  mndind  18771  gsumwspan  18789  efmndmnd  18832  smndex1mnd  18853  sgrp2rid2  18869  sgrp2rid2ex  18870  sgrp2nmndlem4  18871  pwmnd  18880  dfgrp2  18910  isgrpinv  18941  grpidinv  18946  dfgrp3lem  18985  issubg4  19091  0subgOLD  19098  isnsg2  19102  nsgacs  19108  elnmz  19109  cycsubgcl  19152  ghmrn  19174  ghmnsgima  19185  isga  19233  orbsta  19255  cntzfval  19262  elcntz  19264  resscntz  19275  oppgsubg  19308  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  ring1  20235  rngisomring  20395  lringuplu  20470  rhmimasubrnglem  20491  isabv  20688  islss  20807  lssacs  20840  reslmhm  20926  islbs  20950  pj1lmhm  20974  lbsacsbs  21033  rnglidlmcl  21101  rnglidl0  21114  isrrg  21224  zringlpir  21380  psgndiflemA  21520  ocvfval  21585  elocv  21587  iunocv  21600  frlmlbs  21718  islindf  21733  islinds2  21734  islindf2  21735  lindfrn  21742  lsslindf  21751  islindf4  21759  opsrval  21971  ply1coe  22204  cply1coe0bi  22208  mat0dimcrng  22359  mdetunilem1  22501  mdetunilem9  22509  cpmat  22598  cpmatel  22600  1elcpmat  22604  m2cpminvid2lem  22643  basgen2  22879  bastop1  22883  isclo  22978  ordtbaslem  23079  iscn  23126  cnpval  23127  iscnp  23128  iscnp3  23135  lmbr  23149  lmbr2  23150  lmbrf  23151  cnprest  23180  cnprest2  23181  t0sep  23215  isreg  23223  t1sep2  23260  tgcmp  23292  1stcclb  23335  1stcfb  23336  2ndc1stc  23342  1stcrest  23344  2ndcdisj  23347  islly  23359  isnlly  23360  lly1stc  23387  isref  23400  islocfin  23408  elkgen  23427  kgencn  23447  elpt  23463  elptr  23464  ptcnplem  23512  tx1stc  23541  cnmpt21  23562  kqt0lem  23627  isr0  23628  regr1lem2  23631  r0sep  23639  nrmr0reg  23640  flffbas  23886  cnflf  23893  cnflf2  23894  lmflf  23896  txflf  23897  fclsopni  23906  fclsnei  23910  fclsrest  23915  fcfnei  23926  cnfcf  23933  alexsubb  23937  alexsubALTlem3  23940  qustgplem  24012  tsmsfbas  24019  tsmsres  24035  tsmsf1o  24036  tsmsxplem1  24044  ustval  24094  isust  24095  ustincl  24099  ustdiag  24100  ustinvel  24101  ustexhalf  24102  ust0  24111  utopval  24124  ucnval  24169  isucn  24170  isucn2  24171  ucnima  24173  iscfilu  24180  ispsmet  24197  ismet  24216  isxmet  24217  imasdsf1olem  24266  imasf1oxmet  24268  imasf1omet  24269  metss  24404  met1stc  24417  prdsxmslem2  24425  txmetcnp  24443  metucn  24467  tngngp3  24560  nlmvscn  24591  nmoval  24619  nmolb  24621  qtopbaslem  24662  cncfval  24795  elcncf2  24797  mulc1cncf  24812  cncfmet  24816  evth  24872  lebnumlem3  24876  lebnum  24877  xlebnum  24878  ishtpy  24885  isphtpy  24894  pi1xfr  24969  pi1coghm  24975  isclmp  25011  ipcn  25161  lmmbr2  25174  lmmbr3  25175  lmmbrf  25177  cfilfval  25179  iscfil  25180  fmcfil  25187  caufval  25190  iscau  25191  iscau2  25192  iscau3  25193  iscau4  25194  iscauf  25195  caucfil  25198  cfilresi  25210  causs  25213  lmclim  25218  cmetcusp1  25268  minveclem4c  25340  minveclem2  25341  minveclem3b  25343  minveclem4  25347  minveclem6  25349  minveclem7  25350  ovolicc2lem3  25435  ismbl  25442  dyadmax  25514  dyadmbllem  25515  dyadmbl  25516  opnmbllem  25517  ismbf1  25540  ismbf  25544  mbfeqalem2  25558  mbflimsup  25582  mbfi1fseqlem6  25637  mbfi1flimlem  25639  itg2seq  25659  itg2monolem1  25667  isibl  25682  ply1divex  26059  fta1g  26091  dgrco  26197  plydivex  26219  fta1  26230  vieta1  26234  aannenlem1  26250  aannenlem2  26251  aalioulem2  26255  aalioulem3  26256  ulmval  26303  ulm2  26308  ulmi  26309  ulmres  26311  ulmshftlem  26312  ulmcaulem  26317  ulmcau  26318  ulmss  26320  ulmbdd  26321  ulmdvlem1  26323  ulmdvlem3  26325  pilem2  26376  pilem3  26377  cxpcn3  26670  dmarea  26876  rlimcnp  26884  scvxcvx  26905  lgamgulmlem2  26949  lgamgulmlem3  26950  lgamgulmlem5  26952  lgambdd  26956  lgamcvglem  26959  isppw2  27034  perfectlem2  27150  2sqlem6  27343  2sqlem10  27348  addsq2reu  27360  2sqreulem1  27366  2sqreunnlem1  27369  dchrisumlema  27408  dchrisumlem2  27410  dchrisumlem3  27411  pntpbnd  27508  pntibndlem3  27512  pntibnd  27513  pntleme  27528  pntlem3  27529  pntlemp  27530  pnt3  27532  sltval  27567  nosupprefixmo  27620  noinfprefixmo  27621  nosupcbv  27622  nosupno  27623  nosupdm  27624  nosupfv  27626  nosupres  27627  nosupbnd1lem1  27628  nosupbnd1lem3  27630  nosupbnd1lem5  27632  noinfcbv  27637  noinfno  27638  noinfdm  27639  noinffv  27641  noinfres  27642  noinfbnd1lem3  27645  noinfbnd1lem5  27647  noetalem1  27661  noetalem2  27662  nocvxminlem  27697  brsslt  27705  conway  27719  etasslt  27733  slerec  27739  madebdaylemlrcut  27812  madebday  27813  cofcutr  27831  lrrecfr  27847  addsprop  27880  negsunif  27954  istrkgld  28250  axtg5seg  28256  tgcgr4  28322  perpln1  28501  perpln2  28502  isperp  28503  brbtwn2  28703  colinearalg  28708  axsegconlem1  28715  axsegcon  28725  ax5seglem4  28730  ax5seglem5  28731  axlowdim  28759  axeuclidlem  28760  axcontlem1  28762  axcontlem2  28763  axcontlem4  28765  axcontlem5  28766  axcontlem8  28769  axcontlem12  28773  elntg2  28783  uvtxusgr  29202  rgrx0ndm  29394  ewlksfval  29402  wksfval  29410  wwlks  29633  wlkiswwlks2  29673  clwwlk  29780  1conngr  29991  frgrwopregasn  30113  frgrwopregbsn  30114  frgrwopreglem5ALT  30119  frgrregord013  30192  isgrpo  30294  isgrpoi  30295  grpoideu  30306  grpoidinv2  30312  vciOLD  30358  isvclem  30374  cnidOLD  30379  isnvlem  30407  nvi  30411  lnoval  30549  islno  30550  isblo3i  30598  blo3i  30599  blocnilem  30601  ajfval  30606  ubthlem1  30667  ubthlem2  30668  ubthlem3  30669  ubth  30670  minvecolem2  30672  minvecolem3  30673  minvecolem4c  30676  minvecolem4  30677  minvecolem5  30678  minvecolem6  30679  minvecolem7  30680  h2hcau  30776  h2hlm  30777  hilid  30958  hcau  30981  hlimi  30985  hlim2  30989  ocel  31078  adjsym  31630  ellnop  31655  ellnfn  31680  hhcno  31701  hhcnf  31702  lnopeq  31806  elunop2  31810  lnophm  31816  lnconi  31830  lnopcnbd  31833  lnfncnbd  31854  imaelshi  31855  riesz3i  31859  riesz4i  31860  riesz4  31861  riesz1  31862  cnlnadjlem2  31865  cnlnadjlem5  31868  cnlnadjlem8  31871  cnlnadji  31873  nmopadjlei  31885  cnvbraval  31907  leopg  31919  leoppos  31923  mdbr  32091  dmdbr  32096  cdj3i  32238  disjunsn  32369  funcnv5mpt  32437  fgreu  32441  fcnvgreu  32442  xrge0infss  32514  wrdt2ind  32656  resspos  32675  mgccole1  32699  mgccole2  32700  mgcmnt1  32701  mgcmnt2  32702  gsumhashmul  32748  isomnd  32759  inftmrel  32866  isinftm  32867  archiabl  32884  isarchiofld  32972  0nellinds  33022  lindssn  33033  elrspunidl  33079  prmidl  33091  ismxidl  33111  crefeq  33382  zarcmplem  33418  esum2d  33648  sigaval  33666  issgon  33678  isrnmeas  33755  ismbfm  33806  mbfmcst  33815  elcarsg  33861  sitgval  33888  eulerpartlemd  33922  ballotleme  34052  tgoldbachgt  34231  bnj1185  34360  bnj1385  34399  bnj66  34427  bnj106  34435  bnj155  34446  bnj852  34488  bnj893  34495  bnj1228  34578  bnj1234  34580  bnj1463  34622  nummin  34650  derangenlem  34717  subfacp1lem3  34728  subfacp1lem5  34730  subfacp1lem6  34731  subfacp1  34732  erdszelem8  34744  kur14  34762  cnpconn  34776  resconn  34792  cvmscbv  34804  iscvm  34805  cvmsi  34811  cvmsval  34812  cvmlift3lem2  34866  snmlval  34877  satfv1  34909  fmlasucdisj  34945  satffunlem1lem1  34948  satffunlem2lem1  34950  satfv1fvfmla1  34969  mclsssvlem  35108  mclsval  35109  mclsax  35115  mclsind  35116  dfon2lem9  35323  dfrdg2  35327  dfrdg3  35328  fwddifnval  35695  nn0prpwlem  35742  isfne  35759  isfne4  35760  isfne2  35762  isfne3  35763  neibastop3  35782  topmeet  35784  topjoin  35785  filnetlem4  35801  unblimceq0lem  35917  unblimceq0  35918  unbdqndv2  35922  taupilemrplb  36735  fin2so  37015  lindsadd  37021  matunitlindflem2  37025  ptrecube  37028  poimirlem2  37030  poimirlem3  37031  poimirlem4  37032  poimirlem24  37052  poimirlem25  37053  poimirlem26  37054  poimirlem27  37055  poimirlem28  37056  poimirlem29  37057  poimirlem30  37058  poimirlem32  37060  poimir  37061  heicant  37063  mblfinlem1  37065  mblfinlem2  37066  voliunnfl  37072  volsupnfl  37073  mbfresfi  37074  itg2addnc  37082  upixp  37137  indexdom  37142  filbcmb  37148  sdclem2  37150  fdc  37153  lmclim2  37166  caures  37168  istotbnd  37177  istotbnd3  37179  sstotbnd  37183  isbnd  37188  heibor  37229  bfp  37232  rrncmslem  37240  isgrpda  37363  idlval  37421  isidl  37422  0idl  37433  unichnidl  37439  pridl  37445  ismaxidl  37448  smprngopr  37460  igenval2  37474  prnc  37475  ispridlc  37478  scottexf  37576  scott0f  37577  disjsuc2  37800  riotasvd  38365  islfl  38469  eqlkr  38508  eqlkr3  38510  glbconN  38786  glbconNOLD  38787  hlsuprexch  38791  ispsubsp  39155  ldilset  39519  isldil  39520  dilsetN  39563  isdilN  39564  trlset  39571  trlval  39572  cdleme27b  39778  cdleme29b  39785  cdleme31so  39789  cdleme31sn1  39791  cdleme31sn1c  39798  cdleme31fv  39800  cdleme40v  39879  istendo  40170  cdlemkid3N  40343  cdlemkid4  40344  cdlemkid5  40345  dihfval  40641  dihval  40642  islpolN  40893  hdmapffval  41236  hdmapfval  41237  hdmapval  41238  hdmapval2lem  41241  hgmapffval  41295  hgmapfval  41296  hgmapval  41297  hgmapvs  41301  isprimroot  41501  aks6d1c1p1  41511  hashscontpow1  41525  sticksstones2  41551  qsalrel  41651  fsuppind  41745  sn-sup2  41946  isnacs  42046  isnacs2  42048  nacsfix  42054  mzpclval  42067  elmzpcl  42068  rencldnfilem  42162  infmrgelbi  42220  pellfundre  42223  pellfundlb  42226  wepwsolem  42388  fnwe2lem2  42397  aomclem8  42407  dfac11  42408  gicabl  42445  islnr3  42461  hbtlem2  42470  hbtlem5  42474  onintunirab  42578  onsucf1lem  42621  cantnfresb  42676  safesnsupfilb  42771  rp-brsslt  42776  fiinfi  42926  clsk1independent  43399  ntrclsk13  43424  gneispacess2  43499  imo72b2lem0  43518  imo72b2lem2  43520  imo72b2lem1  43522  imo72b2  43525  scottelrankd  43607  mnuop23d  43626  ismnushort  43661  evth2f  44300  evthf  44312  fnchoice  44314  uzwo4  44340  wessf1ornlem  44481  disjinfi  44488  rnmptlb  44542  rnmptbdd  44544  rnmptbd2  44548  rnmptbd  44555  dstregt0  44586  upbdrech2  44613  rexabslelem  44723  rexabsle  44724  uzub  44736  infrpgernmpt  44770  mccl  44909  ellimcabssub0  44928  climf  44933  clim2f  44947  limsupre  44952  clim2cf  44961  clim0cf  44965  climf2  44977  clim2f2  44981  clim2d  44984  limsupref  44996  limsupbnd1f  44997  climinf2  45018  limsuppnf  45022  climinfmpt  45026  climinf3  45027  limsupubuzmpt  45030  limsupmnf  45032  limsupre2lem  45035  limsupre2  45036  limsupmnfuzlem  45037  limsupmnfuz  45038  limsupre2mpt  45041  limsupre3lem  45043  limsupre3  45044  limsupre3mpt  45045  limsupre3uz  45047  limsupreuz  45048  limsupreuzmpt  45050  climuz  45055  liminfreuzlem  45113  liminfreuz  45114  cnrefiisplem  45140  xlimmnfvlem1  45143  xlimmnfv  45145  xlimpnfvlem1  45147  xlimpnfv  45149  xlimmnfmpt  45154  xlimpnfmpt  45155  cncfshift  45185  cncfperiod  45190  fperdvper  45230  dvbdfbdioo  45241  ioodvbdlimc1lem2  45243  ioodvbdlimc2lem  45245  dvnprodlem3  45259  stoweidlem5  45316  stoweidlem9  45320  stoweidlem15  45326  stoweidlem16  45327  stoweidlem27  45338  stoweidlem28  45339  stoweidlem31  45342  stoweidlem34  45345  stoweidlem37  45348  stoweidlem46  45357  stoweidlem48  45359  stoweidlem51  45362  stoweidlem52  45363  stoweidlem59  45370  wallispilem3  45378  stirlinglem13  45397  fourierdlem2  45420  fourierdlem3  45421  fourierdlem16  45434  fourierdlem20  45438  fourierdlem21  45439  fourierdlem22  45440  fourierdlem25  45443  fourierdlem39  45457  fourierdlem42  45460  fourierdlem54  45471  fourierdlem64  45481  fourierdlem77  45494  fourierdlem83  45500  fourierdlem103  45520  fourierdlem104  45521  subsaliuncllem  45668  iundjiun  45771  meaiunincf  45794  caragenval  45804  isome  45805  caragenel  45806  omessle  45809  ovnlerp  45873  hoidmvlelem3  45908  hoidmvle  45911  issmflem  46038  issmfgt  46067  smfmullem2  46103  smfmullem4  46105  smfmul  46106  smfsuplem2  46123  smfsup  46125  smfinflem  46128  smfinf  46129  fsupdm  46153  finfdm  46157  cfsetsnfsetf  46363  cbvral2  46406  2reu8i  46416  2reuimp0  46417  dfdfat2  46431  iccpart  46679  iccpartigtl  46686  paireqne  46774  reupr  46785  perfectALTVlem2  46985  bgoldbachlt  47076  tgoldbachlt  47079  isuspgrim0  47093  grimidvtxedg  47097  grimcnv  47100  grimco  47101  gricushgr  47106  ushggricedg  47116  upwlksfval  47120  nn0mnd  47164  uzlidlring  47220  ply1mulgsumlem1  47377  ply1mulgsumlem2  47378  linindslinci  47439  lindslinindsimp1  47448  lindslinindsimp2lem5  47453  lindslinindsimp2  47454  linds0  47456  lindsrng01  47459  snlindsntor  47462  lmod1  47483  ldepsnlinc  47499  bigoval  47545  elbigo2r  47549  nn0sumshdiglem2  47618  eenglngeehlnmlem1  47733  eenglngeehlnmlem2  47734  lubeldm2d  47900  glbeldm2d  47901  lubsscl  47902  glbsscl  47903  ipolubdm  47921  ipolub  47922  ipoglbdm  47924  ipoglb  47925  isthincd2lem2  47965  setrec1lem2  48042