Theorem eleq1d 2816

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.) Allow shortening of eleq1 2819. (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 2742	. . . 4 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
3	2	anbi1d 631	. . 3 ⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
4	3	exbidv 1922	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
5		dfclel 2807	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶))
6		dfclel 2807	. 2 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2111

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  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  eleq1  2819  eleq12d  2825  eqeltrd  2831  eqneltrd  2851  rspcimdv  3567  reuind  3712  sbcel2  4368  sbccsb2  4387  disjiun  5079  breq1  5094  breq2  5095  axrep6g  5228  inex1g  5257  intex  5282  pwexg  5316  reusv2lem4  5339  reusv2  5341  reusv3  5343  rabxfrd  5355  prex  5375  opelopabsb  5470  csbmpt12  5497  pofun  5542  seex  5575  seinxp  5700  opabid2  5768  opeliunxp2  5778  elrn2g  5830  opeldmd  5846  opeldm  5847  elreldm  5875  elsnres  5970  iss  5984  unielrel  6221  onunel  6413  funopg  6515  brprcneu  6812  brprcneuALT  6813  tz6.12f  6847  ndmfvrcl  6855  ssimaex  6907  dmfco  6918  fvmpti  6928  fvmpt3  6933  fvmptf  6950  fvmptss2  6955  respreima  6999  fvn0ssdmfun  7007  fvelrn  7009  ffnfvf  7053  ffvresb  7058  fmptco  7062  fmptcof  7063  fsn  7068  fsn2g  7071  fressnfv  7093  fvrnressn  7094  fnex  7151  funfvima  7164  funfvima3  7170  f1mpt  7195  fliftfuns  7248  isoselem  7275  isowe2  7284  riotaclb  7344  ovrspc2v  7372  ffnov  7472  fovcld  7473  ovmpos  7494  ov2gf  7495  ovg  7511  funimassov  7523  oprssdm  7527  ndmovrcl  7532  caovclg  7538  elovmpo  7591  ofmpteq  7633  sorpsscmpl  7667  uniexg  7673  unexbOLD  7681  abnexg  7689  difsnexi  7694  onint  7723  limsuc  7779  tfisi  7789  peano5  7823  xpexr  7848  xpexcnv  7850  fnexALT  7883  focdmex  7888  f1stres  7945  f2ndres  7946  xp1st  7953  xp2nd  7954  unielxp  7959  opiota  7991  fmpox  7999  offval22  8018  frxp  8056  fnse  8063  frxp2  8074  sexp2  8076  frxp3  8081  sexp3  8083  opeliunxp2f  8140  dftpos4  8175  fvmpocurryd  8201  undefnel2  8207  onnseq  8264  smoel  8280  smo11  8284  tfrlem8  8303  tfrlem9  8304  tfrlem15  8311  tfr2b  8315  tz7.44-2  8326  tz7.44-3  8327  oacl  8450  omcl  8451  oecl  8452  oaord1  8466  omordi  8481  oen0  8501  oeeui  8517  nnacl  8526  nnmcl  8527  nnecl  8528  nnmordi  8546  nnaordex  8553  omsmolem  8572  naddcllem  8591  naddov2  8594  naddf  8596  naddssim  8600  naddelim  8601  naddasslem1  8609  naddasslem2  8610  naddsuc2  8616  erexb  8647  elecex  8672  qliftfuns  8728  ixpsnval  8824  elixp2  8825  resixp  8857  undifixp  8858  mptelixpg  8859  resixpfo  8860  elixpsn  8861  fundmen  8953  fopwdom  8998  disjen  9047  xpf1o  9052  unfi  9080  cnvfi  9085  fnfi  9087  f1oenfirn  9089  f1domfi  9090  unblem2  9177  imafiOLD  9200  pwfi  9203  fiint  9211  iunfi  9227  isfsupp  9249  fsuppun  9271  ffsuppbi  9282  elfi2  9298  wdom2d  9466  ixpiunwdom  9476  dfom3  9537  cantnfvalf  9555  cantnflt  9562  cantnflem1  9579  r1fin  9666  tz9.12lem3  9682  ranksnb  9720  ranklim  9737  r1pw  9738  r1pwALT  9739  r1pwcl  9740  rankuni2b  9746  djuexb  9802  cardmin2  9892  infxpenc2lem1  9910  dfac8alem  9920  dfac8clem  9923  ac5num  9927  acni2  9937  acnlem  9939  alephon  9960  alephfplem3  9997  alephfplem4  9998  dfac4  10013  dfac5lem1  10014  dfac5lem5  10018  dfac2a  10021  dfac2b  10022  dfacacn  10033  dfac12lem2  10036  dfac12r  10038  dfac12k  10039  cofsmo  10160  cfsmolem  10161  isfin1a  10183  fin1ai  10184  isfin3  10187  infpssrlem3  10196  fin23lem7  10207  fin23lem11  10208  enfin2i  10212  isf34lem4  10268  fin1a2lem7  10297  hsmexlem9  10316  hsmexlem4  10320  hsmex  10323  axcc2lem  10327  axcc3  10329  axdc3lem2  10342  axcclem  10348  zornn0g  10396  ttukeylem3  10402  ttukeylem6  10405  ttukey2g  10407  brdom7disj  10422  brdom6disj  10423  fnct  10428  konigthlem  10459  axregndlem2  10494  axinfnd  10497  axacndlem5  10502  axacnd  10503  fpwwe2lem4  10525  fpwwe2lem12  10533  fpwwe  10537  pwfseqlem1  10549  pwfseqlem3  10551  pwfseqlem4a  10552  pwfseqlem4  10553  wununi  10597  wunpw  10598  wunpr  10600  wunr1om  10610  tskpw  10644  tskr1om  10658  inar1  10666  grupw  10686  grupr  10688  gruurn  10689  gruiun  10690  ingru  10706  grur1a  10710  grothomex  10720  grothac  10721  addnidpi  10792  indpi  10798  adderpq  10847  mulerpq  10848  addclprlem2  10908  mulclprlem  10910  distrlem4pr  10917  prlem934  10924  ltexprlem3  10929  ltexprlem4  10930  ltexprlem7  10933  ltexpri  10934  prlem936  10938  reclem2pr  10939  reclem3pr  10940  addclsr  10974  mulclsr  10975  supsrlem  11002  supsr  11003  axaddf  11036  axmulf  11037  axaddrcl  11043  axmulrcl  11045  renegcl  11424  negreb  11426  negn0  11546  negf1o  11547  ltord1  11643  leord1  11644  eqord1  11645  ltord2  11646  leord2  11647  eqord2  11648  negfi  12071  infm3  12081  cju  12121  peano5nni  12128  peano2nn  12137  dfnn2  12138  nn1m1nn  12146  nnaddcl  12148  nnmulcl  12149  nnsub  12169  nndivtr  12172  un0addcl  12414  un0mulcl  12415  elnnnn0  12424  nn0sub  12431  fcdmnn0fsuppg  12441  elz  12470  nnnegz  12471  elz2  12486  znegclb  12509  zaddcl  12512  nzadd  12520  zmulcl  12521  zneo  12556  nneo  12557  zeo  12559  peano5uzi  12562  zindd  12574  eluzsubOLD  12768  uzp1  12773  uzaddcl  12802  ublbneg  12831  eqreznegel  12832  supminf  12833  zsupss  12835  qmulz  12849  qnegcl  12864  irradd  12871  irrmul  12872  xnn0xaddcl  13134  fzrev2  13488  injresinjlem  13690  negmod0  13782  om2uzuzi  13856  uzindi  13889  fsuppmapnn0ub  13902  mptnn0fsuppr  13906  seqexw  13924  seqcl2  13927  seqcl  13929  seqf  13930  monoord  13939  monoord2  13940  sermono  13941  seqsplit  13942  seqcaopr2  13945  seqid3  13953  seqhomo  13956  expcllem  13979  expcl2lem  13980  m1expcl2  13992  faccl  14190  facdiv  14194  facndiv  14195  bccmpl  14216  bccl  14229  hashclb  14265  hasheq0  14270  hashfn  14282  seqcoll  14371  opfi1uzind  14418  ccatalpha  14501  reuccatpfxs1lem  14653  reuccatpfxs1  14654  repswccat  14693  repswrevw  14694  2cshw  14720  2cshwcshw  14732  cshimadifsn  14736  cshco  14743  swrd2lsw  14859  wwlktovf  14863  wwlktovf1  14864  wwlktovfo  14865  wrd2f1tovbij  14867  shftlem  14975  shftf  14986  cjval  15009  cjth  15010  remim  15024  cnpart  15147  uzin2  15252  caubnd2  15265  sqreulem  15267  clim  15401  clim2  15411  lo1o12  15440  climrlim2  15454  lo1resb  15471  o1resb  15473  lo1eq  15475  climmpt2  15480  climshftlem  15481  rlimcld2  15485  climcn1  15499  climcn2  15500  o1dif  15537  iserex  15564  climub  15569  climserle  15570  isercoll  15575  climcau  15578  caurcvg2  15585  caucvgb  15587  summolem3  15621  summolem2a  15622  zsum  15625  fsum  15627  sumss2  15633  fsumcvg2  15634  fsumclf  15645  fsumsplitf  15649  fsumsplit1  15652  sumpr  15655  sumtp  15656  fsumm1  15658  fsum1p  15660  isummulc2  15669  fsum2dlem  15677  fsumcom2  15681  fsumshftm  15688  fsum0diag2  15690  fsumge1  15704  fsum00  15705  fsumabs  15708  telfsumo  15709  telfsumo2  15710  fsumparts  15713  fsumrlim  15718  fsumo1  15719  o1fsum  15720  fsumiun  15728  binomlem  15736  isumshft  15746  isum1p  15748  isumrpcl  15750  climcndslem1  15756  climcndslem2  15757  climcnds  15758  infcvgaux2i  15765  cvgrat  15790  mertens  15793  clim2prod  15795  prodfn0  15801  prodfrec  15802  prodfdiv  15803  ntrivcvgfvn0  15806  prodmolem3  15840  prodmolem2a  15841  zprod  15844  fprod  15848  prodss  15854  fprodser  15856  fprodm1  15874  fprod1p  15875  fprodm1s  15877  fprodp1s  15878  fprodabs  15881  fprodn0  15886  fprod2dlem  15887  fprodcnv  15890  fprodcom2  15891  fproddivf  15894  fprodsplitf  15895  fprodsplit1f  15897  bpolycl  15959  fprodefsum  16002  rpnnen2lem11  16133  mod2eq1n2dvds  16258  mulsucdiv2z  16264  zob  16270  nn0o1gt2  16292  nno  16293  nn0o  16294  divalglem7  16310  bitsf1  16357  sadcp1  16366  smupp1  16391  qnumdencl  16650  iserodd  16747  pcqcl  16768  pcxnn0cl  16772  pcxcl  16773  pcgcd1  16789  dvdsprmpweqle  16798  pcmpt  16804  pcmpt2  16805  pcmptdvds  16806  infpnlem2  16823  infpn2  16825  1arith  16839  elgz  16843  mul4sq  16866  4sqlem13  16869  4sqlem17  16873  4sqlem18  16874  4sqlem19  16875  vdwlem1  16893  vdwlem2  16894  vdwnn  16910  ramtcl2  16923  ramcl  16941  prmonn2  16951  prmodvdslcmf  16959  isstruct2  17060  wunress  17160  firest  17336  imasaddfnlem  17432  imasvscafn  17441  xpsfrnel2  17468  mreintcl  17497  ismred2  17505  mreexexlemd  17550  mreexexlem3d  17552  mreexexlem4d  17553  iscatd2  17587  catpropd  17615  subsubc  17760  isfunc  17771  inclfusubc  17850  fncnvimaeqv  18026  joindef  18280  joinval  18281  meetdef  18294  meetval  18295  oduclatb  18413  acsdrsel  18449  isacs4lem  18450  isacs5lem  18451  acsdrscl  18452  mgmsscl  18553  mgmpropd  18559  mgm1  18566  gsumvalx  18584  issubmgm  18610  issubmgm2  18611  mgmhmima  18623  sgrppropd  18639  mndpropd  18667  issubm  18711  0subm  18725  insubm  18726  mhmimalem  18732  gsumwsubmcl  18745  gsumwspan  18754  symggrplem  18792  sursubmefmnd  18804  injsubmefmnd  18805  smndex1basss  18813  mulgsubcl  19001  issubg  19039  issubg2  19054  issubg4  19058  0subg  19064  0subgOLD  19065  isnsg  19068  isnsg2  19069  nsgbi  19070  isnsg3  19073  elnmz  19076  nmzbi  19077  nmzsubg  19078  eqgval  19090  eqgid  19093  cycsubgcl  19119  ghmrn  19142  ghmnsgima  19153  gass  19214  oppgsubg  19276  f1omvdconj  19359  symgfisg  19381  psgneldm  19416  0subgALT  19481  odhash3  19489  sylow2blem2  19534  lsmsubm  19566  lsmsubg  19567  efgsf  19642  efgsdm  19643  efgs1b  19649  efgredlema  19653  eqgabl  19747  ablnsg  19760  cyggenod2  19798  gsumzaddlem  19834  gsummhm2  19852  gsum2dlem2  19884  gsum2d2lem  19886  gsumcom2  19888  dprdfeq0  19937  dprdsubg  19939  dprd2da  19957  ablfacrp  19981  pgpfac1lem3  19992  pgpfaclem1  19996  ablfaclem3  20002  ablfac2  20004  cycsubggenodd  20024  isrng  20073  issrg  20107  srgfcl  20115  rglcom4d  20130  srgbinomlem4  20148  isring  20156  iscrng  20159  dvdsr  20281  irredrmul  20346  isrngim  20364  isrim0  20401  issubrng  20463  subrngringnsg  20469  issubrng2  20474  rhmimasubrnglem  20481  issubrg  20487  issubrg2  20508  subrgpropd  20524  isdrngd  20681  isdrngdOLD  20683  issdrg  20704  sdrgacs  20717  issrngd  20771  islmod  20798  lmodlema  20799  islmodd  20800  lmodprop2d  20858  rmodislmodlem  20863  rmodislmod  20864  lssset  20867  islssd  20869  lsscl  20876  lsslss  20895  lsspropd  20952  lmhmima  20982  lbsind  21015  lsmcl  21018  islvec  21039  lmhmlvec  21045  lspsolvlem  21080  lspsolv  21081  lvecpropd  21105  rnglidlmcl  21154  rnglidl0  21167  rnglidlmmgm  21183  rngqiprngimf1lem  21232  rngqiprngimf1  21238  ring2idlqus  21247  xrsdsreclblem  21350  xrsdsreclb  21351  cnsubrglem  21354  prmirred  21412  pzriprnglem4  21422  pzriprnglem8  21426  pzriprngALT  21433  znunithash  21502  cofipsgn  21531  zrhpsgnelbas  21532  rzgrp  21561  isphl  21566  phllmhm  21570  ipcl  21571  isphld  21592  phlpropd  21593  phlssphl  21597  cssincl  21626  pjdm  21645  dsmmval  21672  dsmmbas2  21675  dsmmelbas  21677  frlmbas  21693  frlmup1  21736  lindfind  21754  lindsind  21755  f1lindf  21760  islindf4  21776  psrbag  21855  psrbaglefi  21864  mplsubglem  21937  mpllsslem  21938  ltbwe  21980  psrbagsn  21999  subrgasclcl  22003  mplind  22006  mpfind  22043  psdmul  22082  coe1mul2lem2  22183  gsumply1eq  22225  evl1vsd  22260  mpfpf1  22267  pf1mpf  22268  pf1ind  22271  matecl  22341  m1detdiag  22513  mdetralt  22524  mdetralt2  22525  mdetunilem2  22529  mdetunilem9  22536  m2detleiblem3  22545  m2detleiblem4  22546  smadiadetlem0  22577  cpmatacl  22632  chpscmat  22758  uniopn  22813  inopn  22815  fiinopn  22817  istps  22850  fctop  22920  iscld  22943  isopn2  22948  mretopd  23008  iscldtop  23011  perfi  23071  tgrest  23075  restcld  23088  ordtbaslem  23104  ordtrest2lem  23119  ordtrest2  23120  iscn  23151  cnpval  23152  iscnp  23153  tgcn  23168  subbascn  23170  ssidcn  23171  lmbrf  23176  cnpnei  23180  cnima  23181  iscncl  23185  cnconst2  23199  cnrest2  23202  cnpresti  23204  cnprest  23205  cnindis  23208  lmres  23216  lmcnp  23220  iscnrm  23239  t1sncld  23242  cnrmi  23276  cncmp  23308  cmpsublem  23315  fiuncmp  23320  unconn  23345  conncompid  23347  conncompconn  23348  conncompss  23349  1stcfb  23361  2ndcrest  23370  2ndcctbss  23371  2ndcdisj  23372  1stccnp  23378  islly  23384  isnlly  23385  subislly  23397  restnlly  23398  restlly  23399  islly2  23400  hausllycmp  23410  cldllycmp  23411  dislly  23413  isptfin  23432  islocfin  23433  ptfinfin  23435  finlocfin  23436  dissnlocfin  23445  locfindis  23446  comppfsc  23448  kgenval  23451  elkgen  23452  kgeni  23453  cmpkgen  23467  1stckgenlem  23469  kgencn2  23473  ptpjpre1  23487  elpt  23488  elptr  23489  ptbasin  23493  xkobval  23502  xkoval  23503  xkoopn  23505  txbasval  23522  tx1cn  23525  tx2cn  23526  dfac14  23534  xkoccn  23535  txcnp  23536  ptcnplem  23537  txcnmpt  23540  txindislem  23549  txdis1cn  23551  txlly  23552  txnlly  23553  pthaus  23554  ptrescn  23555  hauseqlcld  23562  txlm  23564  tx2ndc  23567  txkgen  23568  xkoptsub  23570  xkopt  23571  xkoco1cn  23573  xkoco2cn  23574  xkococnlem  23575  xkococn  23576  cnmpt11  23579  cnmpt12  23583  cnmpt21  23587  cnmpt22  23590  cnmptkp  23596  cnmptk1p  23601  xkoinjcn  23603  txconn  23605  qtopval2  23612  elqtop  23613  idqtop  23622  qtopcld  23629  qtopeu  23632  qtoprest  23633  qtopomap  23634  qtopcmap  23635  ishmeo  23675  hmeoopn  23682  hmeocld  23683  ordthmeolem  23717  ptcmpfi  23729  elmptrab  23743  fgcl  23794  trfil2  23803  cfinfil  23809  uzrest  23813  ufilss  23821  trufil  23826  cfinufil  23844  ufinffr  23845  ufildr  23847  rnelfm  23869  flfcntr  23959  ptcmplem2  23969  ptcmplem3  23970  ptcmplem4  23971  ptcmplem5  23972  cnextfvval  23981  tmdcn2  24005  tmdmulg  24008  tmdgsum2  24012  symgtgp  24022  opnsubg  24024  clssubg  24025  tgpconncompeqg  24028  ghmcnp  24031  tgphaus  24033  tgpt0  24035  qustgpopn  24036  qustgplem  24037  tsmsgsum  24055  tsmssubm  24059  tsmsres  24060  tsmsf1o  24061  tsmsxplem1  24069  tsmsxplem2  24070  tsmsxp  24071  istrg  24080  istdrg  24082  istdrg2  24094  istlm  24101  istvc  24108  ustval  24119  ustincl  24124  ustdiag  24125  ustinvel  24126  ustexhalf  24127  ust0  24136  ucnima  24196  fmucndlem  24206  prdsdsf  24283  prdsxmet  24285  imasf1oxmet  24291  imasf1omet  24292  prdsxmslem2  24445  metustsym  24471  isnlm  24591  qtopbaslem  24674  xrtgioo  24723  reperflem  24735  fsumcn  24789  expcn  24791  expcnOLD  24793  xrhmeo  24872  cnllycmp  24883  bndth  24885  isclm  24992  lmhmclm  25015  lmmcvg  25189  fmcfil  25200  iscfil3  25201  iscau2  25205  iscau4  25207  iscmet3lem1  25219  iscmet3  25221  cfilres  25224  caussi  25225  equivcfil  25227  flimcfil  25242  bcthlem1  25252  isbn  25266  srabn  25288  ishl2  25298  cmslssbn  25300  cmscsscms  25301  minveclem3b  25356  ivthlem1  25380  ivthlem2  25381  ivthlem3  25382  ivth2  25384  ivthle  25385  ivthle2  25386  ivthicc  25387  ovolficcss  25398  ovolunlem1a  25425  ovolunlem1  25426  ovolfiniun  25430  ovoliunlem1  25431  ovoliunlem3  25433  ovoliun  25434  ovoliun2  25435  shft2rab  25437  ovolshftlem1  25438  sca2rab  25441  ovolscalem1  25442  mblsplit  25461  finiunmbl  25473  volun  25474  volfiniun  25476  voliunlem1  25479  voliunlem3  25481  iunmbl  25482  voliun  25483  volsup  25485  ioombl  25494  ioorcl  25506  vitalilem1  25537  vitalilem2  25538  vitalilem3  25539  vitalilem4  25540  vitali  25542  ismbf1  25553  mbfdm  25555  ismbf  25557  ismbfcn  25558  mbfima  25559  mbfimaicc  25560  ismbfcn2  25567  ismbfd  25568  ismbf2d  25569  mbfeqalem1  25570  mbfmax  25578  mbfposr  25581  mbfposb  25582  ismbf3d  25583  mbfimaopnlem  25584  mbfimaopn2  25586  cncombf  25587  isi1f  25603  i1fd  25610  itg1mulc  25633  mbfi1fseqlem4  25647  itg2lcl  25656  isibl  25694  iblitg  25697  iblcnlem1  25717  iblcnlem  25718  iblrelem  25720  iblpos  25722  itgeqa  25743  itgfsum  25756  itgabs  25764  limcvallem  25800  ellimc  25802  ellimc2  25806  limcmpt  25812  cnmptlimc  25819  dvbsss  25831  cpnfval  25862  elcpn  25864  dvmptfsum  25907  dvle  25940  dvfsumle  25954  dvfsumleOLD  25955  dvfsumge  25956  dvfsumabs  25957  dvfsumrlimf  25959  dvfsumlem1  25960  dvfsumlem2  25961  dvfsumlem2OLD  25962  dvfsumlem3  25963  dvfsumlem4  25964  dvfsumrlimge0  25965  dvfsumrlim  25966  dvfsumrlim2  25967  dvfsum2  25969  itgsubstlem  25983  itgsubst  25984  mdegcl  26002  deg1nn0clb  26023  isuc1p  26074  plyeq0lem  26143  plyco  26174  plycj  26211  plycjOLD  26213  dvply2g  26220  dvnply2  26223  plydivlem4  26232  fta1lem  26243  fta1  26244  elqaalem1  26255  elqaalem2  26256  elqaalem3  26257  elqaa  26258  ulmcau  26332  radcnv0  26353  radcnvlt1  26355  radcnvle  26357  pserdvlem2  26366  coseq1  26462  efeq1  26465  sinord  26471  efif1olem2  26480  efif1olem4  26482  lognegb  26527  logcj  26543  argimgt0  26549  logtayl  26597  2irrexpq  26668  root1eq1  26693  logrec  26701  2irrexpqALT  26738  angrteqvd  26744  angpieqvdlem  26766  atans  26868  atans2  26869  dmarea  26895  areambl  26896  rlimcnp  26903  rlimcnp2  26904  xrlimcnp  26906  harmonicbnd  26942  harmonicbnd2  26943  lgamcvglem  26978  wilthlem2  27007  wilth  27009  efnnfsumcl  27041  vmacl  27056  efvmacl  27058  efchtdvds  27097  sqff1o  27120  fsumdvdscom  27123  musumsum  27130  fsumdvdsmul  27133  fsumdvdsmulOLD  27135  fsumvma  27152  perfect  27170  dchrelbasd  27178  lgsval  27240  lgsval2lem  27246  lgsdir2lem4  27267  lgsdir2  27269  lgsqrlem1  27285  lgsdchr  27294  m1lgs  27327  2lgs  27346  mul2sq  27358  2sqlem6  27362  2sqblem  27370  2sq2  27372  rplogsumlem2  27424  dchrisumlema  27427  dchrisumlem2  27429  dchrisumlem3  27430  dchrvmasumlem2  27437  dchrvmasumlem3  27438  dchrisum0flblem2  27448  dchrisum0flb  27449  dchrisum0fno1  27450  ostthlem1  27566  nodmon  27590  noextendseq  27607  nodense  27632  madefi  27859  addsproplem1  27913  addsproplem3  27915  addsprop  27920  addsf  27926  addsbdaylem  27960  negsproplem1  27971  negsproplem3  27973  negsprop  27978  negsbdaylem  27999  mulsproplemcbv  28055  mulsproplem1  28056  mulsproplem10  28065  mulsprop  28070  noseqp1  28222  noseqind  28223  peano5n0s  28249  dfn0s2  28261  n0addscl  28273  n0mulscl  28274  n0sbday  28281  onsfi  28284  n0s0m1  28289  n0subs  28290  n0p1nns  28297  dfnns2  28298  nn1m1nns  28300  zaddscl  28319  zmulscld  28322  elzn0s  28323  peano5uzs  28329  expscllem  28354  zs12addscl  28388  zs12half  28391  zs12negsclb  28392  zs12zodd  28393  zs12bday  28395  mirval  28634  perpneq  28693  isperp2  28694  isperp2d  28695  foot  28701  islnopp  28718  islnoppd  28719  outpasch  28734  hlpasch  28735  ishpg  28738  colopp  28748  colhp  28749  lmif  28764  islmib  28766  lmiinv  28771  trgcopy  28783  trgcopyeu  28785  acopyeu  28813  inaghl  28824  tgasa1  28837  f1otrgitv  28849  f1otrg  28850  isfusgr  29297  opfusgr  29302  fusgrfisbase  29307  fusgrfisstep  29308  nbupgrel  29324  nbumgrvtx  29325  nbusgreledg  29332  edgnbusgreu  29346  nb3grprlem1  29359  uvtxusgrel  29382  cusgredg  29403  cplgr2vpr  29412  cusgrexg  29423  usgredgsscusgredg  29439  fusgrn0degnn0  29479  rusgrnumwrdl2  29566  rgrx0ndm  29573  wlkcomp  29610  wlkdlem2  29661  clwlkcomp  29758  iswwlks  29815  wwlknllvtx  29825  0enwwlksnge1  29843  wlkiswwlks2lem5  29852  wwlksm1edg  29860  wwlksnred  29871  wwlksnext  29872  wwlksnextbi  29873  wwlksnredwwlkn  29874  wwlksnextfun  29877  wwlksnextinj  29878  wwlksnextsurj  29879  wwlksnextbij  29881  wwlksnfi  29885  wwlksnextproplem2  29889  wwlksnextprop  29891  2wlkdlem4  29907  rusgrnumwwlkl1  29947  rusgrnumwwlks  29953  isclwwlk  29962  clwwlk1loop  29966  clwwlkccatlem  29967  clwlkclwwlklem2a1  29970  clwlkclwwlklem2a4  29975  clwlkclwwlklem2a  29976  clwlkclwwlklem2  29978  clwlkclwwlklem3  29979  clwlkclwwlk  29980  clwlkclwwlk2  29981  clwwisshclwwslemlem  29991  clwwisshclwwslem  29992  clwwisshclwws  29993  clwwlknlbonbgr1  30017  clwwlkinwwlk  30018  clwwlkn1  30019  loopclwwlkn1b  30020  clwwlkn1loopb  30021  clwwlkn2  30022  clwwlkel  30024  clwwlkf  30025  clwwlkwwlksb  30032  clwwlkext2edg  30034  wwlksext2clwwlk  30035  wwlksubclwwlk  30036  eleclclwwlknlem2  30039  umgr2cwwk2dif  30042  s2elclwwlknon2  30082  clwwlknonwwlknonb  30084  clwwlknonex2lem2  30086  clwwlknonex2  30087  3wlkdlem4  30140  upgr3v3e3cycl  30158  upgr4cycl4dv4e  30163  eupth2lem2  30197  eulerpathpr  30218  1vwmgr  30254  3vfriswmgrlem  30255  3vfriswmgr  30256  3cyclfrgrrn1  30263  vdgn1frgrv2  30274  frgrncvvdeqlem3  30279  frgrncvvdeqlem8  30284  frgrncvvdeqlem9  30285  frgrwopregasn  30294  frgrwopregbsn  30295  frgrwopreglem5ALT  30300  frgr2wwlk1  30307  frgr2wwlkeqm  30309  fusgr2wsp2nb  30312  2clwwlk2clwwlklem  30324  extwwlkfabel  30331  nvvop  30587  isnvlem  30588  sspval  30701  nmorepnf  30746  phpar  30802  siilem2  30830  bnsscmcl  30846  ubthlem1  30848  shaddcl  31195  shmulcl  31196  hsn0elch  31226  hhssablo  31241  hhssnvt  31243  hhsssh  31247  shscl  31296  shintcl  31308  chintcl  31310  shincl  31359  chincl  31477  h1datomi  31559  chscllem2  31616  sumspansn  31627  spansncvi  31630  5oalem2  31633  5oalem3  31634  pjini  31677  pjjsi  31678  eigposi  31814  nmoprepnf  31845  nmfnrepnf  31858  dmadjrnb  31884  lnophmlem1  31994  lnophm  31997  nmcopex  32007  lnconi  32011  nmbdfnlb  32028  nmcfnex  32031  imaelshi  32036  rnbra  32085  leopg  32100  pjbdlni  32127  pjhmop  32128  hmopidmch  32131  pjclem4  32177  pj3si  32185  strlem1  32228  atssma  32356  atcv0eq  32357  atcv1  32358  atomli  32360  atcvatlem  32363  cdj3lem2a  32414  cdj3lem3a  32417  xppreima  32625  fmptcof2  32637  aciunf1lem  32642  funcnv4mpt  32649  1stpreimas  32685  f1od2  32700  fpwrelmapffslem  32713  xrofsup  32748  fzspl  32770  fzsplit3  32774  nnindf  32800  fprodex01  32806  fsumiunle  32810  indfval  32835  indf1ofs  32845  gsumhashmul  33039  fzto1st  33070  fxpsubm  33139  fxpsubg  33140  fxpsubrg  33141  isslmd  33169  slmdlema  33170  elrgspnlem2  33208  elrgspnlem4  33210  subsdrg  33262  qusker  33312  0nellinds  33333  unitprodclb  33352  nsgmgclem  33374  nsgmgc  33375  nsgqusf1olem2  33377  elrspunidl  33391  prmidlval  33400  prmidlc  33411  opprlidlabs  33448  dfufd2lem  33512  psrbasfsupp  33570  lindsunlem  33635  brfldext  33656  brfinext  33663  finextfldext  33675  finexttrb  33676  extdg1id  33677  fldextrspunlsplem  33684  constrconj  33756  constrfin  33757  trisecnconstr  33803  smatrcl  33807  submateq  33820  lmatfval  33825  lmatcl  33827  qtophaus  33847  locfinreflem  33851  locfinref  33852  zartopn  33886  zarcmplem  33892  rhmpreimacnlem  33895  xpinpreima  33917  xpinpreima2  33918  cnre2csqlem  33921  tpr2rico  33923  prsdm  33925  prsrn  33926  ordtrest2NEWlem  33933  ordtrest2NEW  33934  zrhcntr  33990  qqhval2  33993  isrrext  34011  ismntoplly  34036  esumcvg  34097  sigaval  34122  issiga  34123  0elsiga  34125  sigaclcu  34128  issgon  34134  prsiga  34142  sigaclci  34143  difelsiga  34144  unelsiga  34145  ispisys2  34164  inelpisys  34165  unelldsys  34169  sigapildsyslem  34172  sigapildsys  34173  ldgenpisyslem1  34174  ldgenpisys  34177  isros  34179  unelros  34182  difelros  34183  fiunelros  34185  inelsros  34189  diffiunisros  34190  rossros  34191  measvuni  34225  measiun  34229  voliune  34240  volfiniune  34241  brfae  34259  ismbfm  34262  mbfmcnvima  34266  mbfmcst  34270  1stmbfm  34271  2ndmbfm  34272  imambfm  34273  sitgval  34343  issibf  34344  sibfima  34349  sitgfval  34352  sitgclg  34353  eulerpartlemelr  34368  eulerpartlemsf  34370  eulerpartleme  34374  eulerpartlemt0  34380  eulerpartlemt  34382  eulerpartgbij  34383  eulerpartlemr  34385  eulerpartlemmf  34386  eulerpartlemgvv  34387  eulerpartlemgs2  34391  eulerpartlemn  34392  eulerpart  34393  cndprobprob  34449  rrvsum  34465  orvcelel  34481  ballotlemodife  34509  ballotlemsdom  34523  ballotlemrv  34531  ballotlemrv1  34532  ballotlemrv2  34533  ballotlem1ri  34546  fsum2dsub  34618  reprinfz1  34633  reprpmtf1o  34637  reprdifc  34638  breprexplema  34641  hgt750lema  34668  hgt750leme  34669  bnj149  34885  bnj222  34893  bnj1112  34993  bnj1148  35006  fissorduni  35099  fineqvrep  35135  fineqvnttrclse  35142  gblacfnacd  35144  vonf1owev  35150  loop1cycl  35179  subfacp1lem3  35224  subfacp1lem6  35227  erdszelem10  35242  kur14  35258  cvxsconn  35285  cnllysconn  35287  resconn  35288  iscvm  35301  cvmliftlem5  35331  cvmliftlem15  35340  cvmlift2lem1  35344  cvmlift2lem12  35356  cvmlift2lem13  35357  sat1el2xp  35421  fmlasuc  35428  gonan0  35434  gonar  35437  satefvfmla0  35460  msubrn  35571  msubco  35573  ismfs  35591  mvtinf  35597  mclsax  35611  mppspstlem  35613  elmpps  35615  nnuni  35769  dfdm5  35815  dfrn5  35816  elima4  35818  rdgprc0  35833  pprodss4v  35924  elfuns  35955  fnimage  35969  imageval  35970  fwddifval  36202  fwddifnval  36203  fwddifnp1  36205  elhf2g  36216  hfun  36218  hfninf  36226  filnetlem4  36421  onsucconn  36478  onsucsuccmp  36484  limsucncmp  36486  onint1  36489  fveleq  36491  findreccl  36493  nndivsub  36497  weiunse  36508  bj-seex  36962  bj-adjg1  37083  bj-mooreset  37142  bj-ismoored0  37146  bj-ismoored  37147  bj-inftyexpitaudisj  37245  bj-inftyexpidisj  37250  bj-isvec  37327  bj-isclm  37331  csbmpo123  37371  topdifinffinlem  37387  topdifinffin  37388  csbfinxpg  37428  phpreu  37650  finixpnum  37651  lindsenlbs  37661  poimirlem16  37682  poimirlem17  37683  poimirlem19  37685  poimirlem20  37686  poimirlem22  37688  poimirlem23  37689  poimirlem24  37690  poimirlem25  37691  poimirlem26  37692  poimirlem28  37694  poimirlem29  37695  poimirlem30  37696  poimirlem31  37697  poimirlem32  37698  poimir  37699  mblfinlem3  37705  ex-ovoliunnfl  37709  voliunnfl  37710  volsupnfl  37711  mbfresfi  37712  itgabsnc  37735  ftc1anclem6  37744  ftc1anclem7  37745  ftc1anclem8  37746  ftc1anc  37747  dvasin  37750  sdclem2  37788  fdc  37791  incsequz  37794  neificl  37799  mettrifi  37803  cntotbnd  37842  cnpwstotbnd  37843  ismtyima  37849  ismtyhmeolem  37850  heiborlem2  37858  heiborlem3  37859  heiborlem4  37860  heiborlem5  37861  heiborlem6  37862  heiborlem10  37866  isrngo  37943  isdivrngo  37996  drngoi  37997  idlval  38059  isidlc  38061  idladdcl  38065  idllmulcl  38066  idlrmulcl  38067  0idl  38071  pridlval  38079  smprngopr  38098  prnc  38113  ispridlc  38116  pridlc  38117  eqrelf  38296  iss2  38378  elcoeleqvrels  38638  elfunsALTV  38736  eldisjs  38766  eleldisjs  38772  fsumshftd  38997  riotaclbgBAD  38999  renegclALT  39008  lshpinN  39034  isopos  39225  oposlem  39227  glbconN  39422  lnnat  39472  2at0mat0  39570  islvol2aN  39637  dalawlem13  39928  pclfinclN  39995  lhpoc2N  40060  ltrncnvatb  40183  cdleme11h  40311  cdlemefr32sn2aw  40449  cdlemefs32sn1aw  40459  cdleme32fvaw  40484  cdlemg1fvawlemN  40618  dicelvalN  41223  dih1dimatlem  41374  dihlatat  41382  dihjatcclem4  41466  islpolN  41528  lpolsatN  41533  lpolpolsatN  41534  mapdordlem1a  41679  mapdordlem1  41681  mapdhcl  41772  iscsrg  42009  fzsplitnd  42021  lcmineqlem12  42079  intlewftc  42100  dvrelogpow2b  42107  aks4d1p1p3  42108  aks4d1p1p2  42109  aks4d1p1p4  42110  dvle2  42111  aks4d1p8  42126  aks4d1p9  42127  isprimroot  42132  primrootsunit1  42136  primrootscoprmpow  42138  aks6d1c1p1  42146  aks6d1c1p2  42148  aks6d1c1p3  42149  evl1gprodd  42156  hashscontpow  42161  aks6d1c3  42162  aks6d1c2  42169  sticksstones1  42185  sticksstones10  42194  sticksstones11  42195  sticksstones12a  42196  aks6d1c6lem1  42209  unitscyglem5  42238  retire  42358  reelznn0nn  42500  fsuppind  42629  fsuppssindlem2  42631  fsuppssind  42632  isnacs3  42749  nacsfix  42751  mzpclval  42764  mzpcl1  42768  mzpcl2  42769  mzpcl34  42770  mzpexpmpt  42784  mzpsubst  42787  diophin  42811  diophun  42812  2rexfrabdioph  42835  3rexfrabdioph  42836  4rexfrabdioph  42837  6rexfrabdioph  42838  7rexfrabdioph  42839  rabdiophlem2  42841  diophren  42852  fphpd  42855  fphpdo  42856  fiphp3d  42858  pellexlem1  42868  pell14qrexpclnn0  42905  pellqrex  42918  rmspecnonsq  42946  monotuz  42980  monotoddzzfi  42981  monotoddzz  42982  oddcomabszz  42983  modabsdifz  43025  rmxdioph  43055  expdiophlem2  43061  limsuc2  43080  dfac11  43101  kelac1  43102  dfac21  43105  lsmfgcl  43113  islnm  43116  lnmlssfg  43119  lmhmfgima  43123  pwslnm  43133  unxpwdom3  43134  pwfi2f1o  43135  islnr  43150  hbtlem2  43163  cnsrexpcl  43204  flcidc  43209  mendlmod  43228  proot1ex  43235  oaordnr  43335  omnord1  43344  oenord1  43355  cantnfresb  43363  onmcl  43370  tfsnfin  43391  nadd2rabtr  43423  nadd1rabtr  43427  nadd1rabex  43429  nadd1suc  43431  pwelg  43599  fipjust  43604  elnonrel  43624  elinlem  43637  elcnvlem  43640  ss2iundf  43698  dfhe3  43814  dffrege115  44017  rfovcnvf1od  44043  ntrneiel2  44125  clsneiel2  44148  neicvgel2  44159  grur1cld  44271  dvgrat  44351  cvgdvgrat  44352  radcnvrat  44353  binomcxplemdvsum  44394  binomcxplemnotnn0  44395  orbitcl  44996  modelaxreplem1  45017  modelaxreplem2  45018  modelaxrep  45020  fnchoice  45072  fiiuncl  45108  disjf1  45226  disjinfi  45235  choicefi  45243  axccdom  45265  fmptf  45282  fmptff  45312  monoords  45344  supminfrnmpt  45489  supxrleubrnmptf  45495  supminfxr  45508  supminfxr2  45513  supminfxrrnmpt  45515  monoordxrv  45525  monoordxr  45526  monoord2xrv  45527  monoord2xr  45528  caucvgbf  45533  cvgcaule  45535  fsummulc1f  45617  fsumnncl  45618  fsumf1of  45620  fsumreclf  45622  fsumlessf  45623  fsumsermpt  45625  fmul01  45626  fmulcl  45627  fmuldfeqlem1  45628  fmuldfeq  45629  fmul01lt1lem1  45630  fmul01lt1lem2  45631  fprodexp  45640  fprodabs2  45641  mccllem  45643  mccl  45644  fprodcnlem  45645  fprodcn  45646  climmulf  45650  climsuse  45654  climrecf  45655  climaddf  45661  climf  45668  sumnnodd  45676  clim2f  45680  0ellimcdiv  45693  climsubmpt  45704  climreclf  45708  climf2  45710  fnlimcnv  45711  climeldmeqmpt  45712  clim2f2  45714  climfveqmpt  45715  fnlimfvre  45718  fnlimabslt  45723  climfveqmpt3  45726  climbddf  45731  climeldmeqmpt3  45733  climinf2mpt  45758  climinfmpt  45759  limsupequzmptf  45775  lmbr3  45791  liminfreuzlem  45846  coseq0  45908  cncfshift  45918  cncfperiod  45923  fprodcncf  45944  ioodvbdlimc1lem2  45976  ioodvbdlimc2lem  45978  dvmptmulf  45981  dvnmptdivc  45982  dvnmul  45987  dvmptfprod  45989  iblspltprt  46017  itgspltprt  46023  stoweidlem2  46046  stoweidlem3  46047  stoweidlem4  46048  stoweidlem6  46050  stoweidlem8  46052  stoweidlem17  46061  stoweidlem19  46063  stoweidlem20  46064  stoweidlem21  46065  stoweidlem23  46067  stoweidlem27  46071  stoweidlem35  46079  stoweidlem42  46086  stoweidlem43  46087  stoweidlem62  46106  stoweid  46107  wallispilem3  46111  wallispi  46114  fourierdlem16  46167  fourierdlem21  46172  fourierdlem41  46192  fourierdlem42  46193  fourierdlem48  46198  fourierdlem49  46199  fourierdlem50  46200  fourierdlem51  46201  fourierdlem54  46204  fourierdlem63  46213  fourierdlem64  46214  fourierdlem65  46215  fourierdlem71  46221  fourierdlem72  46222  fourierdlem73  46223  fourierdlem83  46233  fourierdlem86  46236  fourierdlem89  46239  fourierdlem90  46240  fourierdlem91  46241  fourierdlem96  46246  fourierdlem97  46247  fourierdlem98  46248  fourierdlem99  46249  fourierdlem100  46250  fourierdlem103  46253  fourierdlem104  46254  fourierdlem105  46255  fourierdlem108  46258  fourierdlem109  46259  fourierdlem110  46260  fourierdlem112  46262  fourierdlem113  46263  etransclem24  46302  salunicl  46360  saluncl  46361  saldifcl  46363  sge0f1o  46426  sge0lempt  46454  sge0iunmptlemfi  46457  sge0p1  46458  sge0fodjrnlem  46460  sge0iunmpt  46462  sge0ltfirpmpt2  46470  sge0isummpt2  46476  sge0xaddlem2  46478  sge0xadd  46479  ismea  46495  nnfoctbdjlem  46499  nnfoctbdj  46500  meadjiun  46510  voliunsge0lem  46516  meaiuninclem  46524  meaiuninc3v  46528  hoidmvlelem2  46640  hoidmvlelem3  46641  vonvolmbl2  46707  hoimbl2  46709  vonhoire  46716  vonicclem2  46728  vonn0ioo2  46734  vonn0icc2  46736  salpreimagelt  46751  salpreimalegt  46753  salpreimagtge  46769  salpreimaltle  46770  issmf  46772  salpreimagtlt  46774  smfpreimalt  46775  smfpreimaltf  46780  issmfle  46789  smfpreimale  46798  issmfgt  46800  smfpreimagt  46806  issmfgelem  46813  issmfge  46814  smflimlem4  46818  smflim  46821  smfpreimage  46826  smfresal  46832  smfpimbor1lem1  46842  smfpimbor1lem2  46843  smflim2  46850  smflimmpt  46854  smflimsuplem1  46864  smflimsuplem2  46865  smflimsuplem3  46866  smflimsuplem5  46868  smflimsuplem7  46870  smflimsup  46872  smfliminf  46875  ormkglobd  46919  cjnpoly  46926  eu2ndop1stv  47162  dmfcoafv  47212  ffnaov  47236  faovcl  47237  funressndmafv2rn  47260  dfatdmfcoafv2  47291  mod2addne  47401  smonoord  47408  iccpartiltu  47459  iccpartigtl  47460  sprsymrelf1lem  47528  prproropf1olem2  47541  fmtno4prmfac193  47610  proththdlem  47650  proththd  47651  iseven  47665  isodd  47666  dfodd2  47673  evenm1odd  47676  evenp1odd  47677  enege  47682  onego  47683  epee  47742  perfectALTV  47760  bgoldbtbndlem2  47843  bgoldbtbndlem3  47844  bgoldbtbndlem4  47845  bgoldbtbnd  47846  clnbupgrel  47871  edgusgrclnbfin  47879  grimuhgr  47924  uhgrimedgi  47927  uhgrimprop  47929  isuspgrim0  47931  isuspgrimlem  47932  grimedg  47972  grtriproplem  47976  grtrif1o  47979  isgrtri  47980  grtriclwlk3  47982  cycl3grtrilem  47983  cycl3grtri  47984  grimgrtri  47986  usgrgrtrirex  47987  isubgr3stgrlem7  48009  grlimprclnbgrvtx  48036  grlimgredgex  48037  grlimgrtri  48040  usgrexmpl1tri  48062  gpgvtxel2  48085  gpgvtx0  48090  gpgvtx1  48091  gpgedgvtx0  48098  gpgedgvtx1  48099  gpgedgiov  48102  gpgedg2ov  48103  gpgedg2iv  48104  gpgnbgrvtx0  48111  gpgnbgrvtx1  48112  gpg3kgrtriex  48126  gpgprismgr4cycllem3  48134  pgnbgreunbgrlem1  48150  pgnbgreunbgrlem2lem1  48151  pgnbgreunbgrlem2lem2  48152  pgnbgreunbgrlem2lem3  48153  pgnbgreunbgrlem4  48156  pgnbgreunbgrlem5lem1  48157  pgnbgreunbgrlem5lem2  48158  pgnbgreunbgrlem5lem3  48159  pgnbgreunbgr  48162  grlimedgnedg  48168  uzlidlring  48272  cbvmpox2  48373  lmod1  48530  nnolog2flm1  48628  dignn0flhalflem1  48653  catprsc  49051  nelsubc3lem  49108  fucofulem2  49349  fucofvalne  49363  isthincd2lem2  49473  euendfunc  49564  cnelsubclem  49641