Theorem eleq2d 2819

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)

Hypothesis

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

Assertion

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

Proof of Theorem eleq2d

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1d.1	. . . 4 ⊢ (𝜑 → 𝐴 = 𝐵)
2		dfcleq 2726	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	1, 2	sylib 218	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		anbi2 634	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	alexbii 1834	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	syl 17	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
7		dfclel 2809	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
8		dfclel 2809	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

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

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 2115  ax-9 2123  ax-ext 2705

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

This theorem is referenced by:  eleq2  2822  eleq12d  2827  eleqtrd  2835  neleqtrd  2855  eqabrd  2874  raleqbidv  3313  rexeqbidv  3314  reueqbidv  3385  rabeqbidva  3412  elabd2  3621  sbcbid  3792  csbeq2d  3852  csbeq2dv  3853  cbvcsbw  3856  cbvcsb  3857  cbvcsbv  3858  csbie  3881  csbied  3882  csbie2g  3886  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  sbcel12  4360  sbcel1g  4365  sbcel2  4367  prel12g  4817  eliuni  4949  iuneqconst  4955  iuneq12df  4970  iuneq12d  4973  cbviun  4987  cbviin  4988  cbviung  4989  cbviing  4990  cbviunv  4991  cbviinv  4992  iinxsng  5040  iinxprg  5041  iunxsng  5042  iunxsngf  5044  cbvdisj  5072  cbvdisjv  5073  disjor  5077  disjiund  5086  mpteq12da  5178  mpteq12f  5180  mpteq12dva  5181  axpweq  5293  rabxfrd  5359  rbropapd  5507  opeliunxp  5688  opeliun2xp  5689  opeliunxp2  5784  iunxpf  5794  elimampt  5999  elrelimasn  6042  elimasni  6047  imadifssran  6106  xpdifid  6123  ressn  6240  funfni  6595  fnbr  6597  dffv3  6827  elfv2ex  6874  fvelrnb  6891  foelcdmi  6892  fvun1  6922  fvco2  6928  elfvmptrab1w  6965  elfvmptrab1  6966  elfvmptrab  6967  elpreima  7000  dff3  7042  fmptco  7071  fnelfp  7118  fnelnfp  7120  tpres  7144  fnprb  7151  fntpb  7152  funfvima3  7179  eluniima  7193  dff13  7197  f1ounsn  7215  f1eqcocnv  7244  isoini  7281  riotaeqdv  7313  mpoeq123dva  7429  cbvmpox  7448  elimampo  7492  ovelrn  7531  elovmpod  7599  elovmpo  7600  elovmporab  7601  elovmporab1w  7602  elovmporab1  7603  elovmpt3rab1  7615  fiun  7884  f1iun  7885  zfrep6  7896  fmpox  8008  el2mpocsbcl  8024  el2mpocl  8025  bropopvvv  8029  bropfvvvv  8031  xpord2indlem  8086  xpord3inddlem  8093  elsuppfng  8108  elsuppfn  8109  suppfnss  8128  opeliunxp2f  8149  mpoxopn0yelv  8152  mpoxopovel  8159  rntpos  8178  mpocurryd  8208  fpr2  8243  wfr2  8266  onoviun  8272  smoel  8289  smoiso  8291  smoel2  8292  smo11  8293  tfrlem9  8313  oalimcl  8484  oaass  8485  omordi  8490  omordlim  8501  omlimcl  8502  odi  8503  omeulem1  8506  omeulem2  8507  oen0  8510  oeordi  8511  oeordsuc  8518  oelimcl  8524  oeeulem  8525  oeeui  8526  nnmordi  8555  oaabs2  8573  omabs  8575  omsmolem  8581  ereldm  8684  iiner  8722  elmapg  8772  elpmg  8776  elixpsn  8871  ixpsnf1o  8872  boxriin  8874  omxpenlem  9002  pw2f1olem  9005  phplem2  9125  php3  9129  infn0  9197  elfi  9308  dffi3  9326  marypha2lem2  9331  ordiso2  9412  wemapsolem  9447  elharval  9458  inf3lemd  9528  inf3lem1  9529  inf3lem2  9530  inf3lem3  9531  cantnfs  9567  cantnfp1lem3  9581  cantnflem1b  9587  cantnflem1  9590  ttrclselem2  9627  trcl  9629  frr2  9664  r1sdom  9678  r1ordg  9682  r1pwss  9688  tz9.12lem3  9693  tz9.12  9694  r1elwf  9700  rankr1ai  9702  rankidb  9704  rankr1bg  9707  rankval2  9722  rankunb  9754  tcrank  9788  acni  9947  acni2  9948  acndom  9953  infpwfien  9964  alephnbtwn  9973  cardaleph  9991  cardinfima  9999  iunfictbso  10016  dfac3  10023  dfac5lem5  10029  dfac5  10031  dfac9  10039  dfac12r  10049  kmlem2  10054  kmlem12  10064  kmlem13  10065  kmlem14  10066  ackbij2lem3  10142  ackbij2  10144  cofsmo  10171  alephsing  10178  fin23lem30  10244  isf32lem9  10263  itunisuc  10321  axcc2lem  10338  axcc3  10340  domtriomlem  10344  axdc2lem  10350  axdc2  10351  axdc3lem2  10353  axdc3lem4  10355  axdc4lem  10357  ac6c4  10383  zorn2lem1  10398  ttukeylem6  10416  pwcfsdom  10485  axregndlem2  10505  axinfndlem1  10507  axacndlem4  10512  axacnd  10514  pwfseqlem1  10560  inar1  10677  inatsk  10680  gruurn  10700  grur1  10722  eltskm  10745  genpelv  10902  eluz1  12746  elixx1  13261  elixx3g  13265  elioo2  13293  elfz1  13419  elfz2  13421  elfzp1  13481  fzpr  13486  fzsuc2  13489  fzrev3  13497  elfzp12  13510  fzm1  13514  elfzo  13568  fz0add1fz1  13642  elfzo0l  13663  elfzom1b  13673  fzosplitsni  13686  elfzr  13688  elfzlmr  13689  zmodidfzo  13811  seqp1  13930  seqf1o  13957  bcval  14218  bcpasc  14235  hashf1lem1  14369  fundmge2nop0  14416  wrdmap  14460  elovmpowrd  14472  ccatfval  14487  elfzelfzccat  14494  ccatlid  14501  ccatass  14503  ccatrn  14504  ccatalpha  14508  swrdfv2  14576  ccatswrd  14583  swrdccat2  14584  pfxfv  14597  pfxeq  14610  ccatpfx  14615  swrdswrd  14619  swrdpfx  14621  pfxpfx  14622  cats1un  14635  swrdccatfn  14638  swrdccatin1  14639  pfxccatin12lem4  14640  pfxccatin12lem1  14642  swrdccatin2  14643  pfxccatin12lem2c  14644  pfxccatin12lem2  14645  swrdccat3blem  14653  swrdccatin1d  14657  swrdccatin2d  14658  pfxccatin12d  14659  revccat  14680  revrev  14681  repswpfx  14699  repswccat  14700  cshwidxmod  14717  2cshw  14727  cshwcshid  14741  cshwcsh2id  14742  cshimadifsn  14743  cshimadifsn0  14744  revco  14748  ccatco  14749  cshco  14750  swrdco  14751  ofccat  14883  shftfn  14987  shftval  14988  limsupgle  15391  ello12  15430  elo12  15441  isercolllem3  15581  sumeq1  15603  fsumsplit  15655  sumsplit  15682  fsum2dlem  15684  fsumcom2  15688  fsumparts  15720  explecnv  15779  pwdif  15782  fprodser  15863  fprodsplit  15880  fprod2dlem  15894  fprodcom2  15898  eftlub  16025  divalgmod  16324  bitsval  16342  bitsp1e  16350  bitsp1o  16351  sadfval  16370  sadcp1  16373  sadval  16374  sadcadd  16376  sadadd2  16378  saddisjlem  16382  sadadd  16385  sadass  16389  smufval  16395  smuval  16399  smuval2  16400  smupvallem  16401  smu01lem  16403  smueqlem  16408  smumul  16411  bezoutlem2  16458  bezoutlem4  16460  algfx  16498  eucalgcvga  16504  reumodprminv  16723  nnnn0modprm0  16725  unbenlem  16827  prmreclem5  16839  vdwapval  16892  vdwapun  16893  vdwnnlem1  16914  vdwnn  16917  ramval  16927  0ram  16939  ramub1lem2  16946  prmgaplem7  16976  prmlem0  17024  elrest  17338  prdsbasmpt  17381  prdsleval  17388  prdsbasmpt2  17393  pwselbasb  17399  imasaddfnlem  17440  imasvscafn  17449  divsfval  17459  ismre  17500  mreunirn  17511  mrisval  17544  ismri  17545  isacs  17565  catidd  17594  iscatd2  17595  ismon  17648  isepi  17655  sectffval  17665  sectfval  17666  dfiso2  17687  cicsym  17719  issubc  17750  catsubcat  17754  isfunc  17779  funcres  17811  funcpropd  17817  ffthiso  17846  isnat  17865  isnat2  17866  fuciso  17893  initoval  17908  termoval  17909  isinito  17911  istermo  17912  iszeroo  17913  isinitoi  17914  istermoi  17915  initoid  17916  termoid  17917  iszeroi  17924  2initoinv  17925  initoeu1  17926  initoeu2  17931  2termoinv  17932  termoeu1  17933  arwhoma  17960  elsetchom  17996  setcmon  18002  setcepi  18003  setciso  18006  catciso  18026  elestrchom  18042  estrcbasbas  18045  funcestrcsetclem7  18060  funcestrcsetclem8  18061  funcestrcsetclem9  18062  fthestrcsetc  18064  fullestrcsetc  18065  equivestrcsetc  18066  setc1strwun  18067  funcsetcestrclem7  18075  funcsetcestrclem8  18076  funcsetcestrclem9  18077  fthsetcestrc  18079  fullsetcestrc  18080  hofcl  18173  hofpropd  18181  yonedalem4c  18191  yonedainv  18195  yonffthlem  18196  lubeldm  18265  glbeldm  18278  joindef  18288  meetdef  18302  poslubdg  18326  acsficl2d  18466  acsmapd  18468  psref  18488  psss  18494  dirge  18517  chnccats1  18539  chnccat  18540  chnrev  18541  mgmpropd  18567  issstrmgm  18569  grpidval  18577  grpidpropd  18578  grpidd  18587  ismgmhm  18612  issubmgm  18618  issgrpd  18646  sgrppropd  18647  ismndd  18672  mndpropd  18675  imasmnd2  18690  imasmnd  18691  xpsmnd0  18694  ismhm  18701  issubm  18719  gsumsgrpccat  18756  elefmndbas2  18790  smndex1mndlem  18825  imasgrp2  18976  imasgrp  18977  issubg  19047  subginv  19054  isnsg  19075  eqg0el  19103  quselbas  19104  isghm  19135  isghmOLD  19136  resghm2b  19154  conjnmzb  19173  conjnsg  19174  ghmpropd  19176  isga  19211  elcntz  19242  elcntzsn  19245  cntzrcl  19247  resscntz  19253  symgextf1  19341  gsmsymgreqlem2  19351  f1otrspeq  19367  pmtrfrn  19378  pmtrdifellem3  19398  pmtrdifellem4  19399  psgnunilem1  19413  psgnunilem5  19414  psgnunilem2  19415  psgnunilem3  19416  psgneldm2  19424  psgnfitr  19437  psgnsn  19440  gexdvds  19504  gex1  19511  isslw  19528  sylow3lem2  19548  lsmelvalx  19560  pj1ghm  19623  efgtlen  19646  efgsfo  19659  efgredlemc  19665  frgp0  19680  frgpmhm  19685  qusabl  19785  frgpnabllem1  19793  imasabl  19796  cycsubmcmn  19809  0cyg  19813  cycsubgcyg  19821  gsumval3  19827  gsumcllem  19828  gsumzaddlem  19841  gsumzsplit  19847  gsummptfzcl  19889  eldprd  19926  dprdcntz2  19960  dprd2d2  19966  dmdprdsplit2lem  19967  dmdprdsplit2  19968  dprdsplit  19970  ablfac2  20011  isrngd  20099  rngpropd  20100  imasrng  20103  qusrng  20106  ringurd  20111  isringd  20217  imasring  20257  xpsring1d  20260  dvdsrval  20288  isunit  20300  dvdsrpropd  20343  isirred  20346  isrnghm  20368  isrngim  20372  c0ghm  20388  c0snghm  20391  isrhm  20405  isrim0  20409  islring  20464  issubrng  20471  opprsubrng  20483  issubrg  20495  opprsubrg  20517  resrhm2b  20526  rhmpropd  20533  rnghmresel  20544  elrngchom  20548  rnghmsubcsetclem1  20555  rnghmsubcsetclem2  20556  rngcid  20559  rngcsect  20560  rngciso  20562  funcrngcsetcALT  20565  zrinitorngc  20566  zrtermorngc  20567  rhmresel  20573  elringchom  20577  rhmsubcsetclem1  20584  rhmsubcsetclem2  20585  ringcid  20588  rhmsscrnghm  20589  rhmsubcrngclem1  20590  rhmsubcrngclem2  20591  ringcsect  20594  ringciso  20596  ringcbasbas  20597  zrtermoringc  20599  srhmsubc  20604  rhmsubclem3  20611  rhmsubclem4  20612  drngunit  20658  isdrngd  20689  isdrngdOLD  20691  issdrg  20712  sdrgunit  20720  isabv  20735  issrngd  20779  islmod  20806  lmodprop2d  20866  islss  20876  islssd  20877  lssats2  20942  ellspsn  20945  islmhm  20970  lmhmf1o  20989  lmhmima  20990  lmhmpreima  20991  reslmhm  20995  pwssplit3  21004  lmhmpropd  21016  islbs  21019  lspprel  21037  lspfixed  21074  lbsacsbs  21102  lbsextlem1  21104  lbsextlem2  21105  lbsextlem3  21106  lbsextlem4  21107  ixpsnbasval  21151  isridlrng  21165  rnglidlmmgm  21191  isridl  21198  quscrng  21229  rngqiprngimfolem  21236  rngqiprngimf1lem  21240  rngqiprngimfo  21247  islpidl  21271  lidldvgen  21280  irinitoringc  21425  pzriprnglem13  21439  pzriprnglem14  21440  zrhrhmb  21456  znf1o  21497  frgpcyg  21519  psgnevpmb  21533  isphld  21600  phlssphl  21605  elocv  21614  iscss  21629  isobs  21666  obs2ss  21675  dsmmfi  21684  dsmmelbas  21685  dsmmlss  21690  frlmelbas  21702  frlmlbs  21743  frlmup1  21744  ellspd  21748  islinds  21755  islindf2  21760  f1lindf  21768  islindf4  21784  assamulgscmlem2  21847  psrgrp  21903  mplsubglem  21945  mpllsslem  21946  mplmonmul  21982  subrgascl  22012  subrgasclcl  22013  mpfind  22061  ismhp  22074  gsumply1subr  22165  lply1binomsc  22246  matbas2d  22358  matecl  22360  matvscl  22366  mat1  22382  mat0dim0  22402  mat0dimid  22403  mat0dimscm  22404  mat1dimelbas  22406  dmatel  22428  scmatel  22440  scmateALT  22447  scmataddcl  22451  scmatsubcl  22452  smatvscl  22459  scmatghm  22468  mat1scmat  22474  mdetunilem7  22553  mdetunilem9  22555  smadiadetr  22610  cramerimplem2  22619  cramer0  22625  pmatcoe1fsupp  22636  cpmatpmat  22645  cpmatel  22646  cpmatacl  22651  cpmatinvcl  22652  mat2pmatghm  22665  mat2pmatmul  22666  decpmatmullem  22706  pmatcollpwlem  22715  pmatcollpw3fi1lem1  22721  pmatcollpwscmatlem1  22724  monmat2matmon  22759  chfacfscmul0  22793  chfacfscmulgsum  22795  chfacfpmmulgsum  22799  cayhamlem1  22801  cpmadugsumlemB  22809  cpmadugsumlemC  22810  cpmadugsumlemF  22811  cayhamlem2  22819  istopon  22847  eltg  22892  eltg2  22893  eltop  22909  eltop2  22910  eltop3  22911  pptbas  22943  iscld  22962  neiss2  23036  isnei  23038  neiptopnei  23067  neiptopreu  23068  lpfval  23073  lpval  23074  islp  23075  maxlp  23082  islpi  23084  neitr  23115  restlp  23118  ordtbas2  23126  ordtrest2  23139  lmfval  23167  cnfval  23168  iscn  23170  iscnp  23172  tgcn  23187  tgcnp  23188  lmbrf  23195  cnpresti  23223  ist1  23256  ist1-2  23282  cnt1  23285  haust1  23287  cmpfi  23343  cmpfii  23344  1stcfb  23380  2ndc1stc  23386  1stcrest  23388  2ndcdisj  23391  1stcelcls  23396  nllyi  23410  subislly  23416  islocfin  23452  lfinpfin  23459  locfindis  23465  locfincf  23466  comppfsc  23467  kgenval  23470  elkgen  23471  kgencn2  23492  txbas  23502  eltx  23503  ptval  23505  ptpjpre1  23506  ptopn2  23519  ptpjopn  23547  ptclsg  23550  xkoccn  23554  txdis  23567  txdis1cn  23570  ptrescn  23574  hausdiag  23580  hauseqlcld  23581  txhaus  23582  xkohaus  23588  elqtop  23632  qtopeu  23651  kqcldsat  23668  hmeofval  23693  ptuncnv  23742  ptunhmeo  23743  elmptrab  23762  fbdmn0  23769  elfg  23806  elfilss  23811  filunirn  23817  fixufil  23857  elfm  23882  rnelfmlem  23887  rnelfm  23888  fmfnfmlem4  23892  elflim2  23899  flimtopon  23905  elflim  23906  hausflim  23916  flimcls  23920  flfnei  23926  isflf  23928  hausflf  23932  cnpflf  23936  cnflf  23937  txflf  23941  isfcls  23944  fclstopon  23947  isfcls2  23948  fclssscls  23953  fclsnei  23954  fclsfnflim  23962  flimfnfcls  23963  isfcf  23969  fcfelbas  23971  cnpfcf  23976  cnfcf  23977  flfcntr  23978  alexsublem  23979  alexsubALTlem3  23984  cnextfun  23999  cnextfvval  24000  cnextf  24001  cnextcn  24002  tmdgsum2  24031  tgpconncomp  24048  ghmcnp  24050  qustgplem  24056  eltsms  24068  haustsms  24071  tsmsgsum  24074  tsmssubm  24078  tsmssplit  24087  isust  24139  ustbas  24162  elutop  24168  ustuqtoplem  24174  ustuqtop4  24179  ustuqtop  24181  utopsnneiplem  24182  utopsnneip  24183  utopsnnei  24184  isusp  24196  isucn  24212  ucncn  24219  iscfilu  24222  neipcfilu  24230  iscusp  24233  cnextucn  24237  ispsmet  24239  ismet  24258  isxmet  24259  elblps  24322  elbl  24323  elmopn  24377  prdsbl  24426  neibl  24436  met1stc  24456  metrest  24459  prdsxmslem2  24464  txmetcnp  24482  txmetcn  24483  metustsym  24490  cfilucfil2  24496  elbl4  24498  metuel  24499  psmetutop  24502  restmetu  24505  metucn  24506  tngngp  24589  isnmhm  24681  zcld  24749  metnrmlem1a  24794  elcncf  24829  cncfcnvcn  24866  cnheibor  24901  lebnumlem1  24907  ishtpy  24918  isphtpy  24927  om1elbas  24979  elpi1  24992  pi1xfr  25002  pi1coghm  25008  tcphcph  25184  lmmbrf  25209  iscfil  25212  iscau  25223  iscauf  25227  caucfil  25230  iscmet  25231  cmetcaulem  25235  iscmet3lem1  25238  iscmet3lem2  25239  iscmet3  25240  bcthlem1  25271  cmsss  25298  cmetcusp1  25300  cmetcusp  25301  cmscsscms  25320  rrxcph  25339  minveclem3b  25375  ovolfioo  25415  ovolficc  25416  ovolctb  25438  ovoliunnul  25455  ovolshftlem1  25457  sca2rab  25460  ovolscalem1  25461  ovolicc2lem1  25465  ovolicc2lem2  25466  ovolicc2lem4  25468  ovolicc2lem5  25469  iundisj  25496  iunmbl2  25505  uniioombllem3  25533  vitalilem2  25557  vitalilem3  25558  mbfss  25594  i1faddlem  25641  i1fmullem  25642  mbfi1fseqlem2  25664  mbfi1fseqlem4  25666  mbfi1fseq  25669  itg2splitlem  25696  itg2split  25697  itg2monolem1  25698  itg2gt0  25708  isibl  25713  iblss2  25754  itgss3  25763  itgsplit  25784  ellimc  25821  limcmo  25830  cnlimc  25836  limciun  25842  limcun  25843  eldv  25846  dvbsss  25850  dvreslem  25857  elcpn  25883  dvaddf  25892  dvmulf  25893  dvcof  25899  rolle  25941  dvlip2  25947  dvivthlem1  25960  lhop1  25966  lhop2  25967  ftc1cn  25997  fta1glem2  26121  plyco0  26144  elply  26147  ply1termlem  26155  eltayl  26314  tayl0  26316  taylplem1  26317  taylplem2  26318  dvtaylp  26325  taylthlem1  26328  taylthlem2  26329  taylthlem2OLD  26330  abelth  26398  cxpcn3  26705  rlimcnp  26922  fsumharmonic  26969  dchrelbas  27194  pntrsumbnd2  27525  ostth2lem2  27592  nolesgn2ores  27631  nogesgn1ores  27633  nosupprefixmo  27659  noinfprefixmo  27660  nosupcbv  27661  nosupdm  27663  nosupfv  27665  nosupres  27666  nosupbnd1lem1  27667  nosupbnd1lem3  27669  nosupbnd1lem5  27671  nosupbnd2lem1  27674  noinfcbv  27676  noinfdm  27678  noinffv  27680  noinfres  27681  noinfbnd1lem1  27682  noinfbnd1lem3  27684  noinfbnd1lem5  27686  noinfbnd2lem1  27689  elmade  27832  elold  27834  ssltleft  27835  ssltright  27836  oldlim  27852  madebday  27865  newbday  27867  sltlpss  27873  bdayiun  27880  cofcutr  27888  cofcutrtime  27891  lrrecval  27902  lrrecval2  27903  addsval  27925  precsexlem9  28173  precsexlem11  28175  sltonold  28218  onnolt  28223  onslt  28224  noseqrdgfn  28256  istrkgb  28453  istrkgcb  28454  istrkge  28455  istrkgl  28456  istrkgld  28457  axtgsegcon  28462  axtg5seg  28463  axtgbtwnid  28464  axtgpasch  28465  axtgupdim2  28469  axtgeucl  28470  tgdim01  28505  iscgrg  28510  isismt  28532  tglnunirn  28546  tglngval  28549  tgellng  28551  legval  28582  legov  28583  legov2  28584  ishlg  28600  mirreu3  28652  mirval  28653  mirfv  28654  mircgr  28655  mirbtwn  28656  ismir  28657  mireq  28663  symquadlem  28687  israg  28695  perpln1  28708  perpln2  28709  isperp  28710  islnopp  28737  outpasch  28753  ishpg  28757  iscgra  28807  dfcgra2  28828  isinag  28836  isleag  28845  iseqlg  28865  f1otrgitv  28868  f1otrg  28869  f1otrge  28870  ttgval  28873  ttgelitv  28881  elee  28892  brbtwn  28898  brcgr  28899  axlowdimlem16  28956  ebtwntg  28981  elntg2  28984  upgrex  29091  edgupgr  29133  upgredg  29136  edglnl  29142  numedglnl  29143  uhgr2edg  29207  umgr2edg1  29210  usgredg2vlem1  29224  usgredg2vlem2  29225  ushgredgedg  29228  ushgredgedgloop  29230  uhgrspansubgrlem  29289  fusgrfisstep  29328  nbgrval  29335  nbgrel  29339  nbupgrel  29344  nbgr2vtx1edg  29349  nbuhgr2vtx1edgblem  29350  nbuhgr2vtx1edgb  29351  nbusgreledg  29352  usgrnbcnvfv  29364  uvtxval  29386  uvtxel  29387  uvtx01vtx  29396  uvtxusgrel  29402  nbcplgr  29433  cplgr3v  29434  cusgrexi  29442  structtocusgr  29445  vtxdgfval  29467  vtxdg0v  29473  vtxdeqd  29477  vtxdun  29481  1loopgrnb0  29502  1loopgrvd0  29504  1hevtxdg0  29505  1hevtxdg1  29506  1egrvtxdg1  29509  umgr2v2evtxel  29522  umgr2v2enb1  29526  umgr2v2evd2  29527  vtxdginducedm1lem4  29542  vtxdginducedm1  29543  finsumvtxdg2sstep  29549  ewlksfval  29601  isewlk  29602  wksfval  29609  iswlk  29610  uspgr2wlkeq  29645  wlkres  29668  dfpth2  29728  usgr2pthlem  29762  clwlkcompim  29779  uspgrn2crct  29807  wwlks  29834  iswwlksn  29837  wwlknvtx  29844  wlkiswwlks2  29874  wwlksm1edg  29880  wwlksnred  29891  wwlksnext  29892  wwlksnredwwlkn  29894  wwlksnredwwlkn0  29895  wwlksnwwlksnon  29914  wspn0  29923  usgr2wspthons3  29966  rusgrnumwwlkb0  29973  clwwlk  29984  clwwlkccatlem  29990  clwlkclwwlklem2a4  29998  clwlkclwwlk  30003  clwwisshclwwslem  30015  clwwlkinwwlk  30041  clwwlkel  30047  clwwlkf  30048  clwwlkext2edg  30057  wwlksext2clwwlk  30058  wwlksubclwwlk  30059  clwwnisshclwwsn  30060  eleclclwwlknlem2  30062  erclwwlknsym  30071  erclwwlkntr  30072  umgrhashecclwwlk  30079  clwwlkvbij  30114  eupth2lem3lem3  30231  eupth2lem3lem4  30232  eupth2lem3lem6  30234  eupth2lemb  30238  eucrct2eupth  30246  fusgreg2wsplem  30334  2clwwlklem  30344  2clwwlk2clwwlklem  30347  2clwwlkel  30350  2clwwlk2clwwlk  30351  extwwlkfabel  30354  clwwlknonclwlknonf1o  30363  dlwwlknondlwlknonf1olem1  30365  numclwwlk2lem1  30377  numclwlk2lem2f  30378  numclwlk2lem2f1o  30380  ex-res  30442  isssp  30725  sspn  30737  islno  30754  isblo  30783  nmlno0  30796  ishmo  30812  dipdir  30843  dipass  30846  ubthlem1  30871  ubthlem2  30872  htthlem  30918  htth  30919  ocel  31282  ocnel  31299  shsel  31315  shsel2  31323  shmodsi  31390  pjhtheu  31395  pjeq  31400  axpjpj  31421  pjoc2  31440  elspani  31544  h1de2ctlem  31556  elspansn  31567  elspansn2  31568  elnlfn  31929  eleigvec  31958  riesz3i  32063  cbviunf  32556  iuneq12daf  32557  iunrdx  32564  iunrnmptss  32566  cbvdisjf  32572  disjorf  32580  disjabrex  32583  disjabrexf  32584  iundisjf  32590  disjrdx  32592  brab2d  32609  fresunsn  32629  2ndresdju  32653  abfmpunirn  32656  abfmpeld  32658  abfmpel  32659  fmptcof2  32661  acunirnmpt2  32664  acunirnmpt2f  32665  aciunf1lem  32666  funcnvmpt  32671  suppss3  32730  fpwrelmap  32740  xrofsup  32775  iundisjfi  32804  eliccioo  32940  s3f1  32957  ccatf1  32959  ccatws1f1o  32961  swrdrn3  32965  ismnt  32993  mgcoval  32996  gsummpt2co  33059  gsumpart  33074  gsumhashmul  33078  gsummulsubdishift1  33079  xrge0tsmsbi  33084  gsumwrd2dccatlem  33087  gsumwrd2dccat  33088  cycpmco2  33143  cyc3co2  33150  isfxp  33178  cntrval2  33181  inftmrel  33190  isinftm  33191  isslmd  33212  urpropd  33241  elrgspn  33256  erlval  33268  rlocval  33269  rloccring  33280  rloc1r  33282  domnprodeq0  33286  domnpropd  33287  isdrng4  33305  fracfld  33318  resv1r  33348  ellspds  33377  ellpi  33382  lbslsp  33386  rhmimaidl  33441  isprmidl  33447  qsidomlem1  33461  qsidomlem2  33462  ismxidl  33471  crngmxidl  33478  drng0mxidl  33485  opprqus0g  33499  qsfld  33507  isrprm  33526  rsprprmprmidlb  33532  ressply1evls1  33574  ply1mulrtss  33591  ply1coedeg  33598  dimpropd  33693  lbslsat  33701  extdg1id  33751  fldextrspunlsplem  33758  fldextrspunlsp  33759  elirng  33771  ply1annidllem  33786  constrsuc  33823  constrconj  33830  constrllcllem  33837  constrlccllem  33838  constrcccllem  33839  nn0constr  33846  smatrcl  33881  smatcl  33887  ist0cld  33918  txomap  33919  locfinreflem  33925  zarclsiin  33956  zart0  33964  rhmpreimacnlem  33969  metidval  33975  cnre2csqima  33996  ordtrest2NEW  34008  fmcncfil  34016  fsumcvg4  34035  ofcfval  34183  measvuni  34299  meascnbl  34304  faeval  34331  ismbfm  34336  elunirnmbfm  34337  imambfm  34347  elcarsg  34390  itgeq12dv  34411  issibf  34418  eulerpartlems  34445  eulerpartlemgc  34447  eulerpartlemgvv  34461  eulerpartlemgu  34462  eulerpart  34467  rrvmbfm  34527  elorvc  34545  elorrvc  34549  dstfrvunirn  34560  ballotlemfc0  34578  ballotlemfcc  34579  ballotlemsima  34601  ballotlemrv  34605  fzssfzo  34624  signstfvn  34654  signstfvneq0  34657  signstres  34660  repr0  34696  reprinrn  34703  reprdifc  34712  hgt750lemg  34739  hgt750lemb  34741  istrkg2d  34751  axtgupdim2ALTV  34753  afsval  34756  brafs  34757  bnj945  34857  bnj1400  34919  bnj18eq1  35011  bnj916  35017  bnj1014  35045  bnj1015  35046  bnj1110  35066  bnj1417  35125  rankval2b  35182  r1filimi  35186  r1ssel  35190  onvf1odlem3  35221  vonf1owev  35224  revpfxsfxrev  35232  cplgredgex  35237  pfxwlk  35240  revwlk  35241  subfacp1lem2b  35297  subfacp1lem4  35299  subfacp1lem5  35300  subfacp1lem6  35301  ptpconn  35349  cvmscbv  35374  iscvm  35375  cvmsi  35381  cvmsval  35382  cvmliftmolem1  35397  cvmlift2lem12  35430  cvmlift2lem13  35431  cvmlift3lem7  35441  snmlval  35447  satfv1  35479  satfvsucsuc  35481  satfrnmapom  35486  satf0op  35493  satf0n0  35494  sat1el2xp  35495  fmlafvel  35501  isfmlasuc  35504  fmlaomn0  35506  gonan0  35508  goaln0  35509  gonar  35511  goalr  35513  satffunlem1lem2  35519  satffunlem2lem2  35522  satfv0fvfmla0  35529  satef  35532  satefvfmla0  35534  sategoelfvb  35535  satfv1fvfmla1  35539  mrsubfval  35624  mrsubvrs  35638  mclsrcl  35677  mclsval  35679  mppsval  35688  mclsppslem  35699  opelco3  35891  wsuclem  35939  funtransport  36147  fvtransport  36148  brcolinear  36175  colineardim1  36177  funray  36256  fvray  36257  funline  36258  fvline  36260  lineelsb2  36264  fwddifval  36278  fwddifnval  36279  rankelg  36284  rankeq1o  36287  elhf2  36291  0hf  36293  rmoeqbidv  36329  disjeq12dv  36331  ixpeq12dv  36332  prodeq12sdv  36334  itgeq12sdv  36335  cbvralvw2  36342  cbvrexvw2  36343  cbvrmovw2  36344  cbvreuvw2  36345  cbvcsbvw2  36347  cbviunvw2  36348  cbviinvw2  36349  cbvmptvw2  36350  cbvdisjvw2  36351  cbvmpo1vw2  36359  cbvmpo2vw2  36360  cbvsbcdavw  36373  cbvcsbdavw  36375  cbvcsbdavw2  36376  cbviundavw  36378  cbviindavw  36379  cbvdisjdavw  36384  cbvrabdavw2  36401  cbviundavw2  36402  cbviindavw2  36403  cbvmptdavw2  36404  cbvdisjdavw2  36405  cbvriotadavw2  36406  cbvmpo1davw2  36408  cbvmpo2davw2  36409  cbvsumdavw2  36411  neibastop2lem  36476  neibastop3  36478  eltail  36490  bj-projeq  37109  bj-projval  37113  bj-restsn  37199  opelopabbv  37260  brabd0  37264  bj-eldiag  37293  bj-eldiag2  37294  mptsnunlem  37455  dissneqlem  37457  iooelexlt  37479  relowlssretop  37480  rdgellim  37493  exrecfnlem  37496  finxpeq1  37503  finxpreclem6  37513  pibp21  37532  curf  37711  uncf  37712  curunc  37715  unccur  37716  fin2so  37720  lindsadd  37726  lindsdom  37727  lindsenlbs  37728  matunitlindflem1  37729  matunitlindflem2  37730  matunitlindf  37731  ptrest  37732  ptrecube  37733  poimirlem2  37735  poimirlem8  37741  poimirlem17  37750  poimirlem18  37751  poimirlem20  37753  poimirlem21  37754  poimirlem22  37755  poimirlem24  37757  poimirlem26  37759  poimirlem29  37762  heicant  37768  mblfinlem1  37770  mblfinlem2  37771  volsupnfl  37778  itg2addnclem  37784  itg2gt0cn  37788  indexdom  37847  incsequz  37861  istotbnd  37882  istotbnd3  37884  0totbnd  37886  sstotbnd  37888  sstotbnd3  37889  isbnd  37893  prdstotbnd  37907  cntotbnd  37909  isismty  37914  heibor1lem  37922  heiborlem2  37925  heiborlem3  37926  heibor  37934  isass  37959  exidcl  37989  exidreslem  37990  elghomlem2OLD  37999  rngoidmlem  38049  rngo1cl  38052  divrngcl  38070  isdrngo2  38071  isrngohom  38078  isrngoiso  38091  isriscg  38097  iscom2  38108  iscringd  38111  isidl  38127  ispridl  38147  ismaxidl  38153  ac6s6  38285  dmecd  38415  dfpre4  38566  releldmqs  38829  releldmqscoss  38831  erimeq2  38849  eldisjlem19  38981  membpartlem19  38982  prter3  39054  islshp  39151  islsat  39163  lcvfbr  39192  islfl  39232  ellkr  39261  islshpkrN  39292  ldual1dim  39338  isopos  39352  cmtfvalN  39382  cvrfval  39440  isat  39458  islln  39678  islpln  39702  islvol  39745  isline  39911  ispointN  39914  ispsubsp  39917  elpmap  39930  elpmapat  39936  elpadd  39971  paddclN  40014  elpclN  40064  elpcliN  40065  pclfinN  40072  pclcmpatN  40073  ispsubclN  40109  iswatN  40166  islhp  40168  islaut  40255  ispautN  40271  isldil  40282  isltrn  40291  isdilN  40326  istrnN  40329  istendo  40932  dvhb1dimN  41158  erng1lem  41159  erngdvlem4-rN  41171  diaelval  41205  diaeldm  41208  dia1dimid  41235  cdlemm10N  41290  dibopelvalN  41315  dibopelval2  41317  dibelval3  41319  dibelval1st  41321  dibelval2nd  41324  dibeldmN  41330  dibvalrel  41335  dibglbN  41338  dicffval  41346  dicfval  41347  dicopelval  41349  dicelvalN  41350  dicelval3  41352  dicvalrelN  41357  dicelval1sta  41359  diclspsn  41366  dihopelvalbN  41410  dihopelvalcqat  41418  dihopelvalcpre  41420  dihvalrel  41451  dih1  41458  dihmeetlem4preN  41478  dihmeetlem13N  41491  dih1dimatlem  41501  dochnel2  41564  dihjatcclem4  41593  dvh2dim  41617  dvh3dim  41618  dvh4dimN  41619  dochfln0  41649  lpolsetN  41654  islpolN  41655  lcfrvalsnN  41713  lcfrlem21  41735  lcfrlem27  41741  lcfrlem37  41751  lcfr  41757  lcdlss  41791  mapdcv  41832  hdmap1fval  41968  hdmapffval  41998  hdmapfval  41999  hdmapval  42000  hgmapffval  42057  hgmapfval  42058  hdmapellkr  42086  hlhilhillem  42132  fzsplitnd  42148  isprimroot  42259  primrootsunit1  42263  primrootscoprmpow  42265  primrootscoprbij  42268  aks6d1c1p2  42275  aks6d1c1p3  42276  aks6d1c1p4  42277  aks6d1c1p5  42278  aks6d1c1p6  42280  aks6d1c1  42282  evl1gprodd  42283  sticksstones11  42322  sticksstones12a  42323  rhmqusspan  42351  grpods  42360  fzosumm1  42420  frlmfielbas  42670  frlmsnic  42710  psrmnd  42713  isnacs  42861  mrefg2  42864  elmzpcl  42883  mzpcompact2  42909  eldiophb  42914  elpell1qr  43004  elpell14qr  43006  elpell1234qr  43008  pw2f1ocnv  43194  pw2f1o2val2  43197  aomclem4  43214  aomclem6  43216  islssfg2  43228  imasgim  43257  lnr2i  43273  elmnc  43293  rngunsnply  43326  onexomgt  43398  onexlimgt  43400  onexoegt  43401  oaordnr  43453  omnord1  43462  oenord1  43473  cantnfresb  43481  tfsconcatun  43494  tfsconcat0i  43502  ofoaf  43512  naddcnff  43519  naddcnffo  43521  naddcnfcom  43523  naddcnfid1  43524  naddcnfid2  43525  naddcnfass  43526  naddwordnexlem4  43558  fiinfi  43730  sqrtcvallem1  43788  elintima  43810  eliunov2  43836  ov2ssiunov2  43857  brtrclfv2  43884  rfovcnvf1od  44161  rfovcnvfvd  44164  fsovrfovd  44166  fsovfvd  44167  fsovcnvlem  44170  ntrclsfv1  44212  ntrclselnel1  44214  ntrclsneine0lem  44221  ntrneifv1  44236  ntrneifv2  44237  ntrneiel  44238  gneispace2  44289  gneispacess2  44303  extoimad  44321  mnringelbased  44374  dvconstbi  44491  bccbc  44502  wfac8prim  45159  permaxrep  45163  permac8prim  45171  eliin2f  45264  iineq12dv  45266  rabbida2  45292  disjinfi  45352  unirnmap  45368  elmptima  45418  iuneqfzuzlem  45495  iooiinioc  45718  fsumiunss  45737  fsumsupp0  45740  lptre2pt  45800  icccncfext  46047  cncfiooicclem1  46053  dvnprodlem2  46107  stoweidlem27  46187  stoweidlem29  46189  stoweidlem31  46191  stoweidlem34  46194  stoweidlem48  46208  stoweidlem59  46219  dirkercncflem2  46264  dirkercncflem4  46266  fourierdlem2  46269  fourierdlem3  46270  fourierdlem25  46292  fourierdlem32  46299  fourierdlem33  46300  fourierdlem41  46308  fourierdlem48  46314  fourierdlem49  46315  fourierdlem62  46328  fourierdlem70  46336  fourierdlem80  46346  fourierdlem92  46358  fourierdlem93  46359  fourierdlem101  46367  etransclem37  46431  sge0val  46526  sge0f1o  46542  sge0iunmptlemre  46575  sge0iunmpt  46578  iundjiun  46620  caragenel  46655  ovncvrrp  46724  ovnsubaddlem1  46730  ovnsubadd  46732  hoidmvlelem2  46756  hoidmvlelem3  46757  hoidmvlelem4  46758  hoidmvle  46760  ovncvr2  46771  hspdifhsp  46776  hoiqssbl  46785  hspmbllem2  46787  hspmbl  46789  opnvonmbllem1  46792  isvonmbl  46798  ovnovollem1  46816  issmflem  46887  smflimlem3  46933  smflimlem4  46934  smflim  46937  smfmullem2  46952  smflimmpt  46970  smfsuplem1  46971  smflimsuplem1  46980  smflimsuplem3  46982  smflimsuplem4  46983  smflimsuplem7  46986  smflimsup  46988  chnsubseq  47040  fcores  47229  fcoresf1  47231  afvelrnb  47325  afvelrnb0  47326  afv2co2  47419  el1fzopredsuc  47487  iccpart  47578  iccpartgtprec  47582  iccpartiltu  47584  iccpartigtl  47585  iccpartltu  47587  iccpartgtl  47588  iccpartgt  47589  iccpartleu  47590  iccpartgel  47591  iccelpart  47595  iccpartiun  47596  icceuelpart  47598  fargshiftfv  47601  fargshiftfo  47604  sprel  47646  prprelb  47678  prprelprb  47679  fpprel  47890  sbgoldbo  47949  wtgoldbnnsum4prm  47964  bgoldbnnsum3prm  47966  bgoldbtbndlem3  47969  bgoldbtbnd  47971  clnbgrval  47984  elclnbgrelnbgr  47987  clnbgrel  47990  clnbupgrel  47996  vopnbgrel  48016  isubgredg  48028  upgrimwlklem3  48061  upgrimwlklem5  48063  upgrimpths  48071  grtriprop  48103  isgrtri  48105  grtriclwlk3  48107  stgredgel  48119  gpgvtxel  48209  gpgiedgdmel  48211  gpgedgel  48212  opgpgvtx  48217  gpg5nbgrvtx13starlem1  48233  gpg5nbgrvtx13starlem2  48234  gpg5nbgrvtx13starlem3  48235  gpg3kgrtriex  48251  grlimedgnedg  48293  upwlksfval  48297  isupwlk  48298  intop  48365  isclintop  48369  assintop  48371  isassintop  48372  assintopcllaw  48374  uzlidlring  48397  elrngchomALTV  48431  rngccatidALTV  48434  rngcsectALTV  48437  rngcisoALTV  48439  rhmsubcALTVlem3  48445  rhmsubcALTVlem4  48446  funcringcsetcALTV2lem7  48458  funcringcsetcALTV2lem9  48460  elringchomALTV  48465  ringccatidALTV  48468  ringcsectALTV  48471  ringcisoALTV  48473  ringcbasbasALTV  48474  funcringcsetclem7ALTV  48481  funcringcsetclem9ALTV  48483  srhmsubcALTV  48487  cbvmpox2  48498  ply1sclrmsm  48546  dmatALTbasel  48564  lcoval  48574  lindslinindsimp1  48619  lindslinindsimp2  48625  lmod1  48654  elbigo  48713  elbigo2  48714  elbigolo1  48719  dig2nn0ld  48766  naryfvalel  48792  rrxlines  48895  rrxlinesc  48897  rrxlinec  48898  eenglngeehlnm  48901  elrrx2linest2  48907  rrxsphere  48910  itsclc0  48933  itsclc0b  48934  itsclinecirc0  48935  itsclinecirc0b  48936  itscnhlinecirc02p  48947  brab2dd  48989  f1omo  49054  f1omoOLD  49055  lubeldm2d  49119  glbeldm2d  49120  catprs  49172  sectpropdlem  49197  nelsubc3lem  49231  initc  49252  imaid  49315  upfval  49337  upfval2  49338  upfval3  49339  uppropd  49342  oppcinito  49396  oppctermo  49397  oppczeroo  49398  initopropd  49404  termopropd  49405  isthinc  49580  isthincd2lem1  49586  thincmoALT  49590  thincmod  49591  isthincd  49597  thincpropd  49603  indcthing  49621  discthing  49622  prsthinc  49625  termcterm  49674  termc2  49679  isinito4  49708  2arwcatlem1  49756  setc1onsubc  49763  cnelsubclem  49764  ranval3  49792  lmdfval2  49816  cmdfval2  49817  termolmd  49831  elsetrecslem  49860