Theorem ralbidv 3176

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2106  ∀wral 3060

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3061

This theorem is referenced by:  2ralbidv  3217  rexralbidv  3219  3ralbidv  3220  4ralbidv  3221  cbvral2vw  3237  cbvral4vw  3240  cbvral2v  3363  rspceaimv  3613  rspc2  3616  rspc2v  3618  rspc3v  3623  rspc4v  3626  reu6i  3720  reu7  3724  sbcralt  3862  reu8nf  3867  raaan  4514  raaanv  4515  raaan2  4518  2reu4lem  4519  reusngf  4669  2ralsng  4673  rexreusng  4676  reuprg0  4699  issn  4826  2ralunsn  4888  elintg  4951  elintrabg  4958  eliin  4995  disjprgw  5136  disjprg  5137  disjxun  5139  brralrspcev  5201  reusv2lem2  5390  reusv3  5396  poeq1  5584  solin  5606  somo  5618  frirr  5646  fr2nr  5647  frminex  5649  wereu2  5666  posn  5753  frsn  5755  ralxpf  5838  cnvpo  6275  reu3op  6280  reuop  6281  dfpo2  6284  frpomin  6330  fnmptfvd  7027  iinpreima  7055  dff4  7087  dff13f  7239  fpropnf1  7250  eusvobj2  7385  ovanraleqv  7417  f1opr  7449  ofreq  7657  sorpssuni  7705  sorpssint  7706  fr3nr  7742  onssmin  7763  funcnvuni  7904  f1oweALT  7941  frxp  8094  frxp2  8112  xpord2indlem  8115  frxp3  8119  xpord3inddlem  8122  poseq  8126  soseq  8127  frecseq123  8249  csbfrecsg  8251  frrlem1  8253  frrlem13  8265  wrecseq123OLD  8282  wfrlem1OLD  8290  wfrlem3OLDa  8293  wfrlem15OLD  8305  smoeq  8332  tfrlem12  8371  tz7.48lem  8423  naddcllem  8658  naddov2  8661  naddunif  8675  naddasslem1  8676  naddasslem2  8677  elixp2  8878  undifixp  8911  xpf1o  9122  nneneq  9192  nneneqOLD  9204  ac6sfi  9270  frfi  9271  fipreima  9341  indexfi  9343  marypha1lem  9410  marypha1  9411  supeq1  9422  supeq3  9426  supmo  9429  eqsup  9433  supub  9436  suplub  9437  sup0  9443  supisoex  9451  eqinf  9461  infval  9463  infmo  9472  oieq1  9489  ordtypecbv  9494  ordtypelem3  9497  ordtypelem6  9500  ordtypelem7  9501  ordtypelem9  9503  wemaplem1  9523  wemaplem2  9524  zfregcl  9571  oemapval  9660  oemapvali  9661  cantnf  9670  wemapwe  9674  ttrcleq  9686  ttrcltr  9693  ttrclss  9697  ttrclselem2  9703  rankval3b  9803  unbndrank  9819  rankunb  9827  rankuni2b  9830  tcrank  9861  scottex  9862  scottexs  9864  scott0s  9865  bnd2  9870  updjud  9911  dfac8clem  10009  ac5num  10013  acni  10022  acni2  10023  alephval3  10087  dfac4  10099  dfac5lem5  10104  dfac5  10105  dfac2a  10106  dfac2b  10107  dfacacn  10118  kmlem2  10128  kmlem13  10139  cflem  10223  cflecard  10230  cfeq0  10233  cfsuc  10234  cfflb  10236  cofsmo  10246  cfsmolem  10247  cfcoflem  10249  coftr  10250  alephsing  10253  fin23lem11  10294  isfin3ds  10306  fin23lem17  10315  fin23lem39  10327  isf33lem  10343  isf34lem6  10357  fin1a2lem13  10389  hsmexlem4  10406  hsmex  10409  axcc2lem  10413  axcc3  10415  dcomex  10424  axdc2lem  10425  axdc3lem2  10428  axdc3lem3  10429  axdc3  10431  axdc4lem  10432  axcclem  10434  zorn2lem2  10474  zorn2lem7  10479  zorn2g  10480  zornn0g  10482  ttukeylem7  10492  axdclem2  10497  brdom3  10505  brdom7disj  10508  brdom6disj  10509  alephval2  10549  inar1  10752  axgroth6  10805  pinq  10904  nqereu  10906  prlem934  11010  supexpr  11031  supsrlem  11088  axpre-sup  11146  dedekind  11359  dedekindle  11360  fiminre2  12144  lbreu  12146  sup2  12152  infm3  12155  nnsub  12238  uzwo  12877  nnwof  12880  ublbneg  12899  lbzbi  12902  zsupss  12903  uzsupss  12906  uzwo3  12909  zmax  12911  rpnnen1lem1  12944  rpnnen1lem3  12945  rpnnen1lem4  12946  rpnnen1lem5  12947  xrsupsslem  13268  xrinfmsslem  13269  xrsupss  13270  xrinfmss  13271  flval2  13761  axdc4uzlem  13930  ssnn0fi  13932  fsuppmapnn0fiubex  13939  faclbnd4lem4  14238  bccl  14264  hashgt12el  14364  hashbc  14394  hashge2el2dif  14423  wrdind  14654  wrd2ind  14655  rexanre  15275  rexico  15282  cau4  15285  reusq0  15391  clim  15420  rlim  15421  rlim2  15422  clim2  15430  clim2c  15431  clim0c  15433  rlim0  15434  rlim0lt  15435  ello12r  15443  ello1d  15449  elo12r  15454  rlimresb  15491  rlimcld2  15504  climabs0  15511  rlimo1  15543  lo1add  15553  lo1mul  15554  isercoll  15596  incexclem  15764  sqrt2irr  16174  gcdcllem1  16422  gcdcllem2  16423  dfgcd2  16470  fissn0dvds  16538  dvdslcmf  16550  lcmfledvds  16551  lcmf  16552  lcmfunsnlem1  16556  lcmfunsnlem2lem1  16557  lcmfunsnlem  16560  lcmfdvds  16561  reumodprminv  16719  pc2dvds  16794  pcz  16796  prmpwdvds  16819  infpn2  16828  prmreclem2  16832  prmreclem3  16833  prmreclem5  16835  prmreclem6  16836  vdwlem6  16901  vdwlem8  16903  vdwlem13  16908  vdwnnlem1  16910  vdwnn  16913  ramcl  16944  cshwrepswhash1  17018  prdsleval  17405  imasval  17439  imasaddfnlem  17456  imasvscafn  17465  mrisval  17556  isacs  17577  isacs2  17579  isacs1i  17583  mreacs  17584  acsfn  17585  acsfn2  17589  iscatd  17599  catidex  17600  catideu  17601  cidval  17603  catidd  17606  comfeq  17632  catpropd  17635  ismon  17662  isfunc  17796  isnat  17880  isinito  17928  istermo  17929  isprs  18232  drsdirfi  18240  ispos  18249  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  isglbd  18444  lubl  18447  lubun  18450  clatleglb  18453  isdlat  18457  ipodrsima  18476  mgm1  18559  gsumval2  18587  sgrp1  18601  mhmima  18681  mndind  18684  gsumwspan  18702  efmndmnd  18745  smndex1mnd  18766  sgrp2rid2  18782  sgrp2rid2ex  18783  sgrp2nmndlem4  18784  pwmnd  18793  dfgrp2  18822  isgrpinv  18853  grpidinv  18857  dfgrp3lem  18895  issubg4  18997  0subgOLD  19004  isnsg2  19008  nsgacs  19014  elnmz  19015  cycsubgcl  19049  ghmrn  19071  ghmnsgima  19082  isga  19121  orbsta  19143  cntzfval  19150  elcntz  19152  resscntz  19162  oppgsubg  19194  symgextfo  19254  gsmsymgreqlem2  19263  gsmsymgreq  19264  pmtrdifel  19312  pmtrdifwrdellem3  19315  pmtrdifwrdel2  19318  psgnunilem2  19327  psgnunilem3  19328  odeq  19382  gexid  19413  gexlem2  19414  gexdvds  19416  isslw  19440  sylow2alem1  19449  sylow2alem2  19450  efgval  19549  efgrelexlemb  19582  efgcpbllemb  19587  abl1  19694  dmdprd  19827  dprd2da  19871  pgpfac1lem5  19908  ring1  20079  lringuplu  20264  isabv  20376  islss  20494  lssacs  20527  reslmhm  20612  islbs  20636  pj1lmhm  20660  lbsacsbs  20718  isrrg  20840  zringlpir  20970  psgndiflemA  21087  ocvfval  21152  elocv  21154  iunocv  21167  frlmlbs  21285  islindf  21300  islinds2  21301  islindf2  21302  lindfrn  21309  lsslindf  21318  islindf4  21326  opsrval  21529  ply1coe  21749  cply1coe0bi  21753  mat0dimcrng  21901  mdetunilem1  22043  mdetunilem9  22051  cpmat  22140  cpmatel  22142  1elcpmat  22146  m2cpminvid2lem  22185  basgen2  22421  bastop1  22425  isclo  22520  ordtbaslem  22621  iscn  22668  cnpval  22669  iscnp  22670  iscnp3  22677  lmbr  22691  lmbr2  22692  lmbrf  22693  cnprest  22722  cnprest2  22723  t0sep  22757  isreg  22765  t1sep2  22802  tgcmp  22834  1stcclb  22877  1stcfb  22878  2ndc1stc  22884  1stcrest  22886  2ndcdisj  22889  islly  22901  isnlly  22902  lly1stc  22929  isref  22942  islocfin  22950  elkgen  22969  kgencn  22989  elpt  23005  elptr  23006  ptcnplem  23054  tx1stc  23083  cnmpt21  23104  kqt0lem  23169  isr0  23170  regr1lem2  23173  r0sep  23181  nrmr0reg  23182  flffbas  23428  cnflf  23435  cnflf2  23436  lmflf  23438  txflf  23439  fclsopni  23448  fclsnei  23452  fclsrest  23457  fcfnei  23468  cnfcf  23475  alexsubb  23479  alexsubALTlem3  23482  qustgplem  23554  tsmsfbas  23561  tsmsres  23577  tsmsf1o  23578  tsmsxplem1  23586  ustval  23636  isust  23637  ustincl  23641  ustdiag  23642  ustinvel  23643  ustexhalf  23644  ust0  23653  utopval  23666  ucnval  23711  isucn  23712  isucn2  23713  ucnima  23715  iscfilu  23722  ispsmet  23739  ismet  23758  isxmet  23759  imasdsf1olem  23808  imasf1oxmet  23810  imasf1omet  23811  metss  23946  met1stc  23959  prdsxmslem2  23967  txmetcnp  23985  metucn  24009  tngngp3  24102  nlmvscn  24133  nmoval  24161  nmolb  24163  qtopbaslem  24204  cncfval  24333  elcncf2  24335  mulc1cncf  24350  cncfmet  24354  evth  24404  lebnumlem3  24408  lebnum  24409  xlebnum  24410  ishtpy  24417  isphtpy  24426  pi1xfr  24500  pi1coghm  24506  isclmp  24542  ipcn  24692  lmmbr2  24705  lmmbr3  24706  lmmbrf  24708  cfilfval  24710  iscfil  24711  fmcfil  24718  caufval  24721  iscau  24722  iscau2  24723  iscau3  24724  iscau4  24725  iscauf  24726  caucfil  24729  cfilresi  24741  causs  24744  lmclim  24749  cmetcusp1  24799  minveclem4c  24871  minveclem2  24872  minveclem3b  24874  minveclem4  24878  minveclem6  24880  minveclem7  24881  ovolicc2lem3  24965  ismbl  24972  dyadmax  25044  dyadmbllem  25045  dyadmbl  25046  opnmbllem  25047  ismbf1  25070  ismbf  25074  mbfeqalem2  25088  mbflimsup  25112  mbfi1fseqlem6  25167  mbfi1flimlem  25169  itg2seq  25189  itg2monolem1  25197  isibl  25212  ply1divex  25583  fta1g  25614  dgrco  25718  plydivex  25739  fta1  25750  vieta1  25754  aannenlem1  25770  aannenlem2  25771  aalioulem2  25775  aalioulem3  25776  ulmval  25821  ulm2  25826  ulmi  25827  ulmres  25829  ulmshftlem  25830  ulmcaulem  25835  ulmcau  25836  ulmss  25838  ulmbdd  25839  ulmdvlem1  25841  ulmdvlem3  25843  pilem2  25893  pilem3  25894  cxpcn3  26183  dmarea  26389  rlimcnp  26397  scvxcvx  26417  lgamgulmlem2  26461  lgamgulmlem3  26462  lgamgulmlem5  26464  lgambdd  26468  lgamcvglem  26471  isppw2  26546  perfectlem2  26660  2sqlem6  26853  2sqlem10  26858  addsq2reu  26870  2sqreulem1  26876  2sqreunnlem1  26879  dchrisumlema  26918  dchrisumlem2  26920  dchrisumlem3  26921  pntpbnd  27018  pntibndlem3  27022  pntibnd  27023  pntleme  27038  pntlem3  27039  pntlemp  27040  pnt3  27042  sltval  27077  nosupprefixmo  27130  noinfprefixmo  27131  nosupcbv  27132  nosupno  27133  nosupdm  27134  nosupfv  27136  nosupres  27137  nosupbnd1lem1  27138  nosupbnd1lem3  27140  nosupbnd1lem5  27142  noinfcbv  27147  noinfno  27148  noinfdm  27149  noinffv  27151  noinfres  27152  noinfbnd1lem3  27155  noinfbnd1lem5  27157  noetalem1  27171  noetalem2  27172  nocvxminlem  27205  brsslt  27213  conway  27226  etasslt  27240  slerec  27246  madebdaylemlrcut  27316  madebday  27317  cofcutr  27331  lrrecfr  27343  addsprop  27376  negsunif  27443  istrkgld  27575  axtg5seg  27581  tgcgr4  27647  perpln1  27826  perpln2  27827  isperp  27828  brbtwn2  28028  colinearalg  28033  axsegconlem1  28040  axsegcon  28050  ax5seglem4  28055  ax5seglem5  28056  axlowdim  28084  axeuclidlem  28085  axcontlem1  28087  axcontlem2  28088  axcontlem4  28090  axcontlem5  28091  axcontlem8  28094  axcontlem12  28098  elntg2  28108  uvtxusgr  28524  rgrx0ndm  28715  ewlksfval  28723  wksfval  28731  wwlks  28954  wlkiswwlks2  28994  clwwlk  29101  1conngr  29312  frgrwopregasn  29434  frgrwopregbsn  29435  frgrwopreglem5ALT  29440  frgrregord013  29513  isgrpo  29613  isgrpoi  29614  grpoideu  29625  grpoidinv2  29631  vciOLD  29677  isvclem  29693  cnidOLD  29698  isnvlem  29726  nvi  29730  lnoval  29868  islno  29869  isblo3i  29917  blo3i  29918  blocnilem  29920  ajfval  29925  ubthlem1  29986  ubthlem2  29987  ubthlem3  29988  ubth  29989  minvecolem2  29991  minvecolem3  29992  minvecolem4c  29995  minvecolem4  29996  minvecolem5  29997  minvecolem6  29998  minvecolem7  29999  h2hcau  30095  h2hlm  30096  hilid  30277  hcau  30300  hlimi  30304  hlim2  30308  ocel  30397  adjsym  30949  ellnop  30974  ellnfn  30999  hhcno  31020  hhcnf  31021  lnopeq  31125  elunop2  31129  lnophm  31135  lnconi  31149  lnopcnbd  31152  lnfncnbd  31173  imaelshi  31174  riesz3i  31178  riesz4i  31179  riesz4  31180  riesz1  31181  cnlnadjlem2  31184  cnlnadjlem5  31187  cnlnadjlem8  31190  cnlnadji  31192  nmopadjlei  31204  cnvbraval  31226  leopg  31238  leoppos  31242  mdbr  31410  dmdbr  31415  cdj3i  31557  disjunsn  31690  funcnv5mpt  31762  fgreu  31766  fcnvgreu  31767  xrge0infss  31844  wrdt2ind  31988  resspos  32007  mgccole1  32031  mgccole2  32032  mgcmnt1  32033  mgcmnt2  32034  gsumhashmul  32079  isomnd  32090  inftmrel  32197  isinftm  32198  archiabl  32215  isarchiofld  32297  0nellinds  32345  lindssn  32352  elrspunidl  32397  prmidl  32409  ismxidl  32429  crefeq  32656  zarcmplem  32692  esum2d  32922  sigaval  32940  issgon  32952  isrnmeas  33029  ismbfm  33080  mbfmcst  33089  elcarsg  33135  sitgval  33162  eulerpartlemd  33196  ballotleme  33326  tgoldbachgt  33506  bnj1185  33635  bnj1385  33674  bnj66  33702  bnj106  33710  bnj155  33721  bnj852  33763  bnj893  33770  bnj1228  33853  bnj1234  33855  bnj1463  33897  nummin  33925  derangenlem  33993  subfacp1lem3  34004  subfacp1lem5  34006  subfacp1lem6  34007  subfacp1  34008  erdszelem8  34020  kur14  34038  cnpconn  34052  resconn  34068  cvmscbv  34080  iscvm  34081  cvmsi  34087  cvmsval  34088  cvmlift3lem2  34142  snmlval  34153  satfv1  34185  fmlasucdisj  34221  satffunlem1lem1  34224  satffunlem2lem1  34226  satfv1fvfmla1  34245  mclsssvlem  34384  mclsval  34385  mclsax  34391  mclsind  34392  dfon2lem9  34593  dfrdg2  34597  dfrdg3  34598  fwddifnval  34965  nn0prpwlem  35011  isfne  35028  isfne4  35029  isfne2  35031  isfne3  35032  neibastop3  35051  topmeet  35053  topjoin  35054  filnetlem4  35070  unblimceq0lem  35186  unblimceq0  35187  unbdqndv2  35191  taupilemrplb  36005  fin2so  36279  lindsadd  36285  matunitlindflem2  36289  ptrecube  36292  poimirlem2  36294  poimirlem3  36295  poimirlem4  36296  poimirlem24  36316  poimirlem25  36317  poimirlem26  36318  poimirlem27  36319  poimirlem28  36320  poimirlem29  36321  poimirlem30  36322  poimirlem32  36324  poimir  36325  heicant  36327  mblfinlem1  36329  mblfinlem2  36330  voliunnfl  36336  volsupnfl  36337  mbfresfi  36338  itg2addnc  36346  upixp  36402  indexdom  36407  filbcmb  36413  sdclem2  36415  fdc  36418  lmclim2  36431  caures  36433  istotbnd  36442  istotbnd3  36444  sstotbnd  36448  isbnd  36453  heibor  36494  bfp  36497  rrncmslem  36505  isgrpda  36628  idlval  36686  isidl  36687  0idl  36698  unichnidl  36704  pridl  36710  ismaxidl  36713  smprngopr  36725  igenval2  36739  prnc  36740  ispridlc  36743  scottexf  36841  scott0f  36842  disjsuc2  37066  riotasvd  37631  islfl  37735  eqlkr  37774  eqlkr3  37776  glbconN  38052  glbconNOLD  38053  hlsuprexch  38057  ispsubsp  38421  ldilset  38785  isldil  38786  dilsetN  38829  isdilN  38830  trlset  38837  trlval  38838  cdleme27b  39044  cdleme29b  39051  cdleme31so  39055  cdleme31sn1  39057  cdleme31sn1c  39064  cdleme31fv  39066  cdleme40v  39145  istendo  39436  cdlemkid3N  39609  cdlemkid4  39610  cdlemkid5  39611  dihfval  39907  dihval  39908  islpolN  40159  hdmapffval  40502  hdmapfval  40503  hdmapval  40504  hdmapval2lem  40507  hgmapffval  40561  hgmapfval  40562  hgmapval  40563  hgmapvs  40567  sticksstones2  40768  qsalrel  40874  fsuppind  40951  sn-sup2  41124  isnacs  41213  isnacs2  41215  nacsfix  41221  mzpclval  41234  elmzpcl  41235  rencldnfilem  41329  infmrgelbi  41387  pellfundre  41390  pellfundlb  41393  wepwsolem  41555  fnwe2lem2  41564  aomclem8  41574  dfac11  41575  gicabl  41612  islnr3  41628  hbtlem2  41637  hbtlem5  41641  onintunirab  41747  onsucf1lem  41790  cantnfresb  41845  safesnsupfilb  41940  rp-brsslt  41945  fiinfi  42095  clsk1independent  42568  ntrclsk13  42593  gneispacess2  42668  imo72b2lem0  42688  imo72b2lem2  42690  imo72b2lem1  42692  imo72b2  42695  scottelrankd  42777  mnuop23d  42796  ismnushort  42831  evth2f  43470  evthf  43482  fnchoice  43484  uzwo4  43511  wessf1ornlem  43653  disjinfi  43662  rnmptlb  43719  rnmptbdd  43721  rnmptbd2  43726  rnmptbd  43733  dstregt0  43764  upbdrech2  43791  rexabslelem  43901  rexabsle  43902  uzub  43914  infrpgernmpt  43948  mccl  44087  ellimcabssub0  44106  climf  44111  clim2f  44125  limsupre  44130  clim2cf  44139  clim0cf  44143  climf2  44155  clim2f2  44159  clim2d  44162  limsupref  44174  limsupbnd1f  44175  climinf2  44196  limsuppnf  44200  climinfmpt  44204  climinf3  44205  limsupubuzmpt  44208  limsupmnf  44210  limsupre2lem  44213  limsupre2  44214  limsupmnfuzlem  44215  limsupmnfuz  44216  limsupre2mpt  44219  limsupre3lem  44221  limsupre3  44222  limsupre3mpt  44223  limsupre3uz  44225  limsupreuz  44226  limsupreuzmpt  44228  climuz  44233  liminfreuzlem  44291  liminfreuz  44292  cnrefiisplem  44318  xlimmnfvlem1  44321  xlimmnfv  44323  xlimpnfvlem1  44325  xlimpnfv  44327  xlimmnfmpt  44332  xlimpnfmpt  44333  cncfshift  44363  cncfperiod  44368  fperdvper  44408  dvbdfbdioo  44419  ioodvbdlimc1lem2  44421  ioodvbdlimc2lem  44423  dvnprodlem3  44437  stoweidlem5  44494  stoweidlem9  44498  stoweidlem15  44504  stoweidlem16  44505  stoweidlem27  44516  stoweidlem28  44517  stoweidlem31  44520  stoweidlem34  44523  stoweidlem37  44526  stoweidlem46  44535  stoweidlem48  44537  stoweidlem51  44540  stoweidlem52  44541  stoweidlem59  44548  wallispilem3  44556  stirlinglem13  44575  fourierdlem2  44598  fourierdlem3  44599  fourierdlem16  44612  fourierdlem20  44616  fourierdlem21  44617  fourierdlem22  44618  fourierdlem25  44621  fourierdlem39  44635  fourierdlem42  44638  fourierdlem54  44649  fourierdlem64  44659  fourierdlem77  44672  fourierdlem83  44678  fourierdlem103  44698  fourierdlem104  44699  subsaliuncllem  44846  iundjiun  44949  meaiunincf  44972  caragenval  44982  isome  44983  caragenel  44984  omessle  44987  ovnlerp  45051  hoidmvlelem3  45086  hoidmvle  45089  issmflem  45216  issmfgt  45245  smfmullem2  45281  smfmullem4  45283  smfmul  45284  smfsuplem2  45301  smfsup  45303  smfinflem  45306  smfinf  45307  fsupdm  45331  finfdm  45335  cfsetsnfsetf  45540  cbvral2  45583  2reu8i  45593  2reuimp0  45594  dfdfat2  45608  iccpart  45856  iccpartigtl  45863  paireqne  45951  reupr  45962  perfectALTVlem2  46162  bgoldbachlt  46253  tgoldbachlt  46256  isomgreqve  46265  isomushgr  46266  isomuspgrlem2  46273  isomgrsym  46276  isomgrtr  46279  ushrisomgr  46281  upwlksfval  46285  mgmhmima  46344  nn0mnd  46361  lidlmsgrp  46472  lidlrng  46473  uzlidlring  46475  ply1mulgsumlem1  46715  ply1mulgsumlem2  46716  linindslinci  46777  lindslinindsimp1  46786  lindslinindsimp2lem5  46791  lindslinindsimp2  46792  linds0  46794  lindsrng01  46797  snlindsntor  46800  lmod1  46821  ldepsnlinc  46837  bigoval  46883  elbigo2r  46887  nn0sumshdiglem2  46956  eenglngeehlnmlem1  47071  eenglngeehlnmlem2  47072  lubeldm2d  47239  glbeldm2d  47240  lubsscl  47241  glbsscl  47242  ipolubdm  47260  ipolub  47261  ipoglbdm  47263  ipoglb  47264  isthincd2lem2  47304  setrec1lem2  47381