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 2110  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

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

This theorem is referenced by:  2ralbidv  3199  rexralbidv  3301  raleqbi1dvOLD  3418  raleqbidvOLD  3424  cbvral2vw  3462  cbvral2v  3465  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  4606  2ralsng  4610  rexreusng  4611  reuprg0  4632  issn  4757  2ralunsn  4819  elintg  4877  elintrabg  4882  eliin  4917  disjprgw  5054  disjprg  5055  disjxun  5057  brralrspcev  5119  reusv2lem2  5292  reusv3  5298  poeq1  5472  somo  5505  frirr  5527  fr2nr  5528  frminex  5530  wereu2  5547  posn  5632  frsn  5634  ralxpf  5712  cnvpo  6133  reu3op  6138  reuop  6139  fnmptfvd  6806  iinpreima  6832  dff4  6862  dff13f  7008  fpropnf1  7019  eusvobj2  7143  ovanraleqv  7174  f1opr  7204  ofreq  7406  sorpssuni  7452  sorpssint  7453  fr3nr  7488  onssmin  7506  funcnvuni  7630  f1oweALT  7667  frxp  7814  wrecseq123  7942  wfrlem1  7948  wfrlem3a  7951  wfrlem15  7963  smoeq  7981  tfrlem12  8019  tz7.48lem  8071  elixp2  8459  undifixp  8492  xpf1o  8673  nneneq  8694  ac6sfi  8756  frfi  8757  fipreima  8824  indexfi  8826  marypha1lem  8891  marypha1  8892  supeq1  8903  supeq3  8907  supmo  8910  eqsup  8914  supub  8917  suplub  8918  sup0  8924  supisoex  8932  eqinf  8942  infval  8944  infmo  8953  oieq1  8970  ordtypecbv  8975  ordtypelem3  8978  ordtypelem6  8981  ordtypelem7  8982  ordtypelem9  8984  wemaplem1  9004  wemaplem2  9005  zfregcl  9052  oemapval  9140  oemapvali  9141  cantnf  9150  wemapwe  9154  rankval3b  9249  unbndrank  9265  rankunb  9273  rankuni2b  9276  tcrank  9307  scottex  9308  scottexs  9310  scott0s  9311  bnd2  9316  updjud  9357  dfac8clem  9452  ac5num  9456  acni  9465  acni2  9466  alephval3  9530  dfac4  9542  dfac5lem5  9547  dfac5  9548  dfac2a  9549  dfac2b  9550  dfacacn  9561  kmlem2  9571  kmlem13  9582  cflem  9662  cflecard  9669  cfeq0  9672  cfsuc  9673  cfflb  9675  cofsmo  9685  cfsmolem  9686  cfcoflem  9688  coftr  9689  alephsing  9692  fin23lem11  9733  isfin3ds  9745  fin23lem17  9754  fin23lem39  9766  isf33lem  9782  isf34lem6  9796  fin1a2lem13  9828  hsmexlem4  9845  hsmex  9848  axcc2lem  9852  axcc3  9854  dcomex  9863  axdc2lem  9864  axdc3lem2  9867  axdc3lem3  9868  axdc3  9870  axdc4lem  9871  axcclem  9873  zorn2lem2  9913  zorn2lem7  9918  zorn2g  9919  zornn0g  9921  ttukeylem7  9931  axdclem2  9936  brdom3  9944  brdom7disj  9947  brdom6disj  9948  alephval2  9988  inar1  10191  axgroth6  10244  pinq  10343  nqereu  10345  prlem934  10449  supexpr  10470  supsrlem  10527  axpre-sup  10585  dedekind  10797  dedekindle  10798  fiminreOLD  11584  lbreu  11585  sup2  11591  infm3  11594  nnsub  11675  uzwo  12305  nnwof  12308  ublbneg  12327  lbzbi  12330  zsupss  12331  uzsupss  12334  uzwo3  12337  zmax  12339  rpnnen1lem1  12371  rpnnen1lem3  12372  rpnnen1lem4  12373  rpnnen1lem5  12374  xrsupsslem  12694  xrinfmsslem  12695  xrsupss  12696  xrinfmss  12697  flval2  13178  axdc4uzlem  13345  ssnn0fi  13347  fsuppmapnn0fiubex  13354  faclbnd4lem4  13650  bccl  13676  hashgt12el  13777  hashbc  13805  hashge2el2dif  13832  wrdind  14078  wrd2ind  14079  rexanre  14700  rexico  14707  cau4  14710  reusq0  14816  clim  14845  rlim  14846  rlim2  14847  clim2  14855  clim2c  14856  clim0c  14858  rlim0  14859  rlim0lt  14860  ello12r  14868  ello1d  14874  elo12r  14879  rlimresb  14916  rlimcld2  14929  climabs0  14936  rlimo1  14967  lo1add  14977  lo1mul  14978  isercoll  15018  incexclem  15185  sqrt2irr  15596  gcdcllem1  15842  gcdcllem2  15843  dfgcd2  15888  fissn0dvds  15957  dvdslcmf  15969  lcmfledvds  15970  lcmf  15971  lcmfunsnlem1  15975  lcmfunsnlem2lem1  15976  lcmfunsnlem  15979  lcmfdvds  15980  reumodprminv  16135  pc2dvds  16209  pcz  16211  prmpwdvds  16234  infpn2  16243  prmreclem2  16247  prmreclem3  16248  prmreclem5  16250  prmreclem6  16251  vdwlem6  16316  vdwlem8  16318  vdwlem13  16323  vdwnnlem1  16325  vdwnn  16328  ramcl  16359  cshwrepswhash1  16430  prdsleval  16744  imasval  16778  imasaddfnlem  16795  imasvscafn  16804  mrisval  16895  isacs  16916  isacs2  16918  isacs1i  16922  mreacs  16923  acsfn  16924  acsfn2  16928  iscatd  16938  catidex  16939  catideu  16940  cidval  16942  catidd  16945  comfeq  16970  catpropd  16973  ismon  16997  isfunc  17128  isnat  17211  isinito  17254  istermo  17255  isprs  17534  drsdirfi  17542  ispos  17551  lubfval  17582  lubeldm  17585  lubval  17588  lubprop  17590  lublecllem  17592  glbfval  17595  glbeldm  17598  glbval  17601  glbprop  17603  joinval2lem  17612  joinlem  17615  meetval2lem  17626  meetlem  17629  isglbd  17721  lubl  17724  lubun  17727  clatleglb  17730  poslubmo  17750  posglbmo  17751  poslubd  17752  ipodrsima  17769  isdlat  17797  mgm1  17862  gsumval2  17890  sgrp1  17904  mhmima  17983  mndind  17986  gsumwspan  18005  efmndmnd  18048  smndex1mnd  18069  sgrp2rid2  18085  sgrp2rid2ex  18086  sgrp2nmndlem4  18087  pwmnd  18096  dfgrp2  18122  isgrpinv  18150  grpidinv  18153  dfgrp3lem  18191  issubg4  18292  0subg  18298  isnsg2  18302  nsgacs  18308  elnmz  18309  cycsubgcl  18343  ghmrn  18365  ghmnsgima  18376  isga  18415  orbsta  18437  cntzfval  18444  elcntz  18446  resscntz  18456  oppgsubg  18485  symgextfo  18544  gsmsymgreqlem2  18553  gsmsymgreq  18554  pmtrdifel  18602  pmtrdifwrdellem3  18605  pmtrdifwrdel2  18608  psgnunilem2  18617  psgnunilem3  18618  odeq  18672  gexid  18700  gexlem2  18701  gexdvds  18703  isslw  18727  sylow2alem1  18736  sylow2alem2  18737  efgval  18837  efgrelexlemb  18870  efgcpbllemb  18875  abl1  18980  dmdprd  19114  dprd2da  19158  pgpfac1lem5  19195  ring1  19346  isabv  19584  islss  19700  lssacs  19733  reslmhm  19818  islbs  19842  pj1lmhm  19866  lbsacsbs  19922  isrrg  20055  opsrval  20249  ply1coe  20458  cply1coe0bi  20462  zringlpir  20630  psgndiflemA  20739  ocvfval  20804  elocv  20806  iunocv  20819  frlmlbs  20935  islindf  20950  islinds2  20951  islindf2  20952  lindfrn  20959  lsslindf  20968  islindf4  20976  mat0dimcrng  21073  mdetunilem1  21215  mdetunilem9  21223  cpmat  21311  cpmatel  21313  1elcpmat  21317  m2cpminvid2lem  21356  basgen2  21591  bastop1  21595  isclo  21689  ordtbaslem  21790  iscn  21837  cnpval  21838  iscnp  21839  iscnp3  21846  lmbr  21860  lmbr2  21861  lmbrf  21862  cnprest  21891  cnprest2  21892  t0sep  21926  isreg  21934  t1sep2  21971  tgcmp  22003  1stcclb  22046  1stcfb  22047  2ndc1stc  22053  1stcrest  22055  2ndcdisj  22058  islly  22070  isnlly  22071  lly1stc  22098  isref  22111  islocfin  22119  elkgen  22138  kgencn  22158  elpt  22174  elptr  22175  ptcnplem  22223  tx1stc  22252  cnmpt21  22273  kqt0lem  22338  isr0  22339  regr1lem2  22342  r0sep  22350  nrmr0reg  22351  flffbas  22597  cnflf  22604  cnflf2  22605  lmflf  22607  txflf  22608  fclsopni  22617  fclsnei  22621  fclsrest  22626  fcfnei  22637  cnfcf  22644  alexsubb  22648  alexsubALTlem3  22651  qustgplem  22723  tsmsfbas  22730  tsmsres  22746  tsmsf1o  22747  tsmsxplem1  22755  ustval  22805  isust  22806  ustincl  22810  ustdiag  22811  ustinvel  22812  ustexhalf  22813  ust0  22822  utopval  22835  ucnval  22880  isucn  22881  isucn2  22882  ucnima  22884  iscfilu  22891  ispsmet  22908  ismet  22927  isxmet  22928  imasdsf1olem  22977  imasf1oxmet  22979  imasf1omet  22980  metss  23112  met1stc  23125  prdsxmslem2  23133  txmetcnp  23151  metucn  23175  tngngp3  23259  nlmvscn  23290  nmoval  23318  nmolb  23320  qtopbaslem  23361  cncfval  23490  elcncf2  23492  mulc1cncf  23507  cncfmet  23510  evth  23557  lebnumlem3  23561  lebnum  23562  xlebnum  23563  ishtpy  23570  isphtpy  23579  pi1xfr  23653  pi1coghm  23659  isclmp  23695  ipcn  23843  lmmbr2  23856  lmmbr3  23857  lmmbrf  23859  cfilfval  23861  iscfil  23862  fmcfil  23869  caufval  23872  iscau  23873  iscau2  23874  iscau3  23875  iscau4  23876  iscauf  23877  caucfil  23880  cfilresi  23892  causs  23895  lmclim  23900  cmetcusp1  23950  minveclem4c  24022  minveclem2  24023  minveclem3b  24025  minveclem4  24029  minveclem6  24031  minveclem7  24032  ovolicc2lem3  24114  ismbl  24121  dyadmax  24193  dyadmbllem  24194  dyadmbl  24195  opnmbllem  24196  ismbf1  24219  ismbf  24223  mbfeqalem2  24237  mbflimsup  24261  mbfi1fseqlem6  24315  mbfi1flimlem  24317  itg2seq  24337  itg2monolem1  24345  isibl  24360  ply1divex  24724  fta1g  24755  dgrco  24859  plydivex  24880  fta1  24891  vieta1  24895  aannenlem1  24911  aannenlem2  24912  aalioulem2  24916  aalioulem3  24917  ulmval  24962  ulm2  24967  ulmi  24968  ulmres  24970  ulmshftlem  24971  ulmcaulem  24976  ulmcau  24977  ulmss  24979  ulmbdd  24980  ulmdvlem1  24982  ulmdvlem3  24984  pilem2  25034  pilem3  25035  cxpcn3  25323  dmarea  25529  rlimcnp  25537  scvxcvx  25557  lgamgulmlem2  25601  lgamgulmlem3  25602  lgamgulmlem5  25604  lgambdd  25608  lgamcvglem  25611  isppw2  25686  perfectlem2  25800  2sqlem6  25993  2sqlem10  25998  addsq2reu  26010  2sqreulem1  26016  2sqreunnlem1  26019  dchrisumlema  26058  dchrisumlem2  26060  dchrisumlem3  26061  pntpbnd  26158  pntibndlem3  26162  pntibnd  26163  pntleme  26178  pntlem3  26179  pntlemp  26180  pnt3  26182  istrkgld  26239  axtg5seg  26245  tgcgr4  26311  perpln1  26490  perpln2  26491  isperp  26492  brbtwn2  26685  colinearalg  26690  axsegconlem1  26697  axsegcon  26707  ax5seglem4  26712  ax5seglem5  26713  axlowdim  26741  axeuclidlem  26742  axcontlem1  26744  axcontlem2  26745  axcontlem4  26747  axcontlem5  26748  axcontlem8  26751  axcontlem12  26755  elntg2  26765  uvtxusgr  27178  rgrx0ndm  27369  ewlksfval  27377  wksfval  27385  wwlks  27607  wlkiswwlks2  27647  clwwlk  27755  1conngr  27967  frgrwopregasn  28089  frgrwopregbsn  28090  frgrwopreglem5ALT  28095  frgrregord013  28168  isgrpo  28268  isgrpoi  28269  grpoideu  28280  grpoidinv2  28286  vciOLD  28332  isvclem  28348  cnidOLD  28353  isnvlem  28381  nvi  28385  lnoval  28523  islno  28524  isblo3i  28572  blo3i  28573  blocnilem  28575  ajfval  28580  ubthlem1  28641  ubthlem2  28642  ubthlem3  28643  ubth  28644  minvecolem2  28646  minvecolem3  28647  minvecolem4c  28650  minvecolem4  28651  minvecolem5  28652  minvecolem6  28653  minvecolem7  28654  h2hcau  28750  h2hlm  28751  hilid  28932  hcau  28955  hlimi  28959  hlim2  28963  ocel  29052  adjsym  29604  ellnop  29629  ellnfn  29654  hhcno  29675  hhcnf  29676  lnopeq  29780  elunop2  29784  lnophm  29790  lnconi  29804  lnopcnbd  29807  lnfncnbd  29828  imaelshi  29829  riesz3i  29833  riesz4i  29834  riesz4  29835  riesz1  29836  cnlnadjlem2  29839  cnlnadjlem5  29842  cnlnadjlem8  29845  cnlnadji  29847  nmopadjlei  29859  cnvbraval  29881  leopg  29893  leoppos  29897  mdbr  30065  dmdbr  30070  cdj3i  30212  disjunsn  30338  funcnv5mpt  30407  fgreu  30411  fcnvgreu  30412  xrge0infss  30478  wrdt2ind  30622  resspos  30641  isomnd  30697  inftmrel  30804  isinftm  30805  archiabl  30822  isarchiofld  30885  0nellinds  30930  lindssn  30934  prmidl  30952  ismxidl  30966  crefeq  31104  esum2d  31347  sigaval  31365  issgon  31377  isrnmeas  31454  ismbfm  31505  isanmbfm  31509  mbfmcst  31512  elcarsg  31558  sitgval  31585  eulerpartlemd  31619  ballotleme  31749  tgoldbachgt  31929  bnj1185  32060  bnj1385  32099  bnj66  32127  bnj106  32135  bnj155  32146  bnj852  32188  bnj893  32195  bnj1228  32278  bnj1234  32280  bnj1463  32322  derangenlem  32413  subfacp1lem3  32424  subfacp1lem5  32426  subfacp1lem6  32427  subfacp1  32428  erdszelem8  32440  kur14  32458  cnpconn  32472  resconn  32488  cvmscbv  32500  iscvm  32501  cvmsi  32507  cvmsval  32508  cvmlift3lem2  32562  snmlval  32573  satfv1  32605  fmlasucdisj  32641  satffunlem1lem1  32644  satffunlem2lem1  32646  satfv1fvfmla1  32665  mclsssvlem  32804  mclsval  32805  mclsax  32811  mclsind  32812  dfpo2  32986  dfon2lem9  33031  dfrdg2  33035  dfrdg3  33036  frpomin  33073  poseq  33090  soseq  33091  frecseq123  33114  frrlem1  33118  frrlem13  33130  sltval  33149  noprefixmo  33197  nosupno  33198  nosupdm  33199  nosupfv  33201  nosupres  33202  nosupbnd1lem1  33203  nosupbnd1lem3  33205  nosupbnd1lem5  33207  noetalem5  33216  noeta  33217  nocvxminlem  33242  brsslt  33249  conway  33259  etasslt  33269  slerec  33272  fwddifnval  33619  nn0prpwlem  33665  isfne  33682  isfne4  33683  isfne2  33685  isfne3  33686  neibastop3  33705  topmeet  33707  topjoin  33708  filnetlem4  33724  unblimceq0lem  33840  unblimceq0  33841  unbdqndv2  33845  taupilemrplb  34595  csbwrecsg  34602  fin2so  34873  lindsadd  34879  matunitlindflem2  34883  ptrecube  34886  poimirlem2  34888  poimirlem3  34889  poimirlem4  34890  poimirlem24  34910  poimirlem25  34911  poimirlem26  34912  poimirlem27  34913  poimirlem28  34914  poimirlem29  34915  poimirlem30  34916  poimirlem32  34918  poimir  34919  heicant  34921  mblfinlem1  34923  mblfinlem2  34924  voliunnfl  34930  volsupnfl  34931  mbfresfi  34932  itg2addnc  34940  upixp  34998  indexdom  35003  filbcmb  35009  sdclem2  35011  fdc  35014  lmclim2  35027  caures  35029  istotbnd  35041  istotbnd3  35043  sstotbnd  35047  isbnd  35052  heibor  35093  bfp  35096  rrncmslem  35104  isgrpda  35227  idlval  35285  isidl  35286  0idl  35297  unichnidl  35303  pridl  35309  ismaxidl  35312  smprngopr  35324  igenval2  35338  prnc  35339  ispridlc  35342  scottexf  35440  scott0f  35441  riotasvd  36086  islfl  36190  eqlkr  36229  eqlkr3  36231  glbconN  36507  hlsuprexch  36511  ispsubsp  36875  ldilset  37239  isldil  37240  dilsetN  37283  isdilN  37284  trlset  37291  trlval  37292  cdleme27b  37498  cdleme29b  37505  cdleme31so  37509  cdleme31sn1  37511  cdleme31sn1c  37518  cdleme31fv  37520  cdleme40v  37599  istendo  37890  cdlemkid3N  38063  cdlemkid4  38064  cdlemkid5  38065  dihfval  38361  dihval  38362  islpolN  38613  hdmapffval  38956  hdmapfval  38957  hdmapval  38958  hdmapval2lem  38961  hgmapffval  39015  hgmapfval  39016  hgmapval  39017  hgmapvs  39021  qsalrel  39118  isnacs  39294  isnacs2  39296  nacsfix  39302  mzpclval  39315  elmzpcl  39316  rencldnfilem  39410  infmrgelbi  39468  pellfundre  39471  pellfundlb  39474  wepwsolem  39635  fnwe2lem2  39644  aomclem8  39654  dfac11  39655  gicabl  39692  islnr3  39708  hbtlem2  39717  hbtlem5  39721  fiinfi  39925  clsk1independent  40389  ntrclsk13  40414  gneispacess2  40489  imo72b2lem0  40509  imo72b2lem2  40511  imo72b2lem1  40514  imo72b2  40518  scottelrankd  40576  mnuop23d  40595  evth2f  41265  evthf  41277  fnchoice  41279  uzwo4  41308  wessf1ornlem  41437  disjinfi  41446  rnmptlb  41506  rnmptbdd  41508  rnmptbd2  41513  rnmptbd  41520  dstregt0  41539  upbdrech2  41567  fiminre2  41638  rexabslelem  41684  rexabsle  41685  uzub  41697  infrpgernmpt  41733  mccl  41871  ellimcabssub0  41890  climf  41895  clim2f  41909  limsupre  41914  clim2cf  41923  clim0cf  41927  climf2  41939  clim2f2  41943  clim2d  41946  limsupref  41958  limsupbnd1f  41959  climinf2  41980  limsuppnf  41984  climinfmpt  41988  climinf3  41989  limsupubuzmpt  41992  limsupmnf  41994  limsupre2lem  41997  limsupre2  41998  limsupmnfuzlem  41999  limsupmnfuz  42000  limsupre2mpt  42003  limsupre3lem  42005  limsupre3  42006  limsupre3mpt  42007  limsupre3uz  42009  limsupreuz  42010  limsupreuzmpt  42012  climuz  42017  liminfreuzlem  42075  liminfreuz  42076  cnrefiisplem  42102  xlimmnfvlem1  42105  xlimmnfv  42107  xlimpnfvlem1  42109  xlimpnfv  42111  xlimmnfmpt  42116  xlimpnfmpt  42117  cncfshift  42149  cncfperiod  42154  fperdvper  42195  dvbdfbdioo  42207  ioodvbdlimc1lem2  42209  ioodvbdlimc2lem  42211  dvnprodlem3  42225  stoweidlem5  42283  stoweidlem9  42287  stoweidlem15  42293  stoweidlem16  42294  stoweidlem27  42305  stoweidlem28  42306  stoweidlem31  42309  stoweidlem34  42312  stoweidlem37  42315  stoweidlem46  42324  stoweidlem48  42326  stoweidlem51  42329  stoweidlem52  42330  stoweidlem59  42337  wallispilem3  42345  stirlinglem13  42364  fourierdlem2  42387  fourierdlem3  42388  fourierdlem16  42401  fourierdlem20  42405  fourierdlem21  42406  fourierdlem22  42407  fourierdlem25  42410  fourierdlem39  42424  fourierdlem42  42427  fourierdlem54  42438  fourierdlem64  42448  fourierdlem77  42461  fourierdlem83  42467  fourierdlem103  42487  fourierdlem104  42488  subsaliuncllem  42633  iundjiun  42735  meaiunincf  42758  caragenval  42768  isome  42769  caragenel  42770  omessle  42773  ovnlerp  42837  hoidmvlelem3  42872  hoidmvle  42875  issmflem  42997  issmfgt  43026  smfmullem2  43060  smfmullem4  43062  smfmul  43063  smfsuplem2  43079  smfsup  43081  smfinflem  43084  smfinf  43085  cbvral2  43294  2reu8i  43305  2reuimp0  43306  dfdfat2  43320  iccpart  43569  iccpartigtl  43576  paireqne  43666  reupr  43677  perfectALTVlem2  43880  bgoldbachlt  43971  tgoldbachlt  43974  isomgreqve  43983  isomushgr  43984  isomuspgrlem2  43991  isomgrsym  43994  isomgrtr  43997  ushrisomgr  43999  upwlksfval  44003  mgmhmima  44062  nn0mnd  44079  lidlmsgrp  44190  lidlrng  44191  uzlidlring  44193  ply1mulgsumlem1  44433  ply1mulgsumlem2  44434  linindslinci  44496  lindslinindsimp1  44505  lindslinindsimp2lem5  44510  lindslinindsimp2  44511  linds0  44513  lindsrng01  44516  snlindsntor  44519  lmod1  44540  ldepsnlinc  44556  bigoval  44602  elbigo2r  44606  nn0sumshdiglem2  44675  eenglngeehlnmlem1  44717  eenglngeehlnmlem2  44718  setrec1lem2  44784