Theorem eleq2d 2815

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 2723	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	1, 2	sylib 218	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		anbi2 634	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	alexbii 1833	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	syl 17	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
7		dfclel 2805	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
8		dfclel 2805	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804

This theorem is referenced by:  eleq2  2818  eleq12d  2823  eleqtrd  2831  neleqtrd  2851  eqabrd  2871  raleqbidv  3321  rexeqbidv  3322  reueqbidv  3397  rabeqbidva  3425  elabd2  3639  sbcbid  3811  csbeq2d  3871  csbeq2dv  3872  cbvcsbw  3875  cbvcsb  3876  cbvcsbv  3877  csbie  3900  csbied  3901  csbie2g  3905  cbvralcsf  3907  cbvreucsf  3909  cbvrabcsf  3910  sbcel12  4377  sbcel1g  4382  sbcel2  4384  prel12g  4831  eliuni  4964  iuneqconst  4970  iuneq12df  4985  iuneq12d  4988  cbviun  5003  cbviin  5004  cbviung  5005  cbviing  5006  cbviunv  5007  cbviinv  5008  iinxsng  5055  iinxprg  5056  iunxsng  5057  iunxsngf  5059  cbvdisj  5087  cbvdisjv  5088  disjor  5092  disjiund  5101  mpteq12da  5193  mpteq12f  5195  mpteq12dva  5196  axpweq  5309  rabxfrd  5375  rbropapd  5527  opeliunxp  5708  opeliun2xp  5709  opeliunxp2  5805  iunxpf  5815  elimampt  6017  elrelimasn  6060  elimasni  6065  imadifssran  6127  xpdifid  6144  ressn  6261  funfni  6627  fnbr  6629  dffv3  6857  elfv2ex  6907  fvelrnb  6924  foelcdmi  6925  fvun1  6955  fvco2  6961  elfvmptrab1w  6998  elfvmptrab1  6999  elfvmptrab  7000  elpreima  7033  dff3  7075  fmptco  7104  fnelfp  7152  fnelnfp  7154  tpres  7178  fnprb  7185  fntpb  7186  funfvima3  7213  eluniima  7227  elunirn2OLD  7230  dff13  7232  f1ounsn  7250  f1eqcocnv  7279  isoini  7316  riotaeqdv  7348  mpoeq123dva  7466  cbvmpox  7485  elimampo  7529  ovelrn  7568  elovmpod  7636  elovmpo  7637  elovmporab  7638  elovmporab1w  7639  elovmporab1  7640  elovmpt3rab1  7652  fiun  7924  f1iun  7925  zfrep6  7936  fmpox  8049  el2mpocsbcl  8067  el2mpocl  8068  bropopvvv  8072  bropfvvvv  8074  xpord2indlem  8129  xpord3inddlem  8136  elsuppfng  8151  elsuppfn  8152  suppfnss  8171  opeliunxp2f  8192  mpoxopn0yelv  8195  mpoxopovel  8202  rntpos  8221  mpocurryd  8251  fpr2  8286  wfr2  8309  onoviun  8315  smoel  8332  smoiso  8334  smoel2  8335  smo11  8336  tfrlem9  8356  oalimcl  8527  oaass  8528  omordi  8533  omordlim  8544  omlimcl  8545  odi  8546  omeulem1  8549  omeulem2  8550  oen0  8553  oeordi  8554  oeordsuc  8561  oelimcl  8567  oeeulem  8568  oeeui  8569  nnmordi  8598  oaabs2  8616  omabs  8618  omsmolem  8624  ereldm  8727  iiner  8765  elmapg  8815  elpmg  8819  elixpsn  8913  ixpsnf1o  8914  boxriin  8916  omxpenlem  9047  pw2f1olem  9050  phplem2  9175  php3  9179  infn0  9258  elfi  9371  dffi3  9389  marypha2lem2  9394  ordiso2  9475  wemapsolem  9510  elharval  9521  inf3lemd  9587  inf3lem1  9588  inf3lem2  9589  inf3lem3  9590  cantnfs  9626  cantnfp1lem3  9640  cantnflem1b  9646  cantnflem1  9649  ttrclselem2  9686  trcl  9688  frr2  9720  r1sdom  9734  r1ordg  9738  r1pwss  9744  tz9.12lem3  9749  tz9.12  9750  r1elwf  9756  rankr1ai  9758  rankidb  9760  rankr1bg  9763  rankval2  9778  rankunb  9810  tcrank  9844  acni  10005  acni2  10006  acndom  10011  infpwfien  10022  alephnbtwn  10031  cardaleph  10049  cardinfima  10057  iunfictbso  10074  dfac3  10081  dfac5lem5  10087  dfac5  10089  dfac9  10097  dfac12r  10107  kmlem2  10112  kmlem12  10122  kmlem13  10123  kmlem14  10124  ackbij2lem3  10200  ackbij2  10202  cofsmo  10229  alephsing  10236  fin23lem30  10302  isf32lem9  10321  itunisuc  10379  axcc2lem  10396  axcc3  10398  domtriomlem  10402  axdc2lem  10408  axdc2  10409  axdc3lem2  10411  axdc3lem4  10413  axdc4lem  10415  ac6c4  10441  zorn2lem1  10456  ttukeylem6  10474  pwcfsdom  10543  axregndlem2  10563  axinfndlem1  10565  axacndlem4  10570  axacnd  10572  pwfseqlem1  10618  inar1  10735  inatsk  10738  gruurn  10758  grur1  10780  eltskm  10803  genpelv  10960  eluz1  12804  eluzaddOLD  12835  eluzsubOLD  12836  elixx1  13322  elixx3g  13326  elioo2  13354  elfz1  13480  elfz2  13482  elfzp1  13542  fzpr  13547  fzsuc2  13550  fzrev3  13558  elfzp12  13571  fzm1  13575  elfzo  13629  fz0add1fz1  13703  elfzo0l  13724  elfzom1b  13734  fzosplitsni  13746  elfzr  13748  elfzlmr  13749  zmodidfzo  13869  seqp1  13988  seqf1o  14015  bcval  14276  bcpasc  14293  hashf1lem1  14427  fundmge2nop0  14474  wrdmap  14518  elovmpowrd  14530  ccatfval  14545  elfzelfzccat  14552  ccatlid  14558  ccatass  14560  ccatrn  14561  ccatalpha  14565  swrdfv2  14633  ccatswrd  14640  swrdccat2  14641  pfxfv  14654  pfxeq  14668  ccatpfx  14673  swrdswrd  14677  swrdpfx  14679  pfxpfx  14680  cats1un  14693  swrdccatfn  14696  swrdccatin1  14697  pfxccatin12lem4  14698  pfxccatin12lem1  14700  swrdccatin2  14701  pfxccatin12lem2c  14702  pfxccatin12lem2  14703  swrdccat3blem  14711  swrdccatin1d  14715  swrdccatin2d  14716  pfxccatin12d  14717  revccat  14738  revrev  14739  repswpfx  14757  repswccat  14758  cshwidxmod  14775  2cshw  14785  cshwcshid  14800  cshwcsh2id  14801  cshimadifsn  14802  cshimadifsn0  14803  revco  14807  ccatco  14808  cshco  14809  swrdco  14810  ofccat  14942  shftfn  15046  shftval  15047  limsupgle  15450  ello12  15489  elo12  15500  isercolllem3  15640  sumeq1  15662  fsumsplit  15714  sumsplit  15741  fsum2dlem  15743  fsumcom2  15747  fsumparts  15779  explecnv  15838  pwdif  15841  fprodser  15922  fprodsplit  15939  fprod2dlem  15953  fprodcom2  15957  eftlub  16084  divalgmod  16383  bitsval  16401  bitsp1e  16409  bitsp1o  16410  sadfval  16429  sadcp1  16432  sadval  16433  sadcadd  16435  sadadd2  16437  saddisjlem  16441  sadadd  16444  sadass  16448  smufval  16454  smuval  16458  smuval2  16459  smupvallem  16460  smu01lem  16462  smueqlem  16467  smumul  16470  bezoutlem2  16517  bezoutlem4  16519  algfx  16557  eucalgcvga  16563  reumodprminv  16782  nnnn0modprm0  16784  unbenlem  16886  prmreclem5  16898  vdwapval  16951  vdwapun  16952  vdwnnlem1  16973  vdwnn  16976  ramval  16986  0ram  16998  ramub1lem2  17005  prmgaplem7  17035  prmlem0  17083  elrest  17397  prdsbasmpt  17440  prdsleval  17447  prdsbasmpt2  17452  pwselbasb  17458  imasaddfnlem  17498  imasvscafn  17507  divsfval  17517  ismre  17558  mreunirn  17569  mrisval  17598  ismri  17599  isacs  17619  catidd  17648  iscatd2  17649  ismon  17702  isepi  17709  sectffval  17719  sectfval  17720  dfiso2  17741  cicsym  17773  issubc  17804  catsubcat  17808  isfunc  17833  funcres  17865  funcpropd  17871  ffthiso  17900  isnat  17919  isnat2  17920  fuciso  17947  initoval  17962  termoval  17963  isinito  17965  istermo  17966  iszeroo  17967  isinitoi  17968  istermoi  17969  initoid  17970  termoid  17971  iszeroi  17978  2initoinv  17979  initoeu1  17980  initoeu2  17985  2termoinv  17986  termoeu1  17987  arwhoma  18014  elsetchom  18050  setcmon  18056  setcepi  18057  setciso  18060  catciso  18080  elestrchom  18096  estrcbasbas  18099  funcestrcsetclem7  18114  funcestrcsetclem8  18115  funcestrcsetclem9  18116  fthestrcsetc  18118  fullestrcsetc  18119  equivestrcsetc  18120  setc1strwun  18121  funcsetcestrclem7  18129  funcsetcestrclem8  18130  funcsetcestrclem9  18131  fthsetcestrc  18133  fullsetcestrc  18134  hofcl  18227  hofpropd  18235  yonedalem4c  18245  yonedainv  18249  yonffthlem  18250  lubeldm  18319  glbeldm  18332  joindef  18342  meetdef  18356  poslubdg  18380  acsficl2d  18518  acsmapd  18520  psref  18540  psss  18546  dirge  18569  mgmpropd  18585  issstrmgm  18587  grpidval  18595  grpidpropd  18596  grpidd  18605  ismgmhm  18630  issubmgm  18636  issgrpd  18664  sgrppropd  18665  ismndd  18690  mndpropd  18693  imasmnd2  18708  imasmnd  18709  xpsmnd0  18712  ismhm  18719  issubm  18737  gsumsgrpccat  18774  elefmndbas2  18808  smndex1mndlem  18843  imasgrp2  18994  imasgrp  18995  issubg  19065  subginv  19072  isnsg  19094  eqg0el  19122  quselbas  19123  isghm  19154  isghmOLD  19155  resghm2b  19173  conjnmzb  19192  conjnsg  19193  ghmpropd  19195  isga  19230  elcntz  19261  elcntzsn  19264  cntzrcl  19266  resscntz  19272  symgextf1  19358  gsmsymgreqlem2  19368  f1otrspeq  19384  pmtrfrn  19395  pmtrdifellem3  19415  pmtrdifellem4  19416  psgnunilem1  19430  psgnunilem5  19431  psgnunilem2  19432  psgnunilem3  19433  psgneldm2  19441  psgnfitr  19454  psgnsn  19457  gexdvds  19521  gex1  19528  isslw  19545  sylow3lem2  19565  lsmelvalx  19577  pj1ghm  19640  efgtlen  19663  efgsfo  19676  efgredlemc  19682  frgp0  19697  frgpmhm  19702  qusabl  19802  frgpnabllem1  19810  imasabl  19813  cycsubmcmn  19826  0cyg  19830  cycsubgcyg  19838  gsumval3  19844  gsumcllem  19845  gsumzaddlem  19858  gsumzsplit  19864  gsummptfzcl  19906  eldprd  19943  dprdcntz2  19977  dprd2d2  19983  dmdprdsplit2lem  19984  dmdprdsplit2  19985  dprdsplit  19987  ablfac2  20028  isrngd  20089  rngpropd  20090  imasrng  20093  qusrng  20096  ringurd  20101  isringd  20207  imasring  20246  xpsring1d  20249  dvdsrval  20277  isunit  20289  dvdsrpropd  20332  isirred  20335  isrnghm  20357  isrngim  20361  c0ghm  20377  c0snghm  20380  isrhm  20394  isrim0OLD  20397  isrim0  20399  islring  20456  issubrng  20463  opprsubrng  20475  issubrg  20487  opprsubrg  20509  resrhm2b  20518  rhmpropd  20525  rnghmresel  20536  elrngchom  20540  rnghmsubcsetclem1  20547  rnghmsubcsetclem2  20548  rngcid  20551  rngcsect  20552  rngciso  20554  funcrngcsetcALT  20557  zrinitorngc  20558  zrtermorngc  20559  rhmresel  20565  elringchom  20569  rhmsubcsetclem1  20576  rhmsubcsetclem2  20577  ringcid  20580  rhmsscrnghm  20581  rhmsubcrngclem1  20582  rhmsubcrngclem2  20583  ringcsect  20586  ringciso  20588  ringcbasbas  20589  zrtermoringc  20591  srhmsubc  20596  rhmsubclem3  20603  rhmsubclem4  20604  drngunit  20650  isdrngd  20681  isdrngdOLD  20683  issdrg  20704  sdrgunit  20712  isabv  20727  issrngd  20771  islmod  20777  lmodprop2d  20837  islss  20847  islssd  20848  lssats2  20913  ellspsn  20916  islmhm  20941  lmhmf1o  20960  lmhmima  20961  lmhmpreima  20962  reslmhm  20966  pwssplit3  20975  lmhmpropd  20987  islbs  20990  lspprel  21008  lspfixed  21045  lbsacsbs  21073  lbsextlem1  21075  lbsextlem2  21076  lbsextlem3  21077  lbsextlem4  21078  ixpsnbasval  21122  isridlrng  21136  rnglidlmmgm  21162  isridl  21169  quscrng  21200  rngqiprngimfolem  21207  rngqiprngimf1lem  21211  rngqiprngimfo  21218  islpidl  21242  lidldvgen  21251  irinitoringc  21396  pzriprnglem13  21410  pzriprnglem14  21411  zrhrhmb  21427  znf1o  21468  frgpcyg  21490  psgnevpmb  21503  isphld  21570  phlssphl  21575  elocv  21584  iscss  21599  isobs  21636  obs2ss  21645  dsmmfi  21654  dsmmelbas  21655  dsmmlss  21660  frlmelbas  21672  frlmlbs  21713  frlmup1  21714  ellspd  21718  islinds  21725  islindf2  21730  f1lindf  21738  islindf4  21754  assamulgscmlem2  21816  psrgrp  21872  mplsubglem  21915  mpllsslem  21916  mplmonmul  21950  subrgascl  21980  subrgasclcl  21981  mpfind  22021  ismhp  22034  gsumply1subr  22125  lply1binomsc  22205  matbas2d  22317  matecl  22319  matvscl  22325  mat1  22341  mat0dim0  22361  mat0dimid  22362  mat0dimscm  22363  mat1dimelbas  22365  dmatel  22387  scmatel  22399  scmateALT  22406  scmataddcl  22410  scmatsubcl  22411  smatvscl  22418  scmatghm  22427  mat1scmat  22433  mdetunilem7  22512  mdetunilem9  22514  smadiadetr  22569  cramerimplem2  22578  cramer0  22584  pmatcoe1fsupp  22595  cpmatpmat  22604  cpmatel  22605  cpmatacl  22610  cpmatinvcl  22611  mat2pmatghm  22624  mat2pmatmul  22625  decpmatmullem  22665  pmatcollpwlem  22674  pmatcollpw3fi1lem1  22680  pmatcollpwscmatlem1  22683  monmat2matmon  22718  chfacfscmul0  22752  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  cayhamlem1  22760  cpmadugsumlemB  22768  cpmadugsumlemC  22769  cpmadugsumlemF  22770  cayhamlem2  22778  istopon  22806  eltg  22851  eltg2  22852  eltop  22868  eltop2  22869  eltop3  22870  pptbas  22902  iscld  22921  neiss2  22995  isnei  22997  neiptopnei  23026  neiptopreu  23027  lpfval  23032  lpval  23033  islp  23034  maxlp  23041  islpi  23043  neitr  23074  restlp  23077  ordtbas2  23085  ordtrest2  23098  lmfval  23126  cnfval  23127  iscn  23129  iscnp  23131  tgcn  23146  tgcnp  23147  lmbrf  23154  cnpresti  23182  ist1  23215  ist1-2  23241  cnt1  23244  haust1  23246  cmpfi  23302  cmpfii  23303  1stcfb  23339  2ndc1stc  23345  1stcrest  23347  2ndcdisj  23350  1stcelcls  23355  nllyi  23369  subislly  23375  islocfin  23411  lfinpfin  23418  locfindis  23424  locfincf  23425  comppfsc  23426  kgenval  23429  elkgen  23430  kgencn2  23451  txbas  23461  eltx  23462  ptval  23464  ptpjpre1  23465  ptopn2  23478  ptpjopn  23506  ptclsg  23509  xkoccn  23513  txdis  23526  txdis1cn  23529  ptrescn  23533  hausdiag  23539  hauseqlcld  23540  txhaus  23541  xkohaus  23547  elqtop  23591  qtopeu  23610  kqcldsat  23627  hmeofval  23652  ptuncnv  23701  ptunhmeo  23702  elmptrab  23721  fbdmn0  23728  elfg  23765  elfilss  23770  filunirn  23776  fixufil  23816  elfm  23841  rnelfmlem  23846  rnelfm  23847  fmfnfmlem4  23851  elflim2  23858  flimtopon  23864  elflim  23865  hausflim  23875  flimcls  23879  flfnei  23885  isflf  23887  hausflf  23891  cnpflf  23895  cnflf  23896  txflf  23900  isfcls  23903  fclstopon  23906  isfcls2  23907  fclssscls  23912  fclsnei  23913  fclsfnflim  23921  flimfnfcls  23922  isfcf  23928  fcfelbas  23930  cnpfcf  23935  cnfcf  23936  flfcntr  23937  alexsublem  23938  alexsubALTlem3  23943  cnextfun  23958  cnextfvval  23959  cnextf  23960  cnextcn  23961  tmdgsum2  23990  tgpconncomp  24007  ghmcnp  24009  qustgplem  24015  eltsms  24027  haustsms  24030  tsmsgsum  24033  tsmssubm  24037  tsmssplit  24046  isust  24098  ustbas  24122  elutop  24128  ustuqtoplem  24134  ustuqtop4  24139  ustuqtop  24141  utopsnneiplem  24142  utopsnneip  24143  utopsnnei  24144  isusp  24156  isucn  24172  ucncn  24179  iscfilu  24182  neipcfilu  24190  iscusp  24193  cnextucn  24197  ispsmet  24199  ismet  24218  isxmet  24219  elblps  24282  elbl  24283  elmopn  24337  prdsbl  24386  neibl  24396  met1stc  24416  metrest  24419  prdsxmslem2  24424  txmetcnp  24442  txmetcn  24443  metustsym  24450  cfilucfil2  24456  elbl4  24458  metuel  24459  psmetutop  24462  restmetu  24465  metucn  24466  tngngp  24549  isnmhm  24641  zcld  24709  metnrmlem1a  24754  elcncf  24789  cncfcnvcn  24826  cnheibor  24861  lebnumlem1  24867  ishtpy  24878  isphtpy  24887  om1elbas  24939  elpi1  24952  pi1xfr  24962  pi1coghm  24968  tcphcph  25144  lmmbrf  25169  iscfil  25172  iscau  25183  iscauf  25187  caucfil  25190  iscmet  25191  cmetcaulem  25195  iscmet3lem1  25198  iscmet3lem2  25199  iscmet3  25200  bcthlem1  25231  cmsss  25258  cmetcusp1  25260  cmetcusp  25261  cmscsscms  25280  rrxcph  25299  minveclem3b  25335  ovolfioo  25375  ovolficc  25376  ovolctb  25398  ovoliunnul  25415  ovolshftlem1  25417  sca2rab  25420  ovolscalem1  25421  ovolicc2lem1  25425  ovolicc2lem2  25426  ovolicc2lem4  25428  ovolicc2lem5  25429  iundisj  25456  iunmbl2  25465  uniioombllem3  25493  vitalilem2  25517  vitalilem3  25518  mbfss  25554  i1faddlem  25601  i1fmullem  25602  mbfi1fseqlem2  25624  mbfi1fseqlem4  25626  mbfi1fseq  25629  itg2splitlem  25656  itg2split  25657  itg2monolem1  25658  itg2gt0  25668  isibl  25673  iblss2  25714  itgss3  25723  itgsplit  25744  ellimc  25781  limcmo  25790  cnlimc  25796  limciun  25802  limcun  25803  eldv  25806  dvbsss  25810  dvreslem  25817  elcpn  25843  dvaddf  25852  dvmulf  25853  dvcof  25859  rolle  25901  dvlip2  25907  dvivthlem1  25920  lhop1  25926  lhop2  25927  ftc1cn  25957  fta1glem2  26081  plyco0  26104  elply  26107  ply1termlem  26115  eltayl  26274  tayl0  26276  taylplem1  26277  taylplem2  26278  dvtaylp  26285  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  abelth  26358  cxpcn3  26665  rlimcnp  26882  fsumharmonic  26929  dchrelbas  27154  pntrsumbnd2  27485  ostth2lem2  27552  nolesgn2ores  27591  nogesgn1ores  27593  nosupprefixmo  27619  noinfprefixmo  27620  nosupcbv  27621  nosupdm  27623  nosupfv  27625  nosupres  27626  nosupbnd1lem1  27627  nosupbnd1lem3  27629  nosupbnd1lem5  27631  nosupbnd2lem1  27634  noinfcbv  27636  noinfdm  27638  noinffv  27640  noinfres  27641  noinfbnd1lem1  27642  noinfbnd1lem3  27644  noinfbnd1lem5  27646  noinfbnd2lem1  27649  elmade  27786  elold  27788  ssltleft  27789  ssltright  27790  oldlim  27805  madebday  27818  newbday  27820  sltlpss  27826  cofcutr  27839  cofcutrtime  27842  lrrecval  27853  lrrecval2  27854  addsval  27876  precsexlem9  28124  precsexlem11  28126  sltonold  28169  onnolt  28174  onslt  28175  noseqrdgfn  28207  istrkgb  28389  istrkgcb  28390  istrkge  28391  istrkgl  28392  istrkgld  28393  axtgsegcon  28398  axtg5seg  28399  axtgbtwnid  28400  axtgpasch  28401  axtgupdim2  28405  axtgeucl  28406  tgdim01  28441  iscgrg  28446  isismt  28468  tglnunirn  28482  tglngval  28485  tgellng  28487  legval  28518  legov  28519  legov2  28520  ishlg  28536  mirreu3  28588  mirval  28589  mirfv  28590  mircgr  28591  mirbtwn  28592  ismir  28593  mireq  28599  symquadlem  28623  israg  28631  perpln1  28644  perpln2  28645  isperp  28646  islnopp  28673  outpasch  28689  ishpg  28693  iscgra  28743  dfcgra2  28764  isinag  28772  isleag  28781  iseqlg  28801  f1otrgitv  28804  f1otrg  28805  f1otrge  28806  ttgval  28809  ttgelitv  28817  elee  28828  brbtwn  28833  brcgr  28834  axlowdimlem16  28891  ebtwntg  28916  elntg2  28919  upgrex  29026  edgupgr  29068  upgredg  29071  edglnl  29077  numedglnl  29078  uhgr2edg  29142  umgr2edg1  29145  usgredg2vlem1  29159  usgredg2vlem2  29160  ushgredgedg  29163  ushgredgedgloop  29165  uhgrspansubgrlem  29224  fusgrfisstep  29263  nbgrval  29270  nbgrel  29274  nbupgrel  29279  nbgr2vtx1edg  29284  nbuhgr2vtx1edgblem  29285  nbuhgr2vtx1edgb  29286  nbusgreledg  29287  usgrnbcnvfv  29299  uvtxval  29321  uvtxel  29322  uvtx01vtx  29331  uvtxusgrel  29337  nbcplgr  29368  cplgr3v  29369  cusgrexi  29377  structtocusgr  29380  vtxdgfval  29402  vtxdg0v  29408  vtxdeqd  29412  vtxdun  29416  1loopgrnb0  29437  1loopgrvd0  29439  1hevtxdg0  29440  1hevtxdg1  29441  1egrvtxdg1  29444  umgr2v2evtxel  29457  umgr2v2enb1  29461  umgr2v2evd2  29462  vtxdginducedm1lem4  29477  vtxdginducedm1  29478  finsumvtxdg2sstep  29484  ewlksfval  29536  isewlk  29537  wksfval  29544  iswlk  29545  uspgr2wlkeq  29581  wlkres  29605  dfpth2  29666  usgr2pthlem  29700  clwlkcompim  29717  uspgrn2crct  29745  wwlks  29772  iswwlksn  29775  wwlknvtx  29782  wlkiswwlks2  29812  wwlksm1edg  29818  wwlksnred  29829  wwlksnext  29830  wwlksnredwwlkn  29832  wwlksnredwwlkn0  29833  wwlksnwwlksnon  29852  wspn0  29861  usgr2wspthons3  29901  rusgrnumwwlkb0  29908  clwwlk  29919  clwwlkccatlem  29925  clwlkclwwlklem2a4  29933  clwlkclwwlk  29938  clwwisshclwwslem  29950  clwwlkinwwlk  29976  clwwlkel  29982  clwwlkf  29983  clwwlkext2edg  29992  wwlksext2clwwlk  29993  wwlksubclwwlk  29994  clwwnisshclwwsn  29995  eleclclwwlknlem2  29997  erclwwlknsym  30006  erclwwlkntr  30007  umgrhashecclwwlk  30014  clwwlkvbij  30049  eupth2lem3lem3  30166  eupth2lem3lem4  30167  eupth2lem3lem6  30169  eupth2lemb  30173  eucrct2eupth  30181  fusgreg2wsplem  30269  2clwwlklem  30279  2clwwlk2clwwlklem  30282  2clwwlkel  30285  2clwwlk2clwwlk  30286  extwwlkfabel  30289  clwwlknonclwlknonf1o  30298  dlwwlknondlwlknonf1olem1  30300  numclwwlk2lem1  30312  numclwlk2lem2f  30313  numclwlk2lem2f1o  30315  ex-res  30377  isssp  30660  sspn  30672  islno  30689  isblo  30718  nmlno0  30731  ishmo  30747  dipdir  30778  dipass  30781  ubthlem1  30806  ubthlem2  30807  htthlem  30853  htth  30854  ocel  31217  ocnel  31234  shsel  31250  shsel2  31258  shmodsi  31325  pjhtheu  31330  pjeq  31335  axpjpj  31356  pjoc2  31375  elspani  31479  h1de2ctlem  31491  elspansn  31502  elspansn2  31503  elnlfn  31864  eleigvec  31893  riesz3i  31998  cbviunf  32491  iuneq12daf  32492  iunrdx  32499  iunrnmptss  32501  cbvdisjf  32507  disjorf  32515  disjabrex  32518  disjabrexf  32519  iundisjf  32525  disjrdx  32527  brab2d  32542  2ndresdju  32580  abfmpunirn  32583  abfmpeld  32585  abfmpel  32586  fmptcof2  32588  acunirnmpt2  32591  acunirnmpt2f  32592  aciunf1lem  32593  funcnvmpt  32598  suppss3  32654  fpwrelmap  32663  xrofsup  32697  iundisjfi  32726  eliccioo  32858  s3f1  32875  ccatf1  32877  ccatws1f1o  32880  swrdrn3  32884  ismnt  32916  mgcoval  32919  chnccats1  32948  gsummpt2co  32995  gsumpart  33004  gsumhashmul  33008  xrge0tsmsbi  33010  gsumwrd2dccatlem  33013  gsumwrd2dccat  33014  cycpmco2  33097  cyc3co2  33104  isfxp  33132  cntrval2  33135  inftmrel  33141  isinftm  33142  isslmd  33162  urpropd  33190  elrgspn  33204  erlval  33216  rlocval  33217  rloccring  33228  rloc1r  33230  domnpropd  33234  isdrng4  33252  fracfld  33265  resv1r  33318  ellspds  33346  ellpi  33351  lbslsp  33355  rhmimaidl  33410  isprmidl  33416  qsidomlem1  33430  qsidomlem2  33431  ismxidl  33440  crngmxidl  33447  drng0mxidl  33454  opprqus0g  33468  qsfld  33476  isrprm  33495  rsprprmprmidlb  33501  ressply1evls1  33541  ply1mulrtss  33557  dimpropd  33611  lbslsat  33619  extdg1id  33668  fldextrspunlsplem  33675  fldextrspunlsp  33676  elirng  33688  ply1annidllem  33698  constrsuc  33735  constrconj  33742  constrllcllem  33749  constrlccllem  33750  constrcccllem  33751  nn0constr  33758  smatrcl  33793  smatcl  33799  ist0cld  33830  txomap  33831  locfinreflem  33837  zarclsiin  33868  zart0  33876  rhmpreimacnlem  33881  metidval  33887  cnre2csqima  33908  ordtrest2NEW  33920  fmcncfil  33928  fsumcvg4  33947  ofcfval  34095  measvuni  34211  meascnbl  34216  faeval  34243  ismbfm  34248  elunirnmbfm  34249  imambfm  34260  elcarsg  34303  itgeq12dv  34324  issibf  34331  eulerpartlems  34358  eulerpartlemgc  34360  eulerpartlemgvv  34374  eulerpartlemgu  34375  eulerpart  34380  rrvmbfm  34440  elorvc  34458  elorrvc  34462  dstfrvunirn  34473  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemsima  34514  ballotlemrv  34518  fzssfzo  34537  signstfvn  34567  signstfvneq0  34570  signstres  34573  repr0  34609  reprinrn  34616  reprdifc  34625  hgt750lemg  34652  hgt750lemb  34654  istrkg2d  34664  axtgupdim2ALTV  34666  afsval  34669  brafs  34670  bnj945  34770  bnj1400  34832  bnj18eq1  34924  bnj916  34930  bnj1014  34958  bnj1015  34959  bnj1110  34979  bnj1417  35038  onvf1odlem3  35099  vonf1owev  35102  revpfxsfxrev  35110  cplgredgex  35115  pfxwlk  35118  revwlk  35119  subfacp1lem2b  35175  subfacp1lem4  35177  subfacp1lem5  35178  subfacp1lem6  35179  ptpconn  35227  cvmscbv  35252  iscvm  35253  cvmsi  35259  cvmsval  35260  cvmliftmolem1  35275  cvmlift2lem12  35308  cvmlift2lem13  35309  cvmlift3lem7  35319  snmlval  35325  satfv1  35357  satfvsucsuc  35359  satfrnmapom  35364  satf0op  35371  satf0n0  35372  sat1el2xp  35373  fmlafvel  35379  isfmlasuc  35382  fmlaomn0  35384  gonan0  35386  goaln0  35387  gonar  35389  goalr  35391  satffunlem1lem2  35397  satffunlem2lem2  35400  satfv0fvfmla0  35407  satef  35410  satefvfmla0  35412  sategoelfvb  35413  satfv1fvfmla1  35417  mrsubfval  35502  mrsubvrs  35516  mclsrcl  35555  mclsval  35557  mppsval  35566  mclsppslem  35577  opelco3  35769  wsuclem  35820  funtransport  36026  fvtransport  36027  brcolinear  36054  colineardim1  36056  funray  36135  fvray  36136  funline  36137  fvline  36139  lineelsb2  36143  fwddifval  36157  fwddifnval  36158  rankelg  36163  rankeq1o  36166  elhf2  36170  0hf  36172  rmoeqbidv  36208  disjeq12dv  36210  ixpeq12dv  36211  prodeq12sdv  36213  itgeq12sdv  36214  cbvralvw2  36221  cbvrexvw2  36222  cbvrmovw2  36223  cbvreuvw2  36224  cbvcsbvw2  36226  cbviunvw2  36227  cbviinvw2  36228  cbvmptvw2  36229  cbvdisjvw2  36230  cbvmpo1vw2  36238  cbvmpo2vw2  36239  cbvsbcdavw  36252  cbvcsbdavw  36254  cbvcsbdavw2  36255  cbviundavw  36257  cbviindavw  36258  cbvdisjdavw  36263  cbvrabdavw2  36280  cbviundavw2  36281  cbviindavw2  36282  cbvmptdavw2  36283  cbvdisjdavw2  36284  cbvriotadavw2  36285  cbvmpo1davw2  36287  cbvmpo2davw2  36288  cbvsumdavw2  36290  neibastop2lem  36355  neibastop3  36357  eltail  36369  bj-projeq  36987  bj-projval  36991  bj-restsn  37077  opelopabbv  37138  brabd0  37142  bj-eldiag  37171  bj-eldiag2  37172  mptsnunlem  37333  dissneqlem  37335  iooelexlt  37357  relowlssretop  37358  rdgellim  37371  exrecfnlem  37374  finxpeq1  37381  finxpreclem6  37391  pibp21  37410  curf  37599  uncf  37600  curunc  37603  unccur  37604  fin2so  37608  lindsadd  37614  lindsdom  37615  lindsenlbs  37616  matunitlindflem1  37617  matunitlindflem2  37618  matunitlindf  37619  ptrest  37620  ptrecube  37621  poimirlem2  37623  poimirlem8  37629  poimirlem17  37638  poimirlem18  37639  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem24  37645  poimirlem26  37647  poimirlem29  37650  heicant  37656  mblfinlem1  37658  mblfinlem2  37659  volsupnfl  37666  itg2addnclem  37672  itg2gt0cn  37676  indexdom  37735  incsequz  37749  istotbnd  37770  istotbnd3  37772  0totbnd  37774  sstotbnd  37776  sstotbnd3  37777  isbnd  37781  prdstotbnd  37795  cntotbnd  37797  isismty  37802  heibor1lem  37810  heiborlem2  37813  heiborlem3  37814  heibor  37822  isass  37847  exidcl  37877  exidreslem  37878  elghomlem2OLD  37887  rngoidmlem  37937  rngo1cl  37940  divrngcl  37958  isdrngo2  37959  isrngohom  37966  isrngoiso  37979  isriscg  37985  iscom2  37996  iscringd  37999  isidl  38015  ispridl  38035  ismaxidl  38041  ac6s6  38173  dmecd  38299  releldmqs  38657  releldmqscoss  38659  erimeq2  38677  eldisjlem19  38809  membpartlem19  38810  prter3  38882  islshp  38979  islsat  38991  lcvfbr  39020  islfl  39060  ellkr  39089  islshpkrN  39120  ldual1dim  39166  isopos  39180  cmtfvalN  39210  cvrfval  39268  isat  39286  islln  39507  islpln  39531  islvol  39574  isline  39740  ispointN  39743  ispsubsp  39746  elpmap  39759  elpmapat  39765  elpadd  39800  paddclN  39843  elpclN  39893  elpcliN  39894  pclfinN  39901  pclcmpatN  39902  ispsubclN  39938  iswatN  39995  islhp  39997  islaut  40084  ispautN  40100  isldil  40111  isltrn  40120  isdilN  40155  istrnN  40158  istendo  40761  dvhb1dimN  40987  erng1lem  40988  erngdvlem4-rN  41000  diaelval  41034  diaeldm  41037  dia1dimid  41064  cdlemm10N  41119  dibopelvalN  41144  dibopelval2  41146  dibelval3  41148  dibelval1st  41150  dibelval2nd  41153  dibeldmN  41159  dibvalrel  41164  dibglbN  41167  dicffval  41175  dicfval  41176  dicopelval  41178  dicelvalN  41179  dicelval3  41181  dicvalrelN  41186  dicelval1sta  41188  diclspsn  41195  dihopelvalbN  41239  dihopelvalcqat  41247  dihopelvalcpre  41249  dihvalrel  41280  dih1  41287  dihmeetlem4preN  41307  dihmeetlem13N  41320  dih1dimatlem  41330  dochnel2  41393  dihjatcclem4  41422  dvh2dim  41446  dvh3dim  41447  dvh4dimN  41448  dochfln0  41478  lpolsetN  41483  islpolN  41484  lcfrvalsnN  41542  lcfrlem21  41564  lcfrlem27  41570  lcfrlem37  41580  lcfr  41586  lcdlss  41620  mapdcv  41661  hdmap1fval  41797  hdmapffval  41827  hdmapfval  41828  hdmapval  41829  hgmapffval  41886  hgmapfval  41887  hdmapellkr  41915  hlhilhillem  41961  fzsplitnd  41977  isprimroot  42088  primrootsunit1  42092  primrootscoprmpow  42094  primrootscoprbij  42097  aks6d1c1p2  42104  aks6d1c1p3  42105  aks6d1c1p4  42106  aks6d1c1p5  42107  aks6d1c1p6  42109  aks6d1c1  42111  evl1gprodd  42112  sticksstones11  42151  sticksstones12a  42152  rhmqusspan  42180  grpods  42189  fzosumm1  42245  frlmfielbas  42495  frlmsnic  42535  psrmnd  42540  isnacs  42699  mrefg2  42702  elmzpcl  42721  mzpcompact2  42747  eldiophb  42752  elpell1qr  42842  elpell14qr  42844  elpell1234qr  42846  pw2f1ocnv  43033  pw2f1o2val2  43036  aomclem4  43053  aomclem6  43055  islssfg2  43067  imasgim  43096  lnr2i  43112  elmnc  43132  rngunsnply  43165  onexomgt  43237  onexlimgt  43239  onexoegt  43240  oaordnr  43292  omnord1  43301  oenord1  43312  cantnfresb  43320  tfsconcatun  43333  tfsconcat0i  43341  ofoaf  43351  naddcnff  43358  naddcnffo  43360  naddcnfcom  43362  naddcnfid1  43363  naddcnfid2  43364  naddcnfass  43365  naddwordnexlem4  43397  fiinfi  43569  sqrtcvallem1  43627  elintima  43649  eliunov2  43675  ov2ssiunov2  43696  brtrclfv2  43723  rfovcnvf1od  44000  rfovcnvfvd  44003  fsovrfovd  44005  fsovfvd  44006  fsovcnvlem  44009  ntrclsfv1  44051  ntrclselnel1  44053  ntrclsneine0lem  44060  ntrneifv1  44075  ntrneifv2  44076  ntrneiel  44077  gneispace2  44128  gneispacess2  44142  extoimad  44160  mnringelbased  44213  dvconstbi  44330  bccbc  44341  wfac8prim  44999  permaxrep  45003  permac8prim  45011  eliin2f  45105  iineq12dv  45107  rabbida2  45133  disjinfi  45193  unirnmap  45209  elmptima  45259  iuneqfzuzlem  45337  iooiinioc  45561  fsumiunss  45580  fsumsupp0  45583  lptre2pt  45645  icccncfext  45892  cncfiooicclem1  45898  dvnprodlem2  45952  stoweidlem27  46032  stoweidlem29  46034  stoweidlem31  46036  stoweidlem34  46039  stoweidlem48  46053  stoweidlem59  46064  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem2  46114  fourierdlem3  46115  fourierdlem25  46137  fourierdlem32  46144  fourierdlem33  46145  fourierdlem41  46153  fourierdlem48  46159  fourierdlem49  46160  fourierdlem62  46173  fourierdlem70  46181  fourierdlem80  46191  fourierdlem92  46203  fourierdlem93  46204  fourierdlem101  46212  etransclem37  46276  sge0val  46371  sge0f1o  46387  sge0iunmptlemre  46420  sge0iunmpt  46423  iundjiun  46465  caragenel  46500  ovncvrrp  46569  ovnsubaddlem1  46575  ovnsubadd  46577  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  hoidmvle  46605  ovncvr2  46616  hspdifhsp  46621  hoiqssbl  46630  hspmbllem2  46632  hspmbl  46634  opnvonmbllem1  46637  isvonmbl  46643  ovnovollem1  46661  issmflem  46732  smflimlem3  46778  smflimlem4  46779  smflim  46782  smfmullem2  46797  smflimmpt  46815  smfsuplem1  46816  smflimsuplem1  46825  smflimsuplem3  46827  smflimsuplem4  46828  smflimsuplem7  46831  smflimsup  46833  tworepnotupword  46891  fcores  47072  fcoresf1  47074  afvelrnb  47168  afvelrnb0  47169  afv2co2  47262  el1fzopredsuc  47330  iccpart  47421  iccpartgtprec  47425  iccpartiltu  47427  iccpartigtl  47428  iccpartltu  47430  iccpartgtl  47431  iccpartgt  47432  iccpartleu  47433  iccpartgel  47434  iccelpart  47438  iccpartiun  47439  icceuelpart  47441  fargshiftfv  47444  fargshiftfo  47447  sprel  47489  prprelb  47521  prprelprb  47522  fpprel  47733  sbgoldbo  47792  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  bgoldbtbndlem3  47812  bgoldbtbnd  47814  clnbgrval  47827  elclnbgrelnbgr  47830  clnbgrel  47833  clnbupgrel  47839  vopnbgrel  47858  isubgredg  47870  upgrimwlklem3  47903  upgrimwlklem5  47905  upgrimpths  47913  grtriprop  47944  isgrtri  47946  grtriclwlk3  47948  stgredgel  47960  gpgvtxel  48042  gpgiedgdmel  48044  gpgedgel  48045  opgpgvtx  48050  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  gpg3kgrtriex  48084  upwlksfval  48127  isupwlk  48128  intop  48195  isclintop  48199  assintop  48201  isassintop  48202  assintopcllaw  48204  uzlidlring  48227  elrngchomALTV  48261  rngccatidALTV  48264  rngcsectALTV  48267  rngcisoALTV  48269  rhmsubcALTVlem3  48275  rhmsubcALTVlem4  48276  funcringcsetcALTV2lem7  48288  funcringcsetcALTV2lem9  48290  elringchomALTV  48295  ringccatidALTV  48298  ringcsectALTV  48301  ringcisoALTV  48303  ringcbasbasALTV  48304  funcringcsetclem7ALTV  48311  funcringcsetclem9ALTV  48313  srhmsubcALTV  48317  cbvmpox2  48328  ply1sclrmsm  48376  dmatALTbasel  48395  lcoval  48405  lindslinindsimp1  48450  lindslinindsimp2  48456  lmod1  48485  elbigo  48544  elbigo2  48545  elbigolo1  48550  dig2nn0ld  48597  naryfvalel  48623  rrxlines  48726  rrxlinesc  48728  rrxlinec  48729  eenglngeehlnm  48732  elrrx2linest2  48738  rrxsphere  48741  itsclc0  48764  itsclc0b  48765  itsclinecirc0  48766  itsclinecirc0b  48767  itscnhlinecirc02p  48778  brab2dd  48820  f1omo  48885  f1omoOLD  48886  lubeldm2d  48950  glbeldm2d  48951  catprs  49004  sectpropdlem  49029  nelsubc3lem  49063  initc  49084  imaid  49147  upfval  49169  upfval2  49170  upfval3  49171  uppropd  49174  oppcinito  49228  oppctermo  49229  oppczeroo  49230  initopropd  49236  termopropd  49237  isthinc  49412  isthincd2lem1  49418  thincmoALT  49422  thincmod  49423  isthincd  49429  thincpropd  49435  indcthing  49453  discthing  49454  prsthinc  49457  termcterm  49506  termc2  49511  isinito4  49540  2arwcatlem1  49588  setc1onsubc  49595  cnelsubclem  49596  ranval3  49624  lmdfval2  49648  cmdfval2  49649  termolmd  49663  elsetrecslem  49692