Theorem ralbidv 3175

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 479	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	ralbidva 3173	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2104  ∀wral 3059

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 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ral 3060

This theorem is referenced by:  2ralbidv  3216  rexralbidv  3218  3ralbidv  3219  4ralbidv  3220  cbvral2vw  3236  cbvral4vw  3239  cbvral2v  3362  rspceaimv  3616  rspc2  3619  rspc2v  3621  rspc3v  3626  rspc4v  3629  reu6i  3723  reu7  3727  sbcralt  3865  reu8nf  3870  raaan  4519  raaanv  4520  raaan2  4523  2reu4lem  4524  reusngf  4675  2ralsng  4679  rexreusng  4682  reuprg0  4705  issn  4832  2ralunsn  4894  elintg  4957  elintrabg  4964  eliin  5001  disjprgw  5142  disjprg  5143  disjxun  5145  brralrspcev  5207  reusv2lem2  5396  reusv3  5402  poeq1  5590  solin  5612  somo  5624  frirr  5652  fr2nr  5653  frminex  5655  wereu2  5672  posn  5760  frsn  5762  ralxpf  5845  cnvpo  6285  reu3op  6290  reuop  6291  dfpo2  6294  frpomin  6340  fnmptfvd  7041  iinpreima  7069  dff4  7101  dff13f  7257  fpropnf1  7268  eusvobj2  7403  ovanraleqv  7435  f1opr  7467  ofreq  7676  sorpssuni  7724  sorpssint  7725  fr3nr  7761  onssmin  7782  funcnvuni  7924  f1oweALT  7961  frxp  8114  frxp2  8132  xpord2indlem  8135  frxp3  8139  xpord3inddlem  8142  poseq  8146  soseq  8147  frecseq123  8269  csbfrecsg  8271  frrlem1  8273  frrlem13  8285  wrecseq123OLD  8302  wfrlem1OLD  8310  wfrlem3OLDa  8313  wfrlem15OLD  8325  smoeq  8352  tfrlem12  8391  tz7.48lem  8443  naddcllem  8677  naddov2  8680  naddunif  8694  naddasslem1  8695  naddasslem2  8696  elixp2  8897  undifixp  8930  xpf1o  9141  nneneq  9211  nneneqOLD  9223  ac6sfi  9289  frfi  9290  fipreima  9360  indexfi  9362  marypha1lem  9430  marypha1  9431  supeq1  9442  supeq3  9446  supmo  9449  eqsup  9453  supub  9456  suplub  9457  sup0  9463  supisoex  9471  eqinf  9481  infval  9483  infmo  9492  oieq1  9509  ordtypecbv  9514  ordtypelem3  9517  ordtypelem6  9520  ordtypelem7  9521  ordtypelem9  9523  wemaplem1  9543  wemaplem2  9544  zfregcl  9591  oemapval  9680  oemapvali  9681  cantnf  9690  wemapwe  9694  ttrcleq  9706  ttrcltr  9713  ttrclss  9717  ttrclselem2  9723  rankval3b  9823  unbndrank  9839  rankunb  9847  rankuni2b  9850  tcrank  9881  scottex  9882  scottexs  9884  scott0s  9885  bnd2  9890  updjud  9931  dfac8clem  10029  ac5num  10033  acni  10042  acni2  10043  alephval3  10107  dfac4  10119  dfac5lem5  10124  dfac5  10125  dfac2a  10126  dfac2b  10127  dfacacn  10138  kmlem2  10148  kmlem13  10159  cflem  10243  cflecard  10250  cfeq0  10253  cfsuc  10254  cfflb  10256  cofsmo  10266  cfsmolem  10267  cfcoflem  10269  coftr  10270  alephsing  10273  fin23lem11  10314  isfin3ds  10326  fin23lem17  10335  fin23lem39  10347  isf33lem  10363  isf34lem6  10377  fin1a2lem13  10409  hsmexlem4  10426  hsmex  10429  axcc2lem  10433  axcc3  10435  dcomex  10444  axdc2lem  10445  axdc3lem2  10448  axdc3lem3  10449  axdc3  10451  axdc4lem  10452  axcclem  10454  zorn2lem2  10494  zorn2lem7  10499  zorn2g  10500  zornn0g  10502  ttukeylem7  10512  axdclem2  10517  brdom3  10525  brdom7disj  10528  brdom6disj  10529  alephval2  10569  inar1  10772  axgroth6  10825  pinq  10924  nqereu  10926  prlem934  11030  supexpr  11051  supsrlem  11108  axpre-sup  11166  dedekind  11381  dedekindle  11382  fiminre2  12166  lbreu  12168  sup2  12174  infm3  12177  nnsub  12260  uzwo  12899  nnwof  12902  ublbneg  12921  lbzbi  12924  zsupss  12925  uzsupss  12928  uzwo3  12931  zmax  12933  rpnnen1lem1  12966  rpnnen1lem3  12967  rpnnen1lem4  12968  rpnnen1lem5  12969  xrsupsslem  13290  xrinfmsslem  13291  xrsupss  13292  xrinfmss  13293  flval2  13783  axdc4uzlem  13952  ssnn0fi  13954  fsuppmapnn0fiubex  13961  faclbnd4lem4  14260  bccl  14286  hashgt12el  14386  hashbc  14416  hashge2el2dif  14445  wrdind  14676  wrd2ind  14677  rexanre  15297  rexico  15304  cau4  15307  reusq0  15413  clim  15442  rlim  15443  rlim2  15444  clim2  15452  clim2c  15453  clim0c  15455  rlim0  15456  rlim0lt  15457  ello12r  15465  ello1d  15471  elo12r  15476  rlimresb  15513  rlimcld2  15526  climabs0  15533  rlimo1  15565  lo1add  15575  lo1mul  15576  isercoll  15618  incexclem  15786  sqrt2irr  16196  gcdcllem1  16444  gcdcllem2  16445  dfgcd2  16492  fissn0dvds  16560  dvdslcmf  16572  lcmfledvds  16573  lcmf  16574  lcmfunsnlem1  16578  lcmfunsnlem2lem1  16579  lcmfunsnlem  16582  lcmfdvds  16583  reumodprminv  16741  pc2dvds  16816  pcz  16818  prmpwdvds  16841  infpn2  16850  prmreclem2  16854  prmreclem3  16855  prmreclem5  16857  prmreclem6  16858  vdwlem6  16923  vdwlem8  16925  vdwlem13  16930  vdwnnlem1  16932  vdwnn  16935  ramcl  16966  cshwrepswhash1  17040  prdsleval  17427  imasval  17461  imasaddfnlem  17478  imasvscafn  17487  mrisval  17578  isacs  17599  isacs2  17601  isacs1i  17605  mreacs  17606  acsfn  17607  acsfn2  17611  iscatd  17621  catidex  17622  catideu  17623  cidval  17625  catidd  17628  comfeq  17654  catpropd  17657  ismon  17684  isfunc  17818  isnat  17902  isinito  17950  istermo  17951  isprs  18254  drsdirfi  18262  ispos  18271  lubfval  18307  lubeldm  18310  lubval  18313  lubprop  18315  lublecllem  18317  glbfval  18320  glbeldm  18323  glbval  18326  glbprop  18328  joinval2lem  18337  joinlem  18340  meetval2lem  18351  meetlem  18354  poslubmo  18368  posglbmo  18369  poslubd  18370  isglbd  18466  lubl  18469  lubun  18472  clatleglb  18475  isdlat  18479  ipodrsima  18498  mgm1  18583  gsumval2  18611  mgmhmima  18640  sgrp1  18654  mhmimalem  18741  mndind  18745  gsumwspan  18763  efmndmnd  18806  smndex1mnd  18827  sgrp2rid2  18843  sgrp2rid2ex  18844  sgrp2nmndlem4  18845  pwmnd  18854  dfgrp2  18883  isgrpinv  18914  grpidinv  18919  dfgrp3lem  18957  issubg4  19061  0subgOLD  19068  isnsg2  19072  nsgacs  19078  elnmz  19079  cycsubgcl  19121  ghmrn  19143  ghmnsgima  19154  isga  19196  orbsta  19218  cntzfval  19225  elcntz  19227  resscntz  19238  oppgsubg  19271  symgextfo  19331  gsmsymgreqlem2  19340  gsmsymgreq  19341  pmtrdifel  19389  pmtrdifwrdellem3  19392  pmtrdifwrdel2  19395  psgnunilem2  19404  psgnunilem3  19405  odeq  19459  gexid  19490  gexlem2  19491  gexdvds  19493  isslw  19517  sylow2alem1  19526  sylow2alem2  19527  efgval  19626  efgrelexlemb  19659  efgcpbllemb  19664  abl1  19775  dmdprd  19909  dprd2da  19953  pgpfac1lem5  19990  ring1  20198  rngisomring  20358  lringuplu  20432  rhmimasubrnglem  20453  isabv  20570  islss  20689  lssacs  20722  reslmhm  20807  islbs  20831  pj1lmhm  20855  lbsacsbs  20914  rnglidlmcl  20982  rnglidl0  21032  isrrg  21104  zringlpir  21238  psgndiflemA  21373  ocvfval  21438  elocv  21440  iunocv  21453  frlmlbs  21571  islindf  21586  islinds2  21587  islindf2  21588  lindfrn  21595  lsslindf  21604  islindf4  21612  opsrval  21820  ply1coe  22040  cply1coe0bi  22044  mat0dimcrng  22192  mdetunilem1  22334  mdetunilem9  22342  cpmat  22431  cpmatel  22433  1elcpmat  22437  m2cpminvid2lem  22476  basgen2  22712  bastop1  22716  isclo  22811  ordtbaslem  22912  iscn  22959  cnpval  22960  iscnp  22961  iscnp3  22968  lmbr  22982  lmbr2  22983  lmbrf  22984  cnprest  23013  cnprest2  23014  t0sep  23048  isreg  23056  t1sep2  23093  tgcmp  23125  1stcclb  23168  1stcfb  23169  2ndc1stc  23175  1stcrest  23177  2ndcdisj  23180  islly  23192  isnlly  23193  lly1stc  23220  isref  23233  islocfin  23241  elkgen  23260  kgencn  23280  elpt  23296  elptr  23297  ptcnplem  23345  tx1stc  23374  cnmpt21  23395  kqt0lem  23460  isr0  23461  regr1lem2  23464  r0sep  23472  nrmr0reg  23473  flffbas  23719  cnflf  23726  cnflf2  23727  lmflf  23729  txflf  23730  fclsopni  23739  fclsnei  23743  fclsrest  23748  fcfnei  23759  cnfcf  23766  alexsubb  23770  alexsubALTlem3  23773  qustgplem  23845  tsmsfbas  23852  tsmsres  23868  tsmsf1o  23869  tsmsxplem1  23877  ustval  23927  isust  23928  ustincl  23932  ustdiag  23933  ustinvel  23934  ustexhalf  23935  ust0  23944  utopval  23957  ucnval  24002  isucn  24003  isucn2  24004  ucnima  24006  iscfilu  24013  ispsmet  24030  ismet  24049  isxmet  24050  imasdsf1olem  24099  imasf1oxmet  24101  imasf1omet  24102  metss  24237  met1stc  24250  prdsxmslem2  24258  txmetcnp  24276  metucn  24300  tngngp3  24393  nlmvscn  24424  nmoval  24452  nmolb  24454  qtopbaslem  24495  cncfval  24628  elcncf2  24630  mulc1cncf  24645  cncfmet  24649  evth  24705  lebnumlem3  24709  lebnum  24710  xlebnum  24711  ishtpy  24718  isphtpy  24727  pi1xfr  24802  pi1coghm  24808  isclmp  24844  ipcn  24994  lmmbr2  25007  lmmbr3  25008  lmmbrf  25010  cfilfval  25012  iscfil  25013  fmcfil  25020  caufval  25023  iscau  25024  iscau2  25025  iscau3  25026  iscau4  25027  iscauf  25028  caucfil  25031  cfilresi  25043  causs  25046  lmclim  25051  cmetcusp1  25101  minveclem4c  25173  minveclem2  25174  minveclem3b  25176  minveclem4  25180  minveclem6  25182  minveclem7  25183  ovolicc2lem3  25268  ismbl  25275  dyadmax  25347  dyadmbllem  25348  dyadmbl  25349  opnmbllem  25350  ismbf1  25373  ismbf  25377  mbfeqalem2  25391  mbflimsup  25415  mbfi1fseqlem6  25470  mbfi1flimlem  25472  itg2seq  25492  itg2monolem1  25500  isibl  25515  ply1divex  25889  fta1g  25920  dgrco  26025  plydivex  26046  fta1  26057  vieta1  26061  aannenlem1  26077  aannenlem2  26078  aalioulem2  26082  aalioulem3  26083  ulmval  26128  ulm2  26133  ulmi  26134  ulmres  26136  ulmshftlem  26137  ulmcaulem  26142  ulmcau  26143  ulmss  26145  ulmbdd  26146  ulmdvlem1  26148  ulmdvlem3  26150  pilem2  26200  pilem3  26201  cxpcn3  26492  dmarea  26698  rlimcnp  26706  scvxcvx  26726  lgamgulmlem2  26770  lgamgulmlem3  26771  lgamgulmlem5  26773  lgambdd  26777  lgamcvglem  26780  isppw2  26855  perfectlem2  26969  2sqlem6  27162  2sqlem10  27167  addsq2reu  27179  2sqreulem1  27185  2sqreunnlem1  27188  dchrisumlema  27227  dchrisumlem2  27229  dchrisumlem3  27230  pntpbnd  27327  pntibndlem3  27331  pntibnd  27332  pntleme  27347  pntlem3  27348  pntlemp  27349  pnt3  27351  sltval  27386  nosupprefixmo  27439  noinfprefixmo  27440  nosupcbv  27441  nosupno  27442  nosupdm  27443  nosupfv  27445  nosupres  27446  nosupbnd1lem1  27447  nosupbnd1lem3  27449  nosupbnd1lem5  27451  noinfcbv  27456  noinfno  27457  noinfdm  27458  noinffv  27460  noinfres  27461  noinfbnd1lem3  27464  noinfbnd1lem5  27466  noetalem1  27480  noetalem2  27481  nocvxminlem  27515  brsslt  27523  conway  27537  etasslt  27551  slerec  27557  madebdaylemlrcut  27630  madebday  27631  cofcutr  27649  lrrecfr  27665  addsprop  27698  negsunif  27768  istrkgld  27977  axtg5seg  27983  tgcgr4  28049  perpln1  28228  perpln2  28229  isperp  28230  brbtwn2  28430  colinearalg  28435  axsegconlem1  28442  axsegcon  28452  ax5seglem4  28457  ax5seglem5  28458  axlowdim  28486  axeuclidlem  28487  axcontlem1  28489  axcontlem2  28490  axcontlem4  28492  axcontlem5  28493  axcontlem8  28496  axcontlem12  28500  elntg2  28510  uvtxusgr  28926  rgrx0ndm  29117  ewlksfval  29125  wksfval  29133  wwlks  29356  wlkiswwlks2  29396  clwwlk  29503  1conngr  29714  frgrwopregasn  29836  frgrwopregbsn  29837  frgrwopreglem5ALT  29842  frgrregord013  29915  isgrpo  30017  isgrpoi  30018  grpoideu  30029  grpoidinv2  30035  vciOLD  30081  isvclem  30097  cnidOLD  30102  isnvlem  30130  nvi  30134  lnoval  30272  islno  30273  isblo3i  30321  blo3i  30322  blocnilem  30324  ajfval  30329  ubthlem1  30390  ubthlem2  30391  ubthlem3  30392  ubth  30393  minvecolem2  30395  minvecolem3  30396  minvecolem4c  30399  minvecolem4  30400  minvecolem5  30401  minvecolem6  30402  minvecolem7  30403  h2hcau  30499  h2hlm  30500  hilid  30681  hcau  30704  hlimi  30708  hlim2  30712  ocel  30801  adjsym  31353  ellnop  31378  ellnfn  31403  hhcno  31424  hhcnf  31425  lnopeq  31529  elunop2  31533  lnophm  31539  lnconi  31553  lnopcnbd  31556  lnfncnbd  31577  imaelshi  31578  riesz3i  31582  riesz4i  31583  riesz4  31584  riesz1  31585  cnlnadjlem2  31588  cnlnadjlem5  31591  cnlnadjlem8  31594  cnlnadji  31596  nmopadjlei  31608  cnvbraval  31630  leopg  31642  leoppos  31646  mdbr  31814  dmdbr  31819  cdj3i  31961  disjunsn  32092  funcnv5mpt  32160  fgreu  32164  fcnvgreu  32165  xrge0infss  32240  wrdt2ind  32384  resspos  32403  mgccole1  32427  mgccole2  32428  mgcmnt1  32429  mgcmnt2  32430  gsumhashmul  32478  isomnd  32489  inftmrel  32596  isinftm  32597  archiabl  32614  isarchiofld  32705  0nellinds  32757  lindssn  32768  elrspunidl  32820  prmidl  32832  ismxidl  32852  crefeq  33123  zarcmplem  33159  esum2d  33389  sigaval  33407  issgon  33419  isrnmeas  33496  ismbfm  33547  mbfmcst  33556  elcarsg  33602  sitgval  33629  eulerpartlemd  33663  ballotleme  33793  tgoldbachgt  33973  bnj1185  34102  bnj1385  34141  bnj66  34169  bnj106  34177  bnj155  34188  bnj852  34230  bnj893  34237  bnj1228  34320  bnj1234  34322  bnj1463  34364  nummin  34392  derangenlem  34460  subfacp1lem3  34471  subfacp1lem5  34473  subfacp1lem6  34474  subfacp1  34475  erdszelem8  34487  kur14  34505  cnpconn  34519  resconn  34535  cvmscbv  34547  iscvm  34548  cvmsi  34554  cvmsval  34555  cvmlift3lem2  34609  snmlval  34620  satfv1  34652  fmlasucdisj  34688  satffunlem1lem1  34691  satffunlem2lem1  34693  satfv1fvfmla1  34712  mclsssvlem  34851  mclsval  34852  mclsax  34858  mclsind  34859  dfon2lem9  35067  dfrdg2  35071  dfrdg3  35072  fwddifnval  35439  nn0prpwlem  35510  isfne  35527  isfne4  35528  isfne2  35530  isfne3  35531  neibastop3  35550  topmeet  35552  topjoin  35553  filnetlem4  35569  unblimceq0lem  35685  unblimceq0  35686  unbdqndv2  35690  taupilemrplb  36504  fin2so  36778  lindsadd  36784  matunitlindflem2  36788  ptrecube  36791  poimirlem2  36793  poimirlem3  36794  poimirlem4  36795  poimirlem24  36815  poimirlem25  36816  poimirlem26  36817  poimirlem27  36818  poimirlem28  36819  poimirlem29  36820  poimirlem30  36821  poimirlem32  36823  poimir  36824  heicant  36826  mblfinlem1  36828  mblfinlem2  36829  voliunnfl  36835  volsupnfl  36836  mbfresfi  36837  itg2addnc  36845  upixp  36900  indexdom  36905  filbcmb  36911  sdclem2  36913  fdc  36916  lmclim2  36929  caures  36931  istotbnd  36940  istotbnd3  36942  sstotbnd  36946  isbnd  36951  heibor  36992  bfp  36995  rrncmslem  37003  isgrpda  37126  idlval  37184  isidl  37185  0idl  37196  unichnidl  37202  pridl  37208  ismaxidl  37211  smprngopr  37223  igenval2  37237  prnc  37238  ispridlc  37241  scottexf  37339  scott0f  37340  disjsuc2  37564  riotasvd  38129  islfl  38233  eqlkr  38272  eqlkr3  38274  glbconN  38550  glbconNOLD  38551  hlsuprexch  38555  ispsubsp  38919  ldilset  39283  isldil  39284  dilsetN  39327  isdilN  39328  trlset  39335  trlval  39336  cdleme27b  39542  cdleme29b  39549  cdleme31so  39553  cdleme31sn1  39555  cdleme31sn1c  39562  cdleme31fv  39564  cdleme40v  39643  istendo  39934  cdlemkid3N  40107  cdlemkid4  40108  cdlemkid5  40109  dihfval  40405  dihval  40406  islpolN  40657  hdmapffval  41000  hdmapfval  41001  hdmapval  41002  hdmapval2lem  41005  hgmapffval  41059  hgmapfval  41060  hgmapval  41061  hgmapvs  41065  sticksstones2  41269  qsalrel  41368  fsuppind  41464  sn-sup2  41644  isnacs  41744  isnacs2  41746  nacsfix  41752  mzpclval  41765  elmzpcl  41766  rencldnfilem  41860  infmrgelbi  41918  pellfundre  41921  pellfundlb  41924  wepwsolem  42086  fnwe2lem2  42095  aomclem8  42105  dfac11  42106  gicabl  42143  islnr3  42159  hbtlem2  42168  hbtlem5  42172  onintunirab  42278  onsucf1lem  42321  cantnfresb  42376  safesnsupfilb  42471  rp-brsslt  42476  fiinfi  42626  clsk1independent  43099  ntrclsk13  43124  gneispacess2  43199  imo72b2lem0  43219  imo72b2lem2  43221  imo72b2lem1  43223  imo72b2  43226  scottelrankd  43308  mnuop23d  43327  ismnushort  43362  evth2f  44001  evthf  44013  fnchoice  44015  uzwo4  44041  wessf1ornlem  44182  disjinfi  44189  rnmptlb  44245  rnmptbdd  44247  rnmptbd2  44251  rnmptbd  44258  dstregt0  44289  upbdrech2  44316  rexabslelem  44426  rexabsle  44427  uzub  44439  infrpgernmpt  44473  mccl  44612  ellimcabssub0  44631  climf  44636  clim2f  44650  limsupre  44655  clim2cf  44664  clim0cf  44668  climf2  44680  clim2f2  44684  clim2d  44687  limsupref  44699  limsupbnd1f  44700  climinf2  44721  limsuppnf  44725  climinfmpt  44729  climinf3  44730  limsupubuzmpt  44733  limsupmnf  44735  limsupre2lem  44738  limsupre2  44739  limsupmnfuzlem  44740  limsupmnfuz  44741  limsupre2mpt  44744  limsupre3lem  44746  limsupre3  44747  limsupre3mpt  44748  limsupre3uz  44750  limsupreuz  44751  limsupreuzmpt  44753  climuz  44758  liminfreuzlem  44816  liminfreuz  44817  cnrefiisplem  44843  xlimmnfvlem1  44846  xlimmnfv  44848  xlimpnfvlem1  44850  xlimpnfv  44852  xlimmnfmpt  44857  xlimpnfmpt  44858  cncfshift  44888  cncfperiod  44893  fperdvper  44933  dvbdfbdioo  44944  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  dvnprodlem3  44962  stoweidlem5  45019  stoweidlem9  45023  stoweidlem15  45029  stoweidlem16  45030  stoweidlem27  45041  stoweidlem28  45042  stoweidlem31  45045  stoweidlem34  45048  stoweidlem37  45051  stoweidlem46  45060  stoweidlem48  45062  stoweidlem51  45065  stoweidlem52  45066  stoweidlem59  45073  wallispilem3  45081  stirlinglem13  45100  fourierdlem2  45123  fourierdlem3  45124  fourierdlem16  45137  fourierdlem20  45141  fourierdlem21  45142  fourierdlem22  45143  fourierdlem25  45146  fourierdlem39  45160  fourierdlem42  45163  fourierdlem54  45174  fourierdlem64  45184  fourierdlem77  45197  fourierdlem83  45203  fourierdlem103  45223  fourierdlem104  45224  subsaliuncllem  45371  iundjiun  45474  meaiunincf  45497  caragenval  45507  isome  45508  caragenel  45509  omessle  45512  ovnlerp  45576  hoidmvlelem3  45611  hoidmvle  45614  issmflem  45741  issmfgt  45770  smfmullem2  45806  smfmullem4  45808  smfmul  45809  smfsuplem2  45826  smfsup  45828  smfinflem  45831  smfinf  45832  fsupdm  45856  finfdm  45860  cfsetsnfsetf  46066  cbvral2  46109  2reu8i  46119  2reuimp0  46120  dfdfat2  46134  iccpart  46382  iccpartigtl  46389  paireqne  46477  reupr  46488  perfectALTVlem2  46688  bgoldbachlt  46779  tgoldbachlt  46782  isomgreqve  46791  isomushgr  46792  isomuspgrlem2  46799  isomgrsym  46802  isomgrtr  46805  ushrisomgr  46807  upwlksfval  46811  nn0mnd  46855  uzlidlring  46915  ply1mulgsumlem1  47154  ply1mulgsumlem2  47155  linindslinci  47216  lindslinindsimp1  47225  lindslinindsimp2lem5  47230  lindslinindsimp2  47231  linds0  47233  lindsrng01  47236  snlindsntor  47239  lmod1  47260  ldepsnlinc  47276  bigoval  47322  elbigo2r  47326  nn0sumshdiglem2  47395  eenglngeehlnmlem1  47510  eenglngeehlnmlem2  47511  lubeldm2d  47678  glbeldm2d  47679  lubsscl  47680  glbsscl  47681  ipolubdm  47699  ipolub  47700  ipoglbdm  47702  ipoglb  47703  isthincd2lem2  47743  setrec1lem2  47820