Theorem ralbidv 3197

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2114  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3143

This theorem is referenced by:  2ralbidv  3199  rexralbidv  3301  raleqbi1dvOLD  3417  raleqbidvOLD  3423  cbvral2vw  3461  cbvral2v  3464  rspceaimv  3628  rspc2  3631  rspc2v  3633  rspc3v  3636  reu6i  3719  reu7  3723  sbcralt  3855  reu8nf  3860  raaan  4460  raaanv  4461  raaan2  4464  2reu4lem  4465  reusngf  4612  2ralsng  4616  rexreusng  4617  reuprg0  4638  issn  4763  2ralunsn  4825  elintg  4884  elintrabg  4889  eliin  4924  disjprgw  5061  disjprg  5062  disjxun  5064  brralrspcev  5126  reusv2lem2  5300  reusv3  5306  poeq1  5477  somo  5510  frirr  5532  fr2nr  5533  frminex  5535  wereu2  5552  posn  5637  frsn  5639  ralxpf  5717  cnvpo  6138  reu3op  6143  reuop  6144  fnmptfvd  6811  iinpreima  6837  dff4  6867  dff13f  7014  fpropnf1  7025  eusvobj2  7149  ovanraleqv  7180  f1opr  7210  ofreq  7412  sorpssuni  7458  sorpssint  7459  fr3nr  7494  onssmin  7512  funcnvuni  7636  f1oweALT  7673  frxp  7820  wrecseq123  7948  wfrlem1  7954  wfrlem3a  7957  wfrlem15  7969  smoeq  7987  tfrlem12  8025  tz7.48lem  8077  elixp2  8465  undifixp  8498  xpf1o  8679  nneneq  8700  ac6sfi  8762  frfi  8763  fipreima  8830  indexfi  8832  marypha1lem  8897  marypha1  8898  supeq1  8909  supeq3  8913  supmo  8916  eqsup  8920  supub  8923  suplub  8924  sup0  8930  supisoex  8938  eqinf  8948  infval  8950  infmo  8959  oieq1  8976  ordtypecbv  8981  ordtypelem3  8984  ordtypelem6  8987  ordtypelem7  8988  ordtypelem9  8990  wemaplem1  9010  wemaplem2  9011  zfregcl  9058  oemapval  9146  oemapvali  9147  cantnf  9156  wemapwe  9160  rankval3b  9255  unbndrank  9271  rankunb  9279  rankuni2b  9282  tcrank  9313  scottex  9314  scottexs  9316  scott0s  9317  bnd2  9322  updjud  9363  dfac8clem  9458  ac5num  9462  acni  9471  acni2  9472  alephval3  9536  dfac4  9548  dfac5lem5  9553  dfac5  9554  dfac2a  9555  dfac2b  9556  dfacacn  9567  kmlem2  9577  kmlem13  9588  cflem  9668  cflecard  9675  cfeq0  9678  cfsuc  9679  cfflb  9681  cofsmo  9691  cfsmolem  9692  cfcoflem  9694  coftr  9695  alephsing  9698  fin23lem11  9739  isfin3ds  9751  fin23lem17  9760  fin23lem39  9772  isf33lem  9788  isf34lem6  9802  fin1a2lem13  9834  hsmexlem4  9851  hsmex  9854  axcc2lem  9858  axcc3  9860  dcomex  9869  axdc2lem  9870  axdc3lem2  9873  axdc3lem3  9874  axdc3  9876  axdc4lem  9877  axcclem  9879  zorn2lem2  9919  zorn2lem7  9924  zorn2g  9925  zornn0g  9927  ttukeylem7  9937  axdclem2  9942  brdom3  9950  brdom7disj  9953  brdom6disj  9954  alephval2  9994  inar1  10197  axgroth6  10250  pinq  10349  nqereu  10351  prlem934  10455  supexpr  10476  supsrlem  10533  axpre-sup  10591  dedekind  10803  dedekindle  10804  fiminreOLD  11590  lbreu  11591  sup2  11597  infm3  11600  nnsub  11682  uzwo  12312  nnwof  12315  ublbneg  12334  lbzbi  12337  zsupss  12338  uzsupss  12341  uzwo3  12344  zmax  12346  rpnnen1lem1  12378  rpnnen1lem3  12379  rpnnen1lem4  12380  rpnnen1lem5  12381  xrsupsslem  12701  xrinfmsslem  12702  xrsupss  12703  xrinfmss  12704  flval2  13185  axdc4uzlem  13352  ssnn0fi  13354  fsuppmapnn0fiubex  13361  faclbnd4lem4  13657  bccl  13683  hashgt12el  13784  hashbc  13812  hashge2el2dif  13839  wrdind  14084  wrd2ind  14085  rexanre  14706  rexico  14713  cau4  14716  reusq0  14822  clim  14851  rlim  14852  rlim2  14853  clim2  14861  clim2c  14862  clim0c  14864  rlim0  14865  rlim0lt  14866  ello12r  14874  ello1d  14880  elo12r  14885  rlimresb  14922  rlimcld2  14935  climabs0  14942  rlimo1  14973  lo1add  14983  lo1mul  14984  isercoll  15024  incexclem  15191  sqrt2irr  15602  gcdcllem1  15848  gcdcllem2  15849  dfgcd2  15894  fissn0dvds  15963  dvdslcmf  15975  lcmfledvds  15976  lcmf  15977  lcmfunsnlem1  15981  lcmfunsnlem2lem1  15982  lcmfunsnlem  15985  lcmfdvds  15986  reumodprminv  16141  pc2dvds  16215  pcz  16217  prmpwdvds  16240  infpn2  16249  prmreclem2  16253  prmreclem3  16254  prmreclem5  16256  prmreclem6  16257  vdwlem6  16322  vdwlem8  16324  vdwlem13  16329  vdwnnlem1  16331  vdwnn  16334  ramcl  16365  cshwrepswhash1  16436  prdsleval  16750  imasval  16784  imasaddfnlem  16801  imasvscafn  16810  mrisval  16901  isacs  16922  isacs2  16924  isacs1i  16928  mreacs  16929  acsfn  16930  acsfn2  16934  iscatd  16944  catidex  16945  catideu  16946  cidval  16948  catidd  16951  comfeq  16976  catpropd  16979  ismon  17003  isfunc  17134  isnat  17217  isinito  17260  istermo  17261  isprs  17540  drsdirfi  17548  ispos  17557  lubfval  17588  lubeldm  17591  lubval  17594  lubprop  17596  lublecllem  17598  glbfval  17601  glbeldm  17604  glbval  17607  glbprop  17609  joinval2lem  17618  joinlem  17621  meetval2lem  17632  meetlem  17635  isglbd  17727  lubl  17730  lubun  17733  clatleglb  17736  poslubmo  17756  posglbmo  17757  poslubd  17758  ipodrsima  17775  isdlat  17803  mgm1  17868  gsumval2  17896  sgrp1  17910  mhmima  17989  mndind  17992  gsumwspan  18011  efmndmnd  18054  smndex1mnd  18075  sgrp2rid2  18091  sgrp2rid2ex  18092  sgrp2nmndlem4  18093  pwmnd  18102  dfgrp2  18128  isgrpinv  18156  grpidinv  18159  dfgrp3lem  18197  issubg4  18298  0subg  18304  isnsg2  18308  nsgacs  18314  elnmz  18315  cycsubgcl  18349  ghmrn  18371  ghmnsgima  18382  isga  18421  orbsta  18443  cntzfval  18450  elcntz  18452  resscntz  18462  oppgsubg  18491  symgextfo  18550  gsmsymgreqlem2  18559  gsmsymgreq  18560  pmtrdifel  18608  pmtrdifwrdellem3  18611  pmtrdifwrdel2  18614  psgnunilem2  18623  psgnunilem3  18624  odeq  18678  gexid  18706  gexlem2  18707  gexdvds  18709  isslw  18733  sylow2alem1  18742  sylow2alem2  18743  efgval  18843  efgrelexlemb  18876  efgcpbllemb  18881  abl1  18986  dmdprd  19120  dprd2da  19164  pgpfac1lem5  19201  ring1  19352  isabv  19590  islss  19706  lssacs  19739  reslmhm  19824  islbs  19848  pj1lmhm  19872  lbsacsbs  19928  isrrg  20061  opsrval  20255  ply1coe  20464  cply1coe0bi  20468  zringlpir  20636  psgndiflemA  20745  ocvfval  20810  elocv  20812  iunocv  20825  frlmlbs  20941  islindf  20956  islinds2  20957  islindf2  20958  lindfrn  20965  lsslindf  20974  islindf4  20982  mat0dimcrng  21079  mdetunilem1  21221  mdetunilem9  21229  cpmat  21317  cpmatel  21319  1elcpmat  21323  m2cpminvid2lem  21362  basgen2  21597  bastop1  21601  isclo  21695  ordtbaslem  21796  iscn  21843  cnpval  21844  iscnp  21845  iscnp3  21852  lmbr  21866  lmbr2  21867  lmbrf  21868  cnprest  21897  cnprest2  21898  t0sep  21932  isreg  21940  t1sep2  21977  tgcmp  22009  1stcclb  22052  1stcfb  22053  2ndc1stc  22059  1stcrest  22061  2ndcdisj  22064  islly  22076  isnlly  22077  lly1stc  22104  isref  22117  islocfin  22125  elkgen  22144  kgencn  22164  elpt  22180  elptr  22181  ptcnplem  22229  tx1stc  22258  cnmpt21  22279  kqt0lem  22344  isr0  22345  regr1lem2  22348  r0sep  22356  nrmr0reg  22357  flffbas  22603  cnflf  22610  cnflf2  22611  lmflf  22613  txflf  22614  fclsopni  22623  fclsnei  22627  fclsrest  22632  fcfnei  22643  cnfcf  22650  alexsubb  22654  alexsubALTlem3  22657  qustgplem  22729  tsmsfbas  22736  tsmsres  22752  tsmsf1o  22753  tsmsxplem1  22761  ustval  22811  isust  22812  ustincl  22816  ustdiag  22817  ustinvel  22818  ustexhalf  22819  ust0  22828  utopval  22841  ucnval  22886  isucn  22887  isucn2  22888  ucnima  22890  iscfilu  22897  ispsmet  22914  ismet  22933  isxmet  22934  imasdsf1olem  22983  imasf1oxmet  22985  imasf1omet  22986  metss  23118  met1stc  23131  prdsxmslem2  23139  txmetcnp  23157  metucn  23181  tngngp3  23265  nlmvscn  23296  nmoval  23324  nmolb  23326  qtopbaslem  23367  cncfval  23496  elcncf2  23498  mulc1cncf  23513  cncfmet  23516  evth  23563  lebnumlem3  23567  lebnum  23568  xlebnum  23569  ishtpy  23576  isphtpy  23585  pi1xfr  23659  pi1coghm  23665  isclmp  23701  ipcn  23849  lmmbr2  23862  lmmbr3  23863  lmmbrf  23865  cfilfval  23867  iscfil  23868  fmcfil  23875  caufval  23878  iscau  23879  iscau2  23880  iscau3  23881  iscau4  23882  iscauf  23883  caucfil  23886  cfilresi  23898  causs  23901  lmclim  23906  cmetcusp1  23956  minveclem4c  24028  minveclem2  24029  minveclem3b  24031  minveclem4  24035  minveclem6  24037  minveclem7  24038  ovolicc2lem3  24120  ismbl  24127  dyadmax  24199  dyadmbllem  24200  dyadmbl  24201  opnmbllem  24202  ismbf1  24225  ismbf  24229  mbfeqalem2  24243  mbflimsup  24267  mbfi1fseqlem6  24321  mbfi1flimlem  24323  itg2seq  24343  itg2monolem1  24351  isibl  24366  ply1divex  24730  fta1g  24761  dgrco  24865  plydivex  24886  fta1  24897  vieta1  24901  aannenlem1  24917  aannenlem2  24918  aalioulem2  24922  aalioulem3  24923  ulmval  24968  ulm2  24973  ulmi  24974  ulmres  24976  ulmshftlem  24977  ulmcaulem  24982  ulmcau  24983  ulmss  24985  ulmbdd  24986  ulmdvlem1  24988  ulmdvlem3  24990  pilem2  25040  pilem3  25041  cxpcn3  25329  dmarea  25535  rlimcnp  25543  scvxcvx  25563  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem5  25610  lgambdd  25614  lgamcvglem  25617  isppw2  25692  perfectlem2  25806  2sqlem6  25999  2sqlem10  26004  addsq2reu  26016  2sqreulem1  26022  2sqreunnlem1  26025  dchrisumlema  26064  dchrisumlem2  26066  dchrisumlem3  26067  pntpbnd  26164  pntibndlem3  26168  pntibnd  26169  pntleme  26184  pntlem3  26185  pntlemp  26186  pnt3  26188  istrkgld  26245  axtg5seg  26251  tgcgr4  26317  perpln1  26496  perpln2  26497  isperp  26498  brbtwn2  26691  colinearalg  26696  axsegconlem1  26703  axsegcon  26713  ax5seglem4  26718  ax5seglem5  26719  axlowdim  26747  axeuclidlem  26748  axcontlem1  26750  axcontlem2  26751  axcontlem4  26753  axcontlem5  26754  axcontlem8  26757  axcontlem12  26761  elntg2  26771  uvtxusgr  27184  rgrx0ndm  27375  ewlksfval  27383  wksfval  27391  wwlks  27613  wlkiswwlks2  27653  clwwlk  27761  1conngr  27973  frgrwopregasn  28095  frgrwopregbsn  28096  frgrwopreglem5ALT  28101  frgrregord013  28174  isgrpo  28274  isgrpoi  28275  grpoideu  28286  grpoidinv2  28292  vciOLD  28338  isvclem  28354  cnidOLD  28359  isnvlem  28387  nvi  28391  lnoval  28529  islno  28530  isblo3i  28578  blo3i  28579  blocnilem  28581  ajfval  28586  ubthlem1  28647  ubthlem2  28648  ubthlem3  28649  ubth  28650  minvecolem2  28652  minvecolem3  28653  minvecolem4c  28656  minvecolem4  28657  minvecolem5  28658  minvecolem6  28659  minvecolem7  28660  h2hcau  28756  h2hlm  28757  hilid  28938  hcau  28961  hlimi  28965  hlim2  28969  ocel  29058  adjsym  29610  ellnop  29635  ellnfn  29660  hhcno  29681  hhcnf  29682  lnopeq  29786  elunop2  29790  lnophm  29796  lnconi  29810  lnopcnbd  29813  lnfncnbd  29834  imaelshi  29835  riesz3i  29839  riesz4i  29840  riesz4  29841  riesz1  29842  cnlnadjlem2  29845  cnlnadjlem5  29848  cnlnadjlem8  29851  cnlnadji  29853  nmopadjlei  29865  cnvbraval  29887  leopg  29899  leoppos  29903  mdbr  30071  dmdbr  30076  cdj3i  30218  disjunsn  30344  funcnv5mpt  30413  fgreu  30417  fcnvgreu  30418  xrge0infss  30484  wrdt2ind  30627  resspos  30646  isomnd  30702  inftmrel  30809  isinftm  30810  archiabl  30827  isarchiofld  30890  0nellinds  30935  lindssn  30939  prmidl  30957  ismxidl  30971  crefeq  31109  esum2d  31352  sigaval  31370  issgon  31382  isrnmeas  31459  ismbfm  31510  isanmbfm  31514  mbfmcst  31517  elcarsg  31563  sitgval  31590  eulerpartlemd  31624  ballotleme  31754  tgoldbachgt  31934  bnj1185  32065  bnj1385  32104  bnj66  32132  bnj106  32140  bnj155  32151  bnj852  32193  bnj893  32200  bnj1228  32283  bnj1234  32285  bnj1463  32327  derangenlem  32418  subfacp1lem3  32429  subfacp1lem5  32431  subfacp1lem6  32432  subfacp1  32433  erdszelem8  32445  kur14  32463  cnpconn  32477  resconn  32493  cvmscbv  32505  iscvm  32506  cvmsi  32512  cvmsval  32513  cvmlift3lem2  32567  snmlval  32578  satfv1  32610  fmlasucdisj  32646  satffunlem1lem1  32649  satffunlem2lem1  32651  satfv1fvfmla1  32670  mclsssvlem  32809  mclsval  32810  mclsax  32816  mclsind  32817  dfpo2  32991  dfon2lem9  33036  dfrdg2  33040  dfrdg3  33041  frpomin  33078  poseq  33095  soseq  33096  frecseq123  33119  frrlem1  33123  frrlem13  33135  sltval  33154  noprefixmo  33202  nosupno  33203  nosupdm  33204  nosupfv  33206  nosupres  33207  nosupbnd1lem1  33208  nosupbnd1lem3  33210  nosupbnd1lem5  33212  noetalem5  33221  noeta  33222  nocvxminlem  33247  brsslt  33254  conway  33264  etasslt  33274  slerec  33277  fwddifnval  33624  nn0prpwlem  33670  isfne  33687  isfne4  33688  isfne2  33690  isfne3  33691  neibastop3  33710  topmeet  33712  topjoin  33713  filnetlem4  33729  unblimceq0lem  33845  unblimceq0  33846  unbdqndv2  33850  taupilemrplb  34604  csbwrecsg  34611  fin2so  34894  lindsadd  34900  matunitlindflem2  34904  ptrecube  34907  poimirlem2  34909  poimirlem3  34910  poimirlem4  34911  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  poimirlem29  34936  poimirlem30  34937  poimirlem32  34939  poimir  34940  heicant  34942  mblfinlem1  34944  mblfinlem2  34945  voliunnfl  34951  volsupnfl  34952  mbfresfi  34953  itg2addnc  34961  upixp  35019  indexdom  35024  filbcmb  35030  sdclem2  35032  fdc  35035  lmclim2  35048  caures  35050  istotbnd  35062  istotbnd3  35064  sstotbnd  35068  isbnd  35073  heibor  35114  bfp  35117  rrncmslem  35125  isgrpda  35248  idlval  35306  isidl  35307  0idl  35318  unichnidl  35324  pridl  35330  ismaxidl  35333  smprngopr  35345  igenval2  35359  prnc  35360  ispridlc  35363  scottexf  35461  scott0f  35462  riotasvd  36107  islfl  36211  eqlkr  36250  eqlkr3  36252  glbconN  36528  hlsuprexch  36532  ispsubsp  36896  ldilset  37260  isldil  37261  dilsetN  37304  isdilN  37305  trlset  37312  trlval  37313  cdleme27b  37519  cdleme29b  37526  cdleme31so  37530  cdleme31sn1  37532  cdleme31sn1c  37539  cdleme31fv  37541  cdleme40v  37620  istendo  37911  cdlemkid3N  38084  cdlemkid4  38085  cdlemkid5  38086  dihfval  38382  dihval  38383  islpolN  38634  hdmapffval  38977  hdmapfval  38978  hdmapval  38979  hdmapval2lem  38982  hgmapffval  39036  hgmapfval  39037  hgmapval  39038  hgmapvs  39042  qsalrel  39145  isnacs  39321  isnacs2  39323  nacsfix  39329  mzpclval  39342  elmzpcl  39343  rencldnfilem  39437  infmrgelbi  39495  pellfundre  39498  pellfundlb  39501  wepwsolem  39662  fnwe2lem2  39671  aomclem8  39681  dfac11  39682  gicabl  39719  islnr3  39735  hbtlem2  39744  hbtlem5  39748  fiinfi  39952  clsk1independent  40416  ntrclsk13  40441  gneispacess2  40516  imo72b2lem0  40536  imo72b2lem2  40538  imo72b2lem1  40541  imo72b2  40545  scottelrankd  40603  mnuop23d  40622  evth2f  41292  evthf  41304  fnchoice  41306  uzwo4  41335  wessf1ornlem  41465  disjinfi  41474  rnmptlb  41534  rnmptbdd  41536  rnmptbd2  41541  rnmptbd  41548  dstregt0  41567  upbdrech2  41595  fiminre2  41666  rexabslelem  41712  rexabsle  41713  uzub  41725  infrpgernmpt  41761  mccl  41899  ellimcabssub0  41918  climf  41923  clim2f  41937  limsupre  41942  clim2cf  41951  clim0cf  41955  climf2  41967  clim2f2  41971  clim2d  41974  limsupref  41986  limsupbnd1f  41987  climinf2  42008  limsuppnf  42012  climinfmpt  42016  climinf3  42017  limsupubuzmpt  42020  limsupmnf  42022  limsupre2lem  42025  limsupre2  42026  limsupmnfuzlem  42027  limsupmnfuz  42028  limsupre2mpt  42031  limsupre3lem  42033  limsupre3  42034  limsupre3mpt  42035  limsupre3uz  42037  limsupreuz  42038  limsupreuzmpt  42040  climuz  42045  liminfreuzlem  42103  liminfreuz  42104  cnrefiisplem  42130  xlimmnfvlem1  42133  xlimmnfv  42135  xlimpnfvlem1  42137  xlimpnfv  42139  xlimmnfmpt  42144  xlimpnfmpt  42145  cncfshift  42177  cncfperiod  42182  fperdvper  42223  dvbdfbdioo  42235  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  dvnprodlem3  42253  stoweidlem5  42310  stoweidlem9  42314  stoweidlem15  42320  stoweidlem16  42321  stoweidlem27  42332  stoweidlem28  42333  stoweidlem31  42336  stoweidlem34  42339  stoweidlem37  42342  stoweidlem46  42351  stoweidlem48  42353  stoweidlem51  42356  stoweidlem52  42357  stoweidlem59  42364  wallispilem3  42372  stirlinglem13  42391  fourierdlem2  42414  fourierdlem3  42415  fourierdlem16  42428  fourierdlem20  42432  fourierdlem21  42433  fourierdlem22  42434  fourierdlem25  42437  fourierdlem39  42451  fourierdlem42  42454  fourierdlem54  42465  fourierdlem64  42475  fourierdlem77  42488  fourierdlem83  42494  fourierdlem103  42514  fourierdlem104  42515  subsaliuncllem  42660  iundjiun  42762  meaiunincf  42785  caragenval  42795  isome  42796  caragenel  42797  omessle  42800  ovnlerp  42864  hoidmvlelem3  42899  hoidmvle  42902  issmflem  43024  issmfgt  43053  smfmullem2  43087  smfmullem4  43089  smfmul  43090  smfsuplem2  43106  smfsup  43108  smfinflem  43111  smfinf  43112  cbvral2  43321  2reu8i  43332  2reuimp0  43333  dfdfat2  43347  iccpart  43596  iccpartigtl  43603  paireqne  43693  reupr  43704  perfectALTVlem2  43907  bgoldbachlt  43998  tgoldbachlt  44001  isomgreqve  44010  isomushgr  44011  isomuspgrlem2  44018  isomgrsym  44021  isomgrtr  44024  ushrisomgr  44026  upwlksfval  44030  mgmhmima  44089  nn0mnd  44106  lidlmsgrp  44217  lidlrng  44218  uzlidlring  44220  ply1mulgsumlem1  44460  ply1mulgsumlem2  44461  linindslinci  44523  lindslinindsimp1  44532  lindslinindsimp2lem5  44537  lindslinindsimp2  44538  linds0  44540  lindsrng01  44543  snlindsntor  44546  lmod1  44567  ldepsnlinc  44583  bigoval  44629  elbigo2r  44633  nn0sumshdiglem2  44702  eenglngeehlnmlem1  44744  eenglngeehlnmlem2  44745  setrec1lem2  44811