Theorem eleq1d 2849

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.) Allow shortening of eleq1 2852. (Revised by Wolf Lammen, 20-Nov-2019.)

Hypothesis

Ref	Expression
eleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eleq1d	⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Proof of Theorem eleq1d

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1d.1	. . . . 5 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqeq2d 2774	. . . 4 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
3	2	anbi1d 643	. . 3 ⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
4	3	exbidv 1956	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
5		dfclel 2840	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶))
6		dfclel 2840	. 2 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  eleq1  2852  eleq12d  2858  eqeltrd  2864  eqneltrd  2884  rspcimdv  3570  reuind  3714  sbcel2  4379  sbccsb2  4398  disjiun  5094  breq1  5109  breq2  5110  axrep6g  5246  inex1g  5283  intex  5309  pwexg  5344  reusv2lem4  5367  reusv2  5369  reusv3  5371  rabxfrd  5383  prexOLD  5405  opelopabsb  5508  csbmpt12  5536  pofun  5581  seex  5614  seinxp  5740  opabid2  5811  opeliunxp2  5820  elrn2g  5878  opeldmd  5894  opeldm  5895  elreldm  5923  elsnres  6021  iss  6038  unielrel  6291  onunel  6485  funopg  6591  brprcneu  6895  brprcneuALT  6896  tz6.12f  6930  ndmfvrcl  6938  ssimaex  6990  dmfco  7001  fvmpti  7012  fvmpt3  7018  fvmptf  7035  fvmptss2  7040  respreima  7086  fvn0ssdmfun  7095  fvelrn  7097  ffnfvf  7141  ffvresb  7147  fmptco  7151  fmptcof  7152  fsn  7157  fsn2g  7160  fressnfv  7185  fvrnressn  7186  fnex  7243  funfvima  7256  funfvima3  7262  f1mpt  7285  fliftfuns  7342  isoselem  7369  isowe2  7378  riotaclb  7438  ovrspc2v  7466  ffnov  7566  fovcld  7567  ovmpos  7589  ov2gf  7590  ovg  7606  funimassov  7619  oprssdm  7623  ndmovrcl  7628  caovclg  7634  elovmpo  7687  ofmpteq  7737  sorpsscmpl  7771  uniexg  7778  abnexg  7791  difsnexi  7796  onint  7825  limsuc  7881  tfisi  7891  peano5  7926  xpexr  7951  xpexcnv  7953  fnexALT  7984  focdmex  7989  f1stres  8046  f2ndres  8047  xp1st  8054  xp2nd  8055  unielxp  8060  opiota  8092  fmpox  8100  offval22  8121  f1od2  8132  frxp  8162  fnse  8174  frxp2  8185  sexp2  8187  frxp3  8192  sexp3  8194  opeliunxp2f  8252  dftpos4  8287  fvmpocurryd  8313  undefnel2  8320  onnseq  8377  smoel  8393  smo11  8397  tfrlem8  8417  tfrlem9  8418  tfrlem15  8425  tfr2b  8429  tz7.44-2  8440  tz7.44-3  8441  oacl  8568  omcl  8569  oecl  8570  oaord1  8584  omordi  8599  oen0  8620  oeeui  8636  nnacl  8645  nnmcl  8646  nnecl  8647  nnmordi  8665  nnaordex  8672  omsmolem  8691  naddcllem  8710  naddov2  8713  naddf  8716  naddssim  8720  naddelim  8721  naddasslem1  8729  naddasslem2  8730  naddsuc2  8736  erexb  8768  elecex  8793  qliftfuns  8850  ixpsnval  8953  elixp2  8954  resixp  8986  undifixp  8987  mptelixpg  8988  resixpfo  8989  elixpsn  8990  fundmen  9084  fopwdom  9129  disjen  9178  xpf1o  9183  unfi  9211  cnvfi  9216  fnfi  9218  f1oenfirn  9220  f1domfi  9221  fissorduni  9307  unblem2  9310  pwfi  9335  fiint  9343  iunfi  9357  tfsnfin2  9377  isfsupp  9382  fsuppun  9403  ffsuppbi  9414  elfi2  9430  wdom2d  9598  ixpiunwdom  9608  dfom3  9672  cantnfvalf  9690  cantnflt  9697  cantnflem1  9714  r1fin  9804  tz9.12lem3  9820  ranksnb  9861  ranklim  9882  r1pw  9883  r1pwALT  9884  r1pwcl  9885  rankuni2b  9891  elhf2g  9935  hfunOLD  9943  djuexb  10014  cardmin2  10104  infxpenc2lem1  10122  dfac8alem  10132  dfac8clem  10135  ac5num  10139  acni2  10149  acnlem  10151  alephon  10172  alephfplem3  10209  alephfplem4  10210  dfac4  10225  dfac5lem1  10226  dfac5lem5  10230  dfac2a  10232  dfac2b  10233  dfacacn  10244  dfac12lem2  10247  dfac12r  10249  dfac12k  10250  cofsmo  10371  cfsmolem  10372  isfin1a  10394  fin1ai  10395  isfin3  10398  infpssrlem3  10407  fin23lem7  10418  fin23lem11  10419  enfin2i  10423  isf34lem4  10479  fin1a2lem7  10508  hsmexlem9  10527  hsmexlem4  10531  hsmex  10534  axcc2lem  10538  axcc3  10540  axdc3lem2  10553  axcclem  10559  zornn0g  10607  ttukeylem3  10613  ttukeylem6  10616  ttukey2g  10618  brdom7disj  10634  brdom6disj  10635  fnct  10644  fnctOLD  10645  konigthlem  10677  axregndlem2  10712  axinfnd  10715  axacndlem5  10720  axacnd  10721  fpwwe2lem4  10743  fpwwe2lem12  10751  fpwwe  10755  pwfseqlem1  10767  pwfseqlem3  10769  pwfseqlem4a  10770  pwfseqlem4  10771  wununi  10815  wunpw  10816  wunpr  10818  wunr1om  10828  tskpw  10862  tskr1om  10876  inar1  10884  grupw  10904  grupr  10906  gruurn  10907  gruiun  10908  ingru  10924  grur1a  10928  grothomex  10938  grothac  10939  addnidpi  11010  indpi  11016  adderpq  11065  mulerpq  11066  addclprlem2  11126  mulclprlem  11128  distrlem4pr  11135  prlem934  11142  ltexprlem3  11147  ltexprlem4  11148  ltexprlem7  11151  ltexpri  11152  prlem936  11156  reclem2pr  11157  reclem3pr  11158  addclsr  11192  mulclsr  11193  supsrlem  11220  supsr  11221  axaddf  11254  axmulf  11255  axaddrcl  11261  axmulrcl  11263  renegcl  11645  negreb  11647  negn0  11769  negf1o  11770  ltord1  11866  leord1  11867  eqord1  11868  ltord2  11869  leord2  11870  eqord2  11871  negfi  12290  infm3  12300  cju  12340  indfval  12351  peano5nni  12362  peano2nn  12371  dfnn2  12372  nn1m1nn  12380  nnaddcl  12382  nnmulcl  12383  nnsub  12406  nndivtr  12409  un0addcl  12663  un0mulcl  12664  elnnnn0  12673  nn0sub  12680  fcdmnn0fsuppg  12690  elz  12719  nnnegz  12720  elz2  12735  znegclb  12757  zaddcl  12760  nzadd  12768  zmulcl  12769  zneo  12806  nneo  12807  zeo  12809  peano5uzi  12812  zindd  12824  uzp1  13026  uzaddcl  13055  ublbneg  13084  eqreznegel  13085  supminf  13086  zsupss  13088  qmulz  13102  qnegcl  13118  irradd  13125  irrmul  13126  xnn0xaddcl  13389  fzrev2  13746  injresinjlem  13949  negmod0  14042  om2uzuzi  14116  uzindi  14149  fsuppmapnn0ub  14162  mptnn0fsuppr  14166  seqexw  14184  seqcl2  14187  seqcl  14189  seqf  14190  monoord  14199  monoord2  14200  sermono  14201  seqsplit  14202  seqcaopr2  14205  seqid3  14213  seqhomo  14216  expcllem  14239  expcl2lem  14240  m1expcl2  14252  faccl  14451  facdiv  14455  facndiv  14456  bccmpl  14477  bccl  14490  hashclb  14526  hasheq0  14531  hashfn  14543  seqcoll  14633  opfi1uzind  14680  ccatalpha  14764  reuccatpfxs1lem  14920  reuccatpfxs1  14921  repswccat  14962  repswrevw  14963  2cshw  14989  2cshwcshw  15001  cshimadifsn  15005  cshco  15012  swrd2lsw  15131  wwlktovf  15135  wwlktovf1  15136  wwlktovfo  15137  wrd2f1tovbij  15139  shftlem  15247  shftf  15258  cjval  15295  cjth  15296  remim  15310  cnpart  15433  uzin2  15538  caubnd2  15551  sqreulem  15553  clim  15687  clim2  15697  lo1o12  15726  climrlim2  15740  lo1resb  15757  o1resb  15759  lo1eq  15761  climmpt2  15766  climshftlem  15767  rlimcld2  15771  climcn1  15785  climcn2  15786  o1dif  15823  iserex  15850  climub  15855  climserle  15856  isercoll  15861  climcau  15864  caurcvg2  15871  caucvgb  15873  summolem3  15906  summolem2a  15907  zsum  15910  fsum  15912  sumss2  15918  fsumcvg2  15919  fsumclf  15930  fsumsplitf  15934  fsumsplit1  15937  sumpr  15940  sumtp  15941  fsumm1  15943  fsum1p  15945  isummulc2  15954  fsum2dlem  15962  fsumcom2  15966  fsumshftm  15973  fsum0diag2  15975  fsumge1  15990  fsum00  15991  fsumabs  15994  telfsumo  15995  telfsumo2  15996  fsumparts  15999  fsumrlim  16004  fsumo1  16005  o1fsum  16006  fsumiun  16014  binomlem  16024  isumshft  16034  isum1p  16036  isumrpcl  16038  climcndslem1  16044  climcndslem2  16045  climcnds  16046  infcvgaux2i  16053  cvgrat  16078  mertens  16081  clim2prod  16083  prodfn0  16089  prodfrec  16090  prodfdiv  16091  ntrivcvgfvn0  16094  prodmolem3  16126  prodmolem2a  16127  zprod  16130  fprod  16134  prodss  16140  fprodser  16142  fprodm1  16160  fprod1p  16161  fprodm1s  16163  fprodp1s  16164  fprodabs  16167  fprodn0  16172  fprod2dlem  16173  fprodcnv  16176  fprodcom2  16177  fproddivf  16180  fprodsplitf  16181  fprodsplit1f  16183  bpolycl  16244  fprodefsum  16287  rpnnen2lem11  16418  mod2eq1n2dvds  16543  mulsucdiv2z  16549  zob  16555  nn0o1gt2  16577  nno  16578  nn0o  16579  divalglem7  16595  bitsf1  16642  sadcp1  16651  smupp1  16676  qnumdencl  16941  iserodd  17039  pcqcl  17060  pcxnn0cl  17064  pcxcl  17065  pcgcd1  17081  dvdsprmpweqle  17090  pcmpt  17096  pcmpt2  17097  pcmptdvds  17098  infpnlem2  17115  infpn2  17117  1arith  17131  elgz  17135  mul4sq  17158  4sqlem13  17161  4sqlem17  17165  4sqlem18  17166  4sqlem19  17167  vdwlem1  17185  vdwlem2  17186  vdwnn  17202  ramtcl2  17215  ramcl  17233  prmonn2  17243  prmodvdslcmf  17251  isstruct2  17353  wunress  17453  firest  17629  imasaddfnlem  17726  imasvscafn  17735  xpsfrnel2  17762  mreintcl  17791  ismred2  17799  mreexexlemd  17844  mreexexlem3d  17846  mreexexlem4d  17847  iscatd2  17881  catpropd  17909  subsubc  18054  isfunc  18065  inclfusubc  18144  fncnvimaeqv  18320  joindef  18574  joinval  18575  meetdef  18588  meetval  18589  oduclatb  18707  acsdrsel  18743  isacs4lem  18744  isacs5lem  18745  acsdrscl  18746  mgmsscl  18847  mgmn0plusgf  18853  mgmpropd  18855  mgm1  18862  gsumvalx  18891  issubmgm  18917  issubmgm2  18918  mgmhmima  18930  sgrppropd  18946  mndpropd  18977  issubm  19024  0subm  19039  insubm  19040  mhmimalem  19046  gsumwsubmcl  19059  gsumwspan  19068  symggrplem  19106  sursubmefmnd  19118  injsubmefmnd  19119  smndex1basss  19130  degenmgm  19163  degenmgm2nfun  19165  degenmgm2  19166  mulgsubcl  19324  issubg  19362  issubg2  19378  issubg4  19382  0subg  19388  isnsg  19391  isnsg2  19392  nsgbi  19393  isnsg3  19396  elnmz  19399  nmzbi  19400  nmzsubg  19401  eqgval  19415  eqgid  19418  cycsubgcl  19447  ghmrn  19469  ghmnsgima  19480  gass  19542  oppgsubg  19604  f1omvdconj  19687  symgfisg  19709  psgneldm  19744  0subgALT  19809  odhash3  19817  sylow2blem2  19862  lsmsubm  19894  lsmsubg  19895  efgsf  19970  efgsdm  19971  efgs1b  19977  efgredlema  19981  eqgabl  20075  ablnsg  20088  cyggenod2  20126  gsumzaddlem  20162  gsummhm2  20180  gsum2dlem2  20212  gsum2d2lem  20214  gsumcom2  20216  dprdfeq0  20265  dprdsubg  20267  dprd2da  20285  ablfacrp  20309  pgpfac1lem3  20320  pgpfaclem1  20324  ablfaclem3  20330  ablfac2  20332  cycsubggenodd  20352  isrng  20403  issrg  20441  srgfcl  20449  rglcom4d  20464  srgbinomlem4  20482  isring  20490  iscrng  20493  dvdsr  20619  irredrmul  20684  isrngim  20702  isrim0  20740  issubrng  20826  subrngringnsg  20832  issubrng2  20837  rhmimasubrnglem  20844  issubrg  20850  issubrg2  20871  subrgpropd  20887  isdrngd  21049  isdrngdOLD  21051  issdrg  21072  sdrgacs  21085  issrngd  21139  islmod  21166  lmodlema  21167  islmodd  21168  lmodprop2d  21226  rmodislmodlem  21231  rmodislmod  21232  lssset  21235  islssd  21237  lsscl  21244  lsslss  21263  lsspropd  21319  lmhmima  21349  lbsind  21382  lsmcl  21385  islvec  21406  lmhmlvec  21412  lspsolvlem  21447  lspsolv  21448  lvecpropd  21472  rnglidlmcl  21522  rnglidl0  21536  rnglidlmmgm  21560  df2idl2crng  21604  rngqiprngimf1lem  21617  rngqiprngimf1  21623  ring2idlqus  21632  prmidlval  21645  prmidlc  21656  prmidlprop  21659  xrsdsreclblem  21746  xrsdsreclb  21747  cnsubrglem  21750  prmirred  21807  pzriprnglem4  21817  pzriprnglem8  21821  pzriprngALT  21828  znunithash  21897  cofipsgn  21926  zrhpsgnelbas  21927  rzgrp  21956  isphl  21961  phllmhm  21965  ipcl  21966  isphld  21987  phlpropd  21988  phlssphl  21992  cssincl  22021  pjdm  22040  dsmmval  22067  dsmmbas2  22070  dsmmelbas  22072  frlmbas  22088  frlmup1  22131  lindfind  22149  lindsind  22150  f1lindf  22155  islindf4  22171  lindsenlbs  22184  psrbag  22252  psrbaglefi  22261  mplsubglem  22333  mpllsslem  22334  ltbwe  22380  psrbagsn  22399  subrgasclcl  22403  mplind  22406  mpfind  22451  psdmul  22514  coe1mul2lem2  22614  gsumply1eq  22654  evl1vsd  22689  mpfpf1  22696  pf1mpf  22697  pf1ind  22700  matecl  22767  m1detdiag  22939  mdetralt  22950  mdetralt2  22951  mdetunilem2  22955  mdetunilem9  22962  m2detleiblem3  22971  m2detleiblem4  22972  smadiadetlem0  23003  cpmatacl  23061  chpscmat  23187  uniopn  23242  inopn  23244  fiinopn  23246  istps  23279  fctop  23349  iscld  23372  isopn2  23377  mretopd  23437  iscldtop  23440  perfi  23500  tgrest  23504  restcld  23517  ordtbaslem  23533  ordtrest2lem  23548  ordtrest2  23549  iscn  23580  cnpval  23581  iscnp  23582  tgcn  23597  subbascn  23599  ssidcn  23600  lmbrf  23605  cnpnei  23609  cnima  23610  iscncl  23614  cnconst2  23628  cnrest2  23631  cnpresti  23633  cnprest  23634  cnindis  23637  lmres  23645  lmcnp  23649  iscnrm  23668  t1sncld  23671  cnrmi  23705  cncmp  23737  cmpsublem  23744  fiuncmp  23749  unconn  23774  conncompid  23776  conncompconn  23777  conncompss  23778  1stcfb  23790  2ndcrest  23799  2ndcctbss  23801  2ndcdisj  23802  1stccnp  23808  islly  23814  isnlly  23815  subislly  23827  restnlly  23828  restlly  23829  islly2  23830  hausllycmp  23840  cldllycmp  23841  dislly  23843  isptfin  23862  islocfin  23863  ptfinfin  23865  finlocfin  23866  dissnlocfin  23875  locfindis  23876  comppfsc  23878  kgenval  23881  elkgen  23882  kgeni  23883  cmpkgen  23897  1stckgenlem  23899  kgencn2  23903  ptpjpre1  23917  elpt  23918  elptr  23919  ptbasin  23923  xkobval  23932  xkoval  23933  xkoopn  23935  txbasval  23952  tx1cn  23955  tx2cn  23956  dfac14  23964  xkoccn  23965  txcnp  23966  ptcnplem  23967  txcnmpt  23970  txindislem  23979  txdis1cn  23981  txlly  23982  txnlly  23983  pthaus  23984  ptrescn  23985  hauseqlcld  23992  txlm  23994  tx2ndc  23997  txkgen  23998  xkoptsub  24000  xkopt  24001  xkoco1cn  24003  xkoco2cn  24004  xkococnlem  24005  xkococn  24006  cnmpt11  24009  cnmpt12  24013  cnmpt21  24017  cnmpt22  24020  cnmptkp  24026  cnmptk1p  24031  xkoinjcn  24033  txconn  24035  qtopval2  24042  elqtop  24043  idqtop  24052  qtopcld  24059  qtopeu  24062  qtoprest  24063  qtopomap  24064  qtopcmap  24065  ishmeo  24105  hmeoopn  24112  hmeocld  24113  ordthmeolem  24147  ptcmpfi  24159  elmptrab  24173  fgcl  24224  trfil2  24233  cfinfil  24239  uzrest  24243  ufilss  24251  trufil  24256  cfinufil  24274  ufinffr  24275  ufildr  24277  rnelfm  24299  flfcntr  24389  ptcmplem2  24399  ptcmplem3  24400  ptcmplem4  24401  ptcmplem5  24402  cnextfvval  24411  tmdcn2  24435  tmdmulg  24438  tmdgsum2  24442  symgtgp  24452  opnsubg  24454  clssubg  24455  tgpconncompeqg  24458  ghmcnp  24461  tgphaus  24463  tgpt0  24465  qustgpopn  24466  qustgplem  24467  tsmsgsum  24485  tsmssubm  24489  tsmsres  24490  tsmsf1o  24491  tsmsxplem1  24499  tsmsxplem2  24500  tsmsxp  24501  istrg  24510  istdrg  24512  istdrg2  24524  istlm  24531  istvc  24538  ustval  24549  ustincl  24554  ustdiag  24555  ustinvel  24556  ustexhalf  24557  ust0  24566  ucnima  24626  fmucndlem  24636  prdsdsf  24713  prdsxmet  24715  imasf1oxmet  24721  imasf1omet  24722  prdsxmslem2  24875  metustsym  24901  isnlm  25021  qtopbaslem  25104  xrtgioo  25153  reperflem  25165  fsumcn  25218  expcn  25220  xrhmeo  25294  cnllycmp  25304  bndth  25306  isclm  25412  lmhmclm  25435  lmmcvg  25609  fmcfil  25620  iscfil3  25621  iscau2  25625  iscau4  25627  iscmet3lem1  25639  iscmet3  25641  cfilres  25644  caussi  25645  equivcfil  25647  flimcfil  25662  bcthlem1  25672  isbn  25686  srabn  25708  ishl2  25718  cmslssbn  25720  cmscsscms  25721  minveclem3b  25776  ivthlem1  25799  ivthlem2  25800  ivthlem3  25801  ivth2  25803  ivthle  25804  ivthle2  25805  ivthicc  25806  ovolficcss  25817  ovolunlem1a  25844  ovolunlem1  25845  ovolfiniun  25849  ovoliunlem1  25850  ovoliunlem3  25852  ovoliun  25853  ovoliun2  25854  shft2rab  25856  ovolshftlem1  25857  sca2rab  25860  ovolscalem1  25861  mblsplit  25880  finiunmbl  25892  volun  25893  volfiniun  25895  voliunlem1  25898  voliunlem3  25900  iunmbl  25901  voliun  25902  volsup  25904  ioombl  25913  ioorcl  25925  vitalilem1  25956  vitalilem2  25957  vitalilem3  25958  vitalilem4  25959  vitali  25961  ismbf1  25972  mbfdm  25974  ismbf  25976  ismbfcn  25977  mbfima  25978  mbfimaicc  25979  ismbfcn2  25986  ismbfd  25987  ismbf2d  25988  mbfeqalem1  25989  mbfmax  25997  mbfposr  26000  mbfposb  26001  ismbf3d  26002  mbfimaopnlem  26003  mbfimaopn2  26005  cncombf  26006  isi1f  26022  i1fd  26029  itg1mulc  26052  mbfi1fseqlem4  26066  itg2lcl  26075  isibl  26113  iblitg  26116  iblcnlem1  26135  iblcnlem  26136  iblrelem  26138  iblpos  26140  itgeqa  26161  itgfsum  26174  itgabs  26182  limcvallem  26218  ellimc  26220  ellimc2  26224  limcmpt  26230  cnmptlimc  26237  dvbsss  26249  cpnfval  26279  elcpn  26281  dvmptfsum  26322  dvle  26354  dvfsumle  26368  dvfsumge  26369  dvfsumabs  26370  dvfsumrlimf  26372  dvfsumlem1  26373  dvfsumlem2  26374  dvfsumlem3  26375  dvfsumlem4  26376  dvfsumrlimge0  26377  dvfsumrlim  26378  dvfsumrlim2  26379  dvfsum2  26381  itgsubstlem  26395  itgsubst  26396  mdegcl  26414  deg1nn0clb  26435  isuc1p  26486  plyeq0lem  26556  plyco  26587  plycj  26623  dvply2g  26633  dvnply2  26635  plydivlem4  26644  fta1lem  26655  fta1  26656  rnplynfin  26657  elqaalem1  26669  elqaalem2  26670  elqaalem3  26671  elqaa  26672  ulmcau  26749  radcnv0  26770  radcnvlt1  26772  radcnvle  26774  pserdvlem2  26782  coseq1  26880  efeq1  26883  sinord  26889  efif1olem2  26898  efif1olem4  26900  lognegb  26945  logcj  26961  argimgt0  26967  logtayl  27015  2irrexpq  27086  root1eq1  27110  logrec  27118  2irrexpqALT  27155  angrteqvd  27161  angpieqvdlem  27183  atans  27285  atans2  27286  dmarea  27312  areambl  27313  rlimcnp  27320  rlimcnp2  27321  xrlimcnp  27323  harmonicbnd  27358  harmonicbnd2  27359  lgamcvglem  27394  wilthlem2  27423  wilth  27425  efnnfsumcl  27457  vmacl  27472  efvmacl  27474  efchtdvds  27513  sqff1o  27536  fsumdvdscom  27539  musumsum  27546  fsumdvdsmul  27549  fsumvma  27567  perfect  27585  dchrelbasd  27593  lgsval  27655  lgsval2lem  27661  lgsdir2lem4  27682  lgsdir2  27684  lgsqrlem1  27700  lgsdchr  27709  m1lgs  27742  2lgs  27761  mul2sq  27773  2sqlem6  27777  2sqblem  27785  2sq2  27787  rplogsumlem2  27839  dchrisumlema  27842  dchrisumlem2  27844  dchrisumlem3  27845  dchrvmasumlem2  27852  dchrvmasumlem3  27853  dchrisum0flblem2  27863  dchrisum0flb  27864  dchrisum0fno1  27865  ostthlem1  27981  nodmon  28034  noextendseq  28051  nodense  28076  madefi  28326  addsproplem1  28382  addsproplem3  28384  addsprop  28389  addsf  28395  addbdaylem  28430  negsproplem1  28441  negsproplem3  28443  negsprop  28448  negbdaylem  28469  mulsproplemcbv  28528  mulsproplem1  28529  mulsproplem10  28538  mulsprop  28543  addonbday  28692  noseqp1  28704  noseqind  28705  peano5n0s  28732  dfn0s2  28745  n0addscl  28757  n0mulscl  28758  n0bday  28765  onsfi  28769  n0s0m1  28775  n0subs  28776  n0p1nns  28784  dfnns2  28785  nn1m1nns  28787  oldfib  28790  zaddscl  28807  zmulscld  28810  elzn0s  28811  peano5uzs  28817  expscllem  28843  z12addscl  28890  z12shalf  28893  z12negsclb  28894  z12zsodd  28895  z12bdaylem  28897  z12bday  28898  bdayfin  28900  mirval  29154  perpneq  29216  isperp2  29217  isperp2d  29218  foot  29224  islnopp  29242  islnoppd  29243  outpasch  29260  hlpasch  29261  ishpg  29264  colopp  29274  colhp  29275  lmif  29317  islmib  29319  lmiinv  29324  trgcopy  29338  trgcopyeu  29340  acopyeu  29369  inaghl  29391  tgasa1  29430  f1otrgitv  29474  f1otrg  29475  isfusgr  29926  opfusgr  29931  fusgrfisbase  29936  fusgrfisstep  29937  nbupgrel  29953  nbumgrvtx  29954  nbusgreledg  29961  edgnbusgreu  29975  nb3grprlem1  29988  uvtxusgrel  30011  cusgredg  30032  cplgr2vpr  30041  cusgrexg  30052  usgredgsscusgredg  30067  fusgrn0degnn0  30107  rusgrnumwrdl2  30194  rgrx0ndm  30201  wlkcomp  30238  wlkdlem2  30289  clwlkcomp  30393  iswwlks  30452  wwlknllvtx  30462  0enwwlksnge1  30480  wlkiswwlks2lem5  30489  wwlksm1edg  30497  wwlksnred  30508  wwlksnext  30509  wwlksnextbi  30510  wwlksnredwwlkn  30511  wwlksnextfun  30514  wwlksnextinj  30515  wwlksnextsurj  30516  wwlksnextbij  30518  wwlksnfi  30522  wwlksnextproplem2  30526  wwlksnextprop  30528  2wlkdlem4  30544  rusgrnumwwlkl1  30587  rusgrnumwwlks  30593  isclwwlk  30602  clwwlk1loop  30606  clwwlkccatlem  30607  clwlkclwwlklem2a1  30610  clwlkclwwlklem2a4  30615  clwlkclwwlklem2a  30616  clwlkclwwlklem2  30618  clwlkclwwlklem3  30619  clwlkclwwlk  30620  clwlkclwwlk2  30621  clwwisshclwwslemlem  30631  clwwisshclwwslem  30632  clwwisshclwws  30633  clwwlknlbonbgr1  30657  clwwlkinwwlk  30658  clwwlkn1  30659  loopclwwlkn1b  30660  clwwlkn1loopb  30661  clwwlkn2  30662  clwwlkel  30664  clwwlkf  30665  clwwlkwwlksb  30672  clwwlkext2edg  30674  wwlksext2clwwlk  30675  wwlksubclwwlk  30676  eleclclwwlknlem2  30679  umgr2cwwk2dif  30682  s2elclwwlknon2  30722  clwwlknonwwlknonb  30724  clwwlknonex2lem2  30726  clwwlknonex2  30727  loop1cycl  30771  3wlkdlem4  30790  upgr3v3e3cycl  30808  upgr4cycl4dv4e  30813  eupth2lem2  30847  eulerpathpr  30868  1vwmgr  30904  3vfriswmgrlem  30905  3vfriswmgr  30906  3cyclfrgrrn1  30913  vdgn1frgrv2  30924  frgrncvvdeqlem3  30929  frgrncvvdeqlem8  30934  frgrncvvdeqlem9  30935  frgrwopregasn  30944  frgrwopregbsn  30945  frgrwopreglem5ALT  30950  frgr2wwlk1  30957  frgr2wwlkeqm  30959  fusgr2wsp2nb  30962  2clwwlk2clwwlklem  30974  extwwlkfabel  30981  nvvop  31238  isnvlem  31239  sspval  31352  nmorepnf  31397  phpar  31453  siilem2  31481  bnsscmcl  31497  ubthlem1  31499  shaddcl  31846  shmulcl  31847  hsn0elch  31877  hhssablo  31892  hhssnvt  31894  hhsssh  31898  shscl  31947  shintcl  31959  chintcl  31961  shincl  32010  chincl  32128  h1datomi  32210  chscllem2  32267  sumspansn  32278  spansncvi  32281  5oalem2  32284  5oalem3  32285  pjini  32328  pjjsi  32329  eigposi  32465  nmoprepnf  32496  nmfnrepnf  32509  dmadjrnb  32535  lnophmlem1  32645  lnophm  32648  nmcopex  32658  lnconi  32662  nmbdfnlb  32679  nmcfnex  32682  imaelshi  32687  rnbra  32736  leopg  32751  pjbdlni  32778  pjhmop  32779  hmopidmch  32782  pjclem4  32828  pj3si  32836  strlem1  32879  atssma  33007  atcv0eq  33008  atcv1  33009  atomli  33011  atcvatlem  33014  cdj3lem2a  33065  cdj3lem3a  33068  inagbtwn  33075  inagcgratrgn  33085  tgextahpl  33096  tgextancgra  33101  xppreima  33308  fmptcof2  33320  aciunf1lem  33325  funcnv4mpt  33331  1stpreimas  33367  fpwrelmapffslem  33391  xrofsup  33426  fzspl  33448  fzsplit3  33452  nnindf  33478  fprodex01  33483  fsumiunle  33487  indf1ofs  33500  gsumhashmul  33695  fzto1st  33731  fxpsubm  33800  fxpsubg  33801  fxpsubrg  33802  isslmd  33830  slmdlema  33831  elrgspnlem2  33871  elrgspnlem4  33873  rlocisunit  33904  subsdrg  33927  qusker  33977  0nellinds  33993  unitprodclb  34011  nsgmgclem  34029  nsgmgc  34030  nsgqusf1olem2  34032  elrspunidl  34045  opprlidlabs  34076  dfufd2lem  34148  psrbasfsupp  34210  selvply1rhmlemb  34218  mplidomlem  34226  lindsunlem  34323  brfldext  34344  brfinext  34351  finextfldext  34363  finexttrb  34364  extdg1id  34365  fldextrspunlsplem  34372  constrconj  34444  constrfin  34445  trisecnconstr  34491  smatrcl  34495  submateq  34508  lmatfval  34513  lmatcl  34515  qtophaus  34535  locfinreflem  34539  locfinref  34540  zartopn  34574  zarcmplem  34580  rhmpreimacnlem  34583  xpinpreima  34605  xpinpreima2  34606  cnre2csqlem  34609  tpr2rico  34611  prsdm  34613  prsrn  34614  ordtrest2NEWlem  34621  ordtrest2NEW  34622  zrhcntr  34678  qqhval2  34681  isrrext  34699  ismntoplly  34724  esumcvg  34785  sigaval  34810  issiga  34811  0elsiga  34813  sigaclcu  34816  issgon  34822  prsiga  34830  sigaclci  34831  difunielsiga  34832  unelsiga  34833  ispisys2  34853  inelpisys  34854  unelldsys  34858  sigapildsyslem  34861  sigapildsys  34862  ldgenpisyslem1  34863  ldgenpisys  34866  isros  34868  unelros  34871  difelros  34872  fiunelros  34874  inelsros  34878  diffiunisros  34879  rossros  34880  measvuni  34914  measiun  34918  voliune  34929  volfiniune  34930  brfae  34948  ismbfm  34951  mbfmcnvima  34955  mbfmcst  34958  1stmbfm  34959  2ndmbfm  34960  imambfm  34961  sitgval  35031  issibf  35032  sibfima  35037  sitgfval  35040  sitgclg  35041  eulerpartlemelr  35056  eulerpartlemsf  35058  eulerpartleme  35062  eulerpartlemt0  35068  eulerpartlemt  35070  eulerpartgbij  35071  eulerpartlemr  35073  eulerpartlemmf  35074  eulerpartlemgvv  35075  eulerpartlemgs2  35079  eulerpartlemn  35080  eulerpart  35081  cndprobprob  35137  rrvsum  35153  orvcelel  35169  ballotlemodife  35197  ballotlemsdom  35211  ballotlemrv  35219  ballotlemrv1  35220  ballotlemrv2  35221  ballotlem1ri  35234  fsum2dsub  35303  reprinfz1  35318  reprpmtf1o  35322  reprdifc  35323  breprexplema  35326  hgt750lema  35353  hgt750leme  35354  bnj149  35572  bnj222  35580  bnj1112  35680  bnj1148  35693  f1preimaex  35782  soinfdom  35797  rankse  35822  fineqvrep  35881  fineqvnttrclse  35891  fineqvinfep  35892  kardnnfi  35936  gblacfnacd  36028  vonf1wev  36035  vonf1owevOLD  36037  vonf1osev  36039  vonf1oonfo  36048  subfacp1lem3  36113  subfacp1lem6  36116  erdszelem10  36131  kur14  36147  cvxsconn  36174  cnllysconn  36176  resconn  36177  iscvm  36190  cvmliftlem5  36220  cvmliftlem15  36229  cvmlift2lem1  36233  cvmlift2lem12  36245  cvmlift2lem13  36246  sat1el2xp  36310  fmlasuc  36317  gonan0  36323  gonar  36326  satefvfmla0  36349  msubrn  36460  msubco  36462  ismfs  36480  mvtinf  36486  mclsax  36500  mppspstlem  36502  elmpps  36504  nnuni  36669  dfdm5  36714  dfrn5  36715  elima4  36717  rdgprc0  36732  pprodss4v  36823  elfuns  36854  fnimage  36868  imageval  36869  fwddifval  37104  fwddifnval  37105  fwddifnp1  37107  hfninf  37112  nmulprop  37116  filnetlem4  37346  onsucconn  37403  onsucsuccmp  37409  limsucncmp  37411  onint1  37414  fveleq  37416  findreccl  37418  nndivsub  37422  weiunse  37433  mh-inf3f1  37506  mh-infprim2bi  37512  mh-infprim3bi  37513  bj-seex  38011  bj-adjg1  38133  bj-mooreset  38213  bj-ismoored0  38217  bj-ismoored  38218  bj-inftyexpitaudisj  38317  bj-inftyexpidisj  38322  bj-isvec  38399  bj-isclm  38403  csbmpo123  38445  topdifinffinlem  38461  topdifinffin  38462  csbfinxpg  38502  phpreu  38718  finixpnum  38719  poimirlem16  38745  poimirlem17  38746  poimirlem19  38748  poimirlem20  38749  poimirlem22  38751  poimirlem23  38752  poimirlem24  38753  poimirlem25  38754  poimirlem26  38755  poimirlem28  38757  poimirlem29  38758  poimirlem30  38759  poimirlem31  38760  poimirlem32  38761  poimir  38762  mblfinlem3  38768  ex-ovoliunnfl  38772  voliunnfl  38773  volsupnfl  38774  mbfresfi  38775  itgabsnc  38798  ftc1anclem6  38807  ftc1anclem7  38808  ftc1anclem8  38809  ftc1anc  38810  dvasin  38813  sdclem2  38867  fdc  38870  incsequz  38873  neificl  38878  mettrifi  38882  cntotbnd  38921  cnpwstotbnd  38922  ismtyima  38928  ismtyhmeolem  38929  heiborlem2  38937  heiborlem3  38938  heiborlem4  38939  heiborlem5  38940  heiborlem6  38941  heiborlem10  38945  isrngo  39022  isdivrngo  39075  drngoi  39076  idlval  39138  isidlc  39140  idladdcl  39144  idllmulcl  39145  idlrmulcl  39146  0idl  39150  pridlval  39158  smprngopr  39177  prnc  39192  ispridlc  39195  pridlc  39196  eqrelf  39381  iss2  39467  elcoeleqvrels  39802  elfunsALTV  39900  eldisjs  39942  eleldisjs  39951  fsumshftd  40200  riotaclbgBAD  40202  renegclALT  40211  lshpinN  40237  isopos  40428  oposlem  40430  glbconN  40625  lnnat  40675  2at0mat0  40773  islvol2aN  40840  dalawlem13  41131  pclfinclN  41198  lhpoc2N  41263  ltrncnvatb  41386  cdleme11h  41514  cdlemefr32sn2aw  41652  cdlemefs32sn1aw  41662  cdleme32fvaw  41687  cdlemg1fvawlemN  41821  dicelvalN  42426  dih1dimatlem  42577  dihlatat  42585  dihjatcclem4  42669  islpolN  42731  lpolsatN  42736  lpolpolsatN  42737  mapdordlem1a  42882  mapdordlem1  42884  mapdhcl  42975  iscsrg  43212  fzsplitnd  43223  lcmineqlem12  43281  intlewftc  43302  dvrelogpow2b  43309  aks4d1p1p3  43310  aks4d1p1p2  43311  aks4d1p1p4  43312  dvle2  43313  aks4d1p8  43328  aks4d1p9  43329  isprimroot  43334  primrootsunit1  43338  primrootscoprmpow  43340  aks6d1c1p1  43348  aks6d1c1p2  43350  aks6d1c1p3  43351  evl1gprodd  43358  hashscontpow  43363  aks6d1c3  43364  aks6d1c2  43371  sticksstones1  43387  sticksstones10  43396  sticksstones11  43397  aks6d1c6lem1  43411  unitscyglem5  43440  retire  43567  reelznn0nn  43716  fsuppind  43809  fsuppssindlem2  43811  fsuppssind  43812  isnacs3  43912  nacsfix  43914  mzpclval  43927  mzpcl1  43931  mzpcl2  43932  mzpcl34  43933  mzpexpmpt  43947  mzpsubst  43950  diophin  43974  diophun  43975  2rexfrabdioph  43994  3rexfrabdioph  43995  4rexfrabdioph  43996  6rexfrabdioph  43997  7rexfrabdioph  43998  rabdiophlem2  44000  diophren  44011  fphpd  44014  fphpdo  44015  fiphp3d  44017  pellexlem1  44027  pell14qrexpclnn0  44064  pellqrex  44077  rmspecnonsq  44105  monotuz  44139  monotoddzzfi  44140  monotoddzz  44141  oddcomabszz  44142  modabsdifz  44184  rmxdioph  44214  expdiophlem2  44220  limsuc2  44239  dfac11  44255  kelac1  44256  dfac21  44259  lsmfgcl  44267  islnm  44270  lnmlssfg  44273  lmhmfgima  44277  pwslnm  44287  unxpwdom3  44288  pwfi2f1o  44289  islnr  44303  hbtlem2  44316  cnsrexpcl  44357  flcidc  44362  mendlmod  44381  proot1ex  44388  oaordnr  44488  omnord1  44497  oenord1  44508  cantnfresb  44516  onmcl  44523  tfsnfin  44544  nadd2rabtr  44576  nadd1rabtr  44580  nadd1rabex  44582  nadd1suc  44584  pwelg  44751  fipjust  44756  elnonrel  44776  elinlem  44788  elcnvlem  44791  ss2iundf  44849  dfhe3  44965  dffrege115  45168  rfovcnvf1od  45194  ntrneiel2  45276  clsneiel2  45299  neicvgel2  45310  grur1cld  45420  dvgrat  45486  cvgdvgrat  45487  radcnvrat  45488  binomcxplemdvsum  45529  binomcxplemnotnn0  45530  orbitcl  46140  modelaxreplem1  46161  modelaxreplem2  46162  modelaxrep  46164  fnchoice  46249  fiiuncl  46285  disjf1  46401  disjinfi  46410  choicefi  46417  axccdom  46438  fmptf  46454  fmptff  46484  monoords  46516  supminfrnmpt  46658  supxrleubrnmptf  46664  supminfxr  46677  supminfxr2  46682  supminfxrrnmpt  46684  monoordxrv  46694  monoordxr  46695  monoord2xrv  46696  monoord2xr  46697  caucvgbf  46702  cvgcaule  46704  fsummulc1f  46786  fsumnncl  46787  fsumf1of  46789  fsumreclf  46791  fsumlessf  46792  fsumsermpt  46794  fmul01  46795  fmulcl  46796  fmuldfeqlem1  46797  fmuldfeq  46798  fmul01lt1lem1  46799  fmul01lt1lem2  46800  fprodexp  46809  fprodabs2  46810  mccllem  46812  mccl  46813  fprodcnlem  46814  fprodcn  46815  climmulf  46819  climsuse  46823  climrecf  46824  climaddf  46830  climf  46837  sumnnodd  46845  clim2f  46849  0ellimcdiv  46862  climsubmpt  46873  climreclf  46877  climf2  46879  fnlimcnv  46880  climeldmeqmpt  46881  clim2f2  46883  climfveqmpt  46884  fnlimfvre  46887  fnlimabslt  46892  climfveqmpt3  46895  climbddf  46900  climeldmeqmpt3  46902  climinf2mpt  46927  climinfmpt  46928  limsupequzmptf  46944  lmbr3  46960  liminfreuzlem  47015  coseq0  47077  cncfshift  47087  cncfperiod  47092  fprodcncf  47113  ioodvbdlimc1lem2  47145  ioodvbdlimc2lem  47147  dvmptmulf  47150  dvnmptdivc  47151  dvnmul  47156  dvmptfprod  47158  iblspltprt  47186  itgspltprt  47192  stoweidlem2  47215  stoweidlem3  47216  stoweidlem4  47217  stoweidlem6  47219  stoweidlem8  47221  stoweidlem17  47230  stoweidlem19  47232  stoweidlem20  47233  stoweidlem21  47234  stoweidlem23  47236  stoweidlem27  47240  stoweidlem35  47248  stoweidlem42  47255  stoweidlem43  47256  stoweidlem62  47275  stoweid  47276  wallispilem3  47280  wallispi  47283  fourierdlem16  47336  fourierdlem21  47341  fourierdlem41  47361  fourierdlem42  47362  fourierdlem48  47367  fourierdlem49  47368  fourierdlem50  47369  fourierdlem51  47370  fourierdlem54  47373  fourierdlem63  47382  fourierdlem64  47383  fourierdlem65  47384  fourierdlem71  47390  fourierdlem72  47391  fourierdlem73  47392  fourierdlem83  47402  fourierdlem86  47405  fourierdlem89  47408  fourierdlem90  47409  fourierdlem91  47410  fourierdlem96  47415  fourierdlem97  47416  fourierdlem98  47417  fourierdlem99  47418  fourierdlem100  47419  fourierdlem103  47422  fourierdlem104  47423  fourierdlem105  47424  fourierdlem108  47427  fourierdlem109  47428  fourierdlem110  47429  fourierdlem112  47431  fourierdlem113  47432  etransclem24  47471  salunicl  47529  saluncl  47530  saldifcl  47532  sge0f1o  47595  sge0lempt  47623  sge0iunmptlemfi  47626  sge0p1  47627  sge0fodjrnlem  47629  sge0iunmpt  47631  sge0ltfirpmpt2  47639  sge0isummpt2  47645  sge0xaddlem2  47647  sge0xadd  47648  ismea  47664  nnfoctbdjlem  47668  nnfoctbdj  47669  meadjiun  47679  voliunsge0lem  47685  meaiuninclem  47693  meaiuninc3v  47697  hoidmvlelem2  47809  hoidmvlelem3  47810  vonvolmbl2  47876  hoimbl2  47878  vonhoire  47885  vonicclem2  47897  vonn0ioo2  47903  vonn0icc2  47905  salpreimagelt  47920  salpreimalegt  47922  salpreimagtge  47938  salpreimaltle  47939  issmf  47941  salpreimagtlt  47943  smfpreimalt  47944  smfpreimaltf  47949  issmfle  47958  smfpreimale  47967  issmfgt  47969  smfpreimagt  47975  issmfgelem  47982  issmfge  47983  smflimlem4  47987  smflim  47990  smfpreimage  47995  smfresal  48001  smfpimbor1lem1  48011  smfpimbor1lem2  48012  smflim2  48019  smflimmpt  48023  smflimsuplem1  48033  smflimsuplem2  48034  smflimsuplem3  48035  smflimsuplem5  48037  smflimsuplem7  48039  smflimsup  48041  smfliminf  48044  ormkglobd  48090  eu2ndop1stv  48398  dmfcoafv  48448  ffnaov  48472  faovcl  48473  funressndmafv2rn  48496  dfatdmfcoafv2  48527  mod2addne  48643  smonoord  48650  iccpartiltu  48707  iccpartigtl  48708  sprsymrelf1lem  48776  prproropf1olem2  48789  fmtno4prmfac193  48861  proththdlem  48901  proththd  48902  iseven  48929  isodd  48930  dfodd2  48937  evenm1odd  48940  evenp1odd  48941  enege  48946  onego  48947  epee  49006  perfectALTV  49024  bgoldbtbndlem2  49107  bgoldbtbndlem3  49108  bgoldbtbndlem4  49109  bgoldbtbnd  49110  clnbupgrel  49135  edgusgrclnbfin  49143  grimuhgr  49188  uhgrimedgi  49191  uhgrimprop  49193  isuspgrim0  49195  isuspgrimlem  49196  grimedg  49236  grtriproplem  49240  grtrif1o  49243  isgrtri  49244  grtriclwlk3  49246  cycl3grtrilem  49247  cycl3grtri  49248  grimgrtri  49250  usgrgrtrirex  49251  isubgr3stgrlem7  49273  grlimprclnbgrvtx  49300  grlimgredgex  49301  grlimgrtri  49304  usgrexmpl1tri  49326  gpgvtxel2  49349  gpgvtx0  49354  gpgvtx1  49355  gpgedgvtx0  49362  gpgedgvtx1  49363  gpgedgiov  49366  gpgedg2ov  49367  gpgedg2iv  49368  gpgnbgrvtx0  49375  gpgnbgrvtx1  49376  gpg3kgrtriex  49390  gpgprismgr4cycllem3  49398  pgnbgreunbgrlem1  49414  pgnbgreunbgrlem2lem1  49415  pgnbgreunbgrlem2lem2  49416  pgnbgreunbgrlem2lem3  49417  pgnbgreunbgrlem4  49420  pgnbgreunbgrlem5lem1  49421  pgnbgreunbgrlem5lem2  49422  pgnbgreunbgrlem5lem3  49423  pgnbgreunbgr  49426  grlimedgnedg  49432  uzlidlring  49535  smprngprmrng  49639  cbvmpox2  49651  lmod1  49807  nnolog2flm1  49905  dignn0flhalflem1  49930  elovmpoeq  50183  catprsc  50330  nelsubc3lem  50387  fucofulem2  50636  fucofvalne  50650  isthincd2lem2  50773  euendfunc  50864  cnelsubcw  50944  parmapfunc2  50977  parmapfunc  50978