Theorem eleq2d 2830

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  eleq2  2833  eleq12d  2838  eleqtrd  2846  neleqtrd  2866  eqabrd  2887  drnfc1OLD  2929  drnfc2OLD  2931  raleqbidv  3354  rexeqbidv  3355  rabeqbidva  3460  elabd2  3683  sbcbid  3863  csbeq2d  3927  csbeq2dv  3928  cbvcsbw  3931  cbvcsb  3932  cbvcsbv  3933  csbie  3957  csbied  3959  csbie2g  3964  cbvralcsf  3966  cbvreucsf  3968  cbvrabcsf  3969  sbcel12  4434  sbcel1g  4439  sbcel2  4441  prel12g  4888  eliuni  5021  iuneqconst  5026  iuneq12df  5041  iuneq12d  5044  cbviun  5059  cbviin  5060  cbviung  5061  cbviing  5062  cbviunv  5063  cbviinv  5064  iinxsng  5111  iinxprg  5112  iunxsng  5113  iunxsngf  5115  cbvdisj  5143  cbvdisjv  5144  disjor  5148  disjiund  5157  mpteq12da  5251  mpteq12dfOLD  5253  mpteq12f  5254  mpteq12dva  5255  axpweq  5369  rabxfrd  5435  rbropapd  5583  opeliunxp  5767  opeliunxp2  5863  iunxpf  5873  elimampt  6072  elrelimasn  6115  elimasngOLD  6120  elimasni  6121  xpdifid  6199  ressn  6316  funfni  6685  fnbr  6687  dffv3  6916  elfv2ex  6966  fvelrnb  6982  foelcdmi  6983  fvun1  7013  fvco2  7019  elfvmptrab1w  7056  elfvmptrab1  7057  elfvmptrab  7058  elpreima  7091  dff3  7134  fmptco  7163  fnelfp  7209  fnelnfp  7211  tpres  7238  fnprb  7245  fntpb  7246  funfvima3  7273  eluniima  7287  elunirn2OLD  7290  dff13  7292  f1eqcocnv  7337  isoini  7374  riotaeqdv  7405  mpoeq123dva  7524  cbvmpox  7543  elimampo  7587  ovelrn  7626  elovmpod  7694  elovmpo  7695  elovmporab  7696  elovmporab1w  7697  elovmporab1  7698  elovmpt3rab1  7710  fiun  7983  f1iun  7984  zfrep6  7995  fmpox  8108  el2mpocsbcl  8126  el2mpocl  8127  bropopvvv  8131  bropfvvvv  8133  xpord2indlem  8188  xpord3inddlem  8195  elsuppfng  8210  elsuppfn  8211  suppfnss  8230  opeliunxp2f  8251  mpoxopn0yelv  8254  mpoxopovel  8261  rntpos  8280  mpocurryd  8310  fpr2  8345  wfrdmclOLD  8373  wfrlem12OLD  8376  wfr2  8392  onoviun  8399  smoel  8416  smoiso  8418  smoel2  8419  smo11  8420  tfrlem9  8441  oalimcl  8616  oaass  8617  omordi  8622  omordlim  8633  omlimcl  8634  odi  8635  omeulem1  8638  omeulem2  8639  oen0  8642  oeordi  8643  oeordsuc  8650  oelimcl  8656  oeeulem  8657  oeeui  8658  nnmordi  8687  oaabs2  8705  omabs  8707  omsmolem  8713  ereldm  8813  iiner  8847  elmapg  8897  elpmg  8901  elixpsn  8995  ixpsnf1o  8996  boxriin  8998  omxpenlem  9139  pw2f1olem  9142  phplem2  9271  php3  9275  phplem4OLD  9283  php3OLD  9287  infn0  9368  elfi  9482  dffi3  9500  marypha2lem2  9505  ordiso2  9584  wemapsolem  9619  elharval  9630  inf3lemd  9696  inf3lem1  9697  inf3lem2  9698  inf3lem3  9699  cantnfs  9735  cantnfp1lem3  9749  cantnflem1b  9755  cantnflem1  9758  ttrclselem2  9795  trcl  9797  frr2  9829  r1sdom  9843  r1ordg  9847  r1pwss  9853  tz9.12lem3  9858  tz9.12  9859  r1elwf  9865  rankr1ai  9867  rankidb  9869  rankr1bg  9872  rankval2  9887  rankunb  9919  tcrank  9953  acni  10114  acni2  10115  acndom  10120  infpwfien  10131  alephnbtwn  10140  cardaleph  10158  cardinfima  10166  iunfictbso  10183  dfac3  10190  dfac5lem5  10196  dfac5  10198  dfac9  10206  dfac12r  10216  kmlem2  10221  kmlem12  10231  kmlem13  10232  kmlem14  10233  ackbij2lem3  10309  ackbij2  10311  cofsmo  10338  alephsing  10345  fin23lem30  10411  isf32lem9  10430  itunisuc  10488  axcc2lem  10505  axcc3  10507  domtriomlem  10511  axdc2lem  10517  axdc2  10518  axdc3lem2  10520  axdc3lem4  10522  axdc4lem  10524  ac6c4  10550  zorn2lem1  10565  ttukeylem6  10583  pwcfsdom  10652  axregndlem2  10672  axinfndlem1  10674  axacndlem4  10679  axacnd  10681  pwfseqlem1  10727  inar1  10844  inatsk  10847  gruurn  10867  grur1  10889  eltskm  10912  genpelv  11069  eluz1  12907  eluzaddOLD  12938  eluzsubOLD  12939  elixx1  13416  elixx3g  13420  elioo2  13448  elfz1  13572  elfz2  13574  elfzp1  13634  fzpr  13639  fzsuc2  13642  fzrev3  13650  elfzp12  13663  fzm1  13664  elfzo  13718  fz0add1fz1  13786  elfzo0l  13806  elfzom1b  13816  fzosplitsni  13828  elfzr  13830  elfzlmr  13831  zmodidfzo  13951  seqp1  14067  seqf1o  14094  bcval  14353  bcpasc  14370  hashf1lem1  14504  fundmge2nop0  14551  wrdmap  14594  elovmpowrd  14606  ccatfval  14621  elfzelfzccat  14628  ccatlid  14634  ccatass  14636  ccatrn  14637  ccatalpha  14641  swrdfv2  14709  ccatswrd  14716  swrdccat2  14717  pfxfv  14730  pfxeq  14744  ccatpfx  14749  swrdswrd  14753  swrdpfx  14755  pfxpfx  14756  cats1un  14769  swrdccatfn  14772  swrdccatin1  14773  pfxccatin12lem4  14774  pfxccatin12lem1  14776  swrdccatin2  14777  pfxccatin12lem2c  14778  pfxccatin12lem2  14779  swrdccat3blem  14787  swrdccatin1d  14791  swrdccatin2d  14792  pfxccatin12d  14793  revccat  14814  revrev  14815  repswpfx  14833  repswccat  14834  cshwidxmod  14851  2cshw  14861  cshwcshid  14876  cshwcsh2id  14877  cshimadifsn  14878  cshimadifsn0  14879  revco  14883  ccatco  14884  cshco  14885  swrdco  14886  ofccat  15018  shftfn  15122  shftval  15123  limsupgle  15523  ello12  15562  elo12  15573  isercolllem3  15715  sumeq1  15737  fsumsplit  15789  sumsplit  15816  fsum2dlem  15818  fsumcom2  15822  fsumparts  15854  explecnv  15913  pwdif  15916  fprodser  15997  fprodsplit  16014  fprod2dlem  16028  fprodcom2  16032  eftlub  16157  divalgmod  16454  bitsval  16470  bitsp1e  16478  bitsp1o  16479  sadfval  16498  sadcp1  16501  sadval  16502  sadcadd  16504  sadadd2  16506  saddisjlem  16510  sadadd  16513  sadass  16517  smufval  16523  smuval  16527  smuval2  16528  smupvallem  16529  smu01lem  16531  smueqlem  16536  smumul  16539  bezoutlem2  16587  bezoutlem4  16589  algfx  16627  eucalgcvga  16633  reumodprminv  16851  nnnn0modprm0  16853  unbenlem  16955  prmreclem5  16967  vdwapval  17020  vdwapun  17021  vdwnnlem1  17042  vdwnn  17045  ramval  17055  0ram  17067  ramub1lem2  17074  prmgaplem7  17104  prmlem0  17153  elrest  17487  prdsbasmpt  17530  prdsleval  17537  prdsbasmpt2  17542  pwselbasb  17548  imasaddfnlem  17588  imasvscafn  17597  divsfval  17607  ismre  17648  mreunirn  17659  mrisval  17688  ismri  17689  isacs  17709  catidd  17738  iscatd2  17739  ismon  17794  isepi  17801  sectffval  17811  sectfval  17812  dfiso2  17833  cicsym  17865  issubc  17899  catsubcat  17903  isfunc  17928  funcres  17960  funcpropd  17967  ffthiso  17996  isnat  18015  isnat2  18016  fuciso  18045  initoval  18060  termoval  18061  isinito  18063  istermo  18064  iszeroo  18065  isinitoi  18066  istermoi  18067  initoid  18068  termoid  18069  iszeroi  18076  2initoinv  18077  initoeu1  18078  initoeu2  18083  2termoinv  18084  termoeu1  18085  arwhoma  18112  elsetchom  18148  setcmon  18154  setcepi  18155  setciso  18158  catciso  18178  elestrchom  18196  estrcbasbas  18199  funcestrcsetclem7  18215  funcestrcsetclem8  18216  funcestrcsetclem9  18217  fthestrcsetc  18219  fullestrcsetc  18220  equivestrcsetc  18221  setc1strwun  18222  funcsetcestrclem7  18230  funcsetcestrclem8  18231  funcsetcestrclem9  18232  fthsetcestrc  18234  fullsetcestrc  18235  hofcl  18329  hofpropd  18337  yonedalem4c  18347  yonedainv  18351  yonffthlem  18352  lubeldm  18423  glbeldm  18436  joindef  18446  meetdef  18460  poslubdg  18484  acsficl2d  18622  acsmapd  18624  psref  18644  psss  18650  dirge  18673  mgmpropd  18689  issstrmgm  18691  grpidval  18699  grpidpropd  18700  grpidd  18709  ismgmhm  18734  issubmgm  18740  issgrpd  18768  sgrppropd  18769  ismndd  18794  mndpropd  18797  imasmnd2  18809  imasmnd  18810  xpsmnd0  18813  ismhm  18820  issubm  18838  gsumsgrpccat  18875  elefmndbas2  18909  smndex1mndlem  18944  imasgrp2  19095  imasgrp  19096  issubg  19166  subginv  19173  isnsg  19195  eqg0el  19223  quselbas  19224  isghm  19255  isghmOLD  19256  resghm2b  19274  conjnmzb  19293  conjnsg  19294  ghmpropd  19296  isga  19331  elcntz  19362  elcntzsn  19365  cntzrcl  19367  resscntz  19373  symgextf1  19463  gsmsymgreqlem2  19473  f1otrspeq  19489  pmtrfrn  19500  pmtrdifellem3  19520  pmtrdifellem4  19521  psgnunilem1  19535  psgnunilem5  19536  psgnunilem2  19537  psgnunilem3  19538  psgneldm2  19546  psgnfitr  19559  psgnsn  19562  gexdvds  19626  gex1  19633  isslw  19650  sylow3lem2  19670  lsmelvalx  19682  pj1ghm  19745  efgtlen  19768  efgsfo  19781  efgredlemc  19787  frgp0  19802  frgpmhm  19807  qusabl  19907  frgpnabllem1  19915  imasabl  19918  cycsubmcmn  19931  0cyg  19935  cycsubgcyg  19943  gsumval3  19949  gsumcllem  19950  gsumzaddlem  19963  gsumzsplit  19969  gsummptfzcl  20011  eldprd  20048  dprdcntz2  20082  dprd2d2  20088  dmdprdsplit2lem  20089  dmdprdsplit2  20090  dprdsplit  20092  ablfac2  20133  isrngd  20200  rngpropd  20201  imasrng  20204  qusrng  20207  ringurd  20212  isringd  20314  imasring  20353  xpsring1d  20356  dvdsrval  20387  isunit  20399  dvdsrpropd  20442  isirred  20445  isrnghm  20467  isrngim  20471  c0ghm  20487  c0snghm  20490  isrhm  20504  isrim0OLD  20507  isrim0  20509  islring  20566  issubrng  20573  opprsubrng  20585  issubrg  20599  opprsubrg  20621  resrhm2b  20630  rhmpropd  20637  rnghmresel  20642  elrngchom  20646  rnghmsubcsetclem1  20653  rnghmsubcsetclem2  20654  rngcid  20657  rngcsect  20658  rngciso  20660  funcrngcsetcALT  20663  zrinitorngc  20664  zrtermorngc  20665  rhmresel  20671  elringchom  20675  rhmsubcsetclem1  20682  rhmsubcsetclem2  20683  ringcid  20686  rhmsscrnghm  20687  rhmsubcrngclem1  20688  rhmsubcrngclem2  20689  ringcsect  20692  ringciso  20694  ringcbasbas  20695  zrtermoringc  20697  srhmsubc  20702  rhmsubclem3  20709  rhmsubclem4  20710  drngunit  20756  isdrngd  20787  isdrngdOLD  20789  issdrg  20811  sdrgunit  20819  isabv  20834  issrngd  20878  islmod  20884  lmodprop2d  20944  islss  20955  islssd  20956  lssats2  21021  ellspsn  21024  islmhm  21049  lmhmf1o  21068  lmhmima  21069  lmhmpreima  21070  reslmhm  21074  pwssplit3  21083  lmhmpropd  21095  islbs  21098  lspprel  21116  lspfixed  21153  lbsacsbs  21181  lbsextlem1  21183  lbsextlem2  21184  lbsextlem3  21185  lbsextlem4  21186  ixpsnbasval  21238  isridlrng  21252  rnglidlmmgm  21278  isridl  21285  quscrng  21316  rngqiprngimfolem  21323  rngqiprngimf1lem  21327  rngqiprngimfo  21334  islpidl  21358  lidldvgen  21367  irinitoringc  21513  pzriprnglem13  21527  pzriprnglem14  21528  zrhrhmb  21544  znf1o  21593  frgpcyg  21615  psgnevpmb  21628  isphld  21695  phlssphl  21700  elocv  21709  iscss  21724  isobs  21763  obs2ss  21772  dsmmfi  21781  dsmmelbas  21782  dsmmlss  21787  frlmelbas  21799  frlmlbs  21840  frlmup1  21841  ellspd  21845  islinds  21852  islindf2  21857  f1lindf  21865  islindf4  21881  assamulgscmlem2  21943  psrgrp  21999  mplsubglem  22042  mpllsslem  22043  mplmonmul  22077  subrgascl  22113  subrgasclcl  22114  mpfind  22154  ismhp  22167  gsumply1subr  22256  lply1binomsc  22336  matbas2d  22450  matecl  22452  matvscl  22458  mat1  22474  mat0dim0  22494  mat0dimid  22495  mat0dimscm  22496  mat1dimelbas  22498  dmatel  22520  scmatel  22532  scmateALT  22539  scmataddcl  22543  scmatsubcl  22544  smatvscl  22551  scmatghm  22560  mat1scmat  22566  mdetunilem7  22645  mdetunilem9  22647  smadiadetr  22702  cramerimplem2  22711  cramer0  22717  pmatcoe1fsupp  22728  cpmatpmat  22737  cpmatel  22738  cpmatacl  22743  cpmatinvcl  22744  mat2pmatghm  22757  mat2pmatmul  22758  decpmatmullem  22798  pmatcollpwlem  22807  pmatcollpw3fi1lem1  22813  pmatcollpwscmatlem1  22816  monmat2matmon  22851  chfacfscmul0  22885  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  cayhamlem1  22893  cpmadugsumlemB  22901  cpmadugsumlemC  22902  cpmadugsumlemF  22903  cayhamlem2  22911  istopon  22939  eltg  22985  eltg2  22986  eltop  23002  eltop2  23003  eltop3  23004  pptbas  23036  iscld  23056  neiss2  23130  isnei  23132  neiptopnei  23161  neiptopreu  23162  lpfval  23167  lpval  23168  islp  23169  maxlp  23176  islpi  23178  neitr  23209  restlp  23212  ordtbas2  23220  ordtrest2  23233  lmfval  23261  cnfval  23262  iscn  23264  iscnp  23266  tgcn  23281  tgcnp  23282  lmbrf  23289  cnpresti  23317  ist1  23350  ist1-2  23376  cnt1  23379  haust1  23381  cmpfi  23437  cmpfii  23438  1stcfb  23474  2ndc1stc  23480  1stcrest  23482  2ndcdisj  23485  1stcelcls  23490  nllyi  23504  subislly  23510  islocfin  23546  lfinpfin  23553  locfindis  23559  locfincf  23560  comppfsc  23561  kgenval  23564  elkgen  23565  kgencn2  23586  txbas  23596  eltx  23597  ptval  23599  ptpjpre1  23600  ptopn2  23613  ptpjopn  23641  ptclsg  23644  xkoccn  23648  txdis  23661  txdis1cn  23664  ptrescn  23668  hausdiag  23674  hauseqlcld  23675  txhaus  23676  xkohaus  23682  elqtop  23726  qtopeu  23745  kqcldsat  23762  hmeofval  23787  ptuncnv  23836  ptunhmeo  23837  elmptrab  23856  fbdmn0  23863  elfg  23900  elfilss  23905  filunirn  23911  fixufil  23951  elfm  23976  rnelfmlem  23981  rnelfm  23982  fmfnfmlem4  23986  elflim2  23993  flimtopon  23999  elflim  24000  hausflim  24010  flimcls  24014  flfnei  24020  isflf  24022  hausflf  24026  cnpflf  24030  cnflf  24031  txflf  24035  isfcls  24038  fclstopon  24041  isfcls2  24042  fclssscls  24047  fclsnei  24048  fclsfnflim  24056  flimfnfcls  24057  isfcf  24063  fcfelbas  24065  cnpfcf  24070  cnfcf  24071  flfcntr  24072  alexsublem  24073  alexsubALTlem3  24078  cnextfun  24093  cnextfvval  24094  cnextf  24095  cnextcn  24096  tmdgsum2  24125  tgpconncomp  24142  ghmcnp  24144  qustgplem  24150  eltsms  24162  haustsms  24165  tsmsgsum  24168  tsmssubm  24172  tsmssplit  24181  isust  24233  ustbas  24257  elutop  24263  ustuqtoplem  24269  ustuqtop4  24274  ustuqtop  24276  utopsnneiplem  24277  utopsnneip  24278  utopsnnei  24279  isusp  24291  isucn  24308  ucncn  24315  iscfilu  24318  neipcfilu  24326  iscusp  24329  cnextucn  24333  ispsmet  24335  ismet  24354  isxmet  24355  elblps  24418  elbl  24419  elmopn  24473  prdsbl  24525  neibl  24535  met1stc  24555  metrest  24558  prdsxmslem2  24563  txmetcnp  24581  txmetcn  24582  metustsym  24589  cfilucfil2  24595  elbl4  24597  metuel  24598  psmetutop  24601  restmetu  24604  metucn  24605  tngngp  24696  isnmhm  24788  zcld  24854  metnrmlem1a  24899  elcncf  24934  cncfcnvcn  24971  cnheibor  25006  lebnumlem1  25012  ishtpy  25023  isphtpy  25032  om1elbas  25084  elpi1  25097  pi1xfr  25107  pi1coghm  25113  tcphcph  25290  lmmbrf  25315  iscfil  25318  iscau  25329  iscauf  25333  caucfil  25336  iscmet  25337  cmetcaulem  25341  iscmet3lem1  25344  iscmet3lem2  25345  iscmet3  25346  bcthlem1  25377  cmsss  25404  cmetcusp1  25406  cmetcusp  25407  cmscsscms  25426  rrxcph  25445  minveclem3b  25481  ovolfioo  25521  ovolficc  25522  ovolctb  25544  ovoliunnul  25561  ovolshftlem1  25563  sca2rab  25566  ovolscalem1  25567  ovolicc2lem1  25571  ovolicc2lem2  25572  ovolicc2lem4  25574  ovolicc2lem5  25575  iundisj  25602  iunmbl2  25611  uniioombllem3  25639  vitalilem2  25663  vitalilem3  25664  mbfss  25700  i1faddlem  25747  i1fmullem  25748  mbfi1fseqlem2  25771  mbfi1fseqlem4  25773  mbfi1fseq  25776  itg2splitlem  25803  itg2split  25804  itg2monolem1  25805  itg2gt0  25815  isibl  25820  iblss2  25861  itgss3  25870  itgsplit  25891  ellimc  25928  limcmo  25937  cnlimc  25943  limciun  25949  limcun  25950  eldv  25953  dvbsss  25957  dvreslem  25964  elcpn  25990  dvaddf  25999  dvmulf  26000  dvcof  26006  rolle  26048  dvlip2  26054  dvivthlem1  26067  lhop1  26073  lhop2  26074  ftc1cn  26104  fta1glem2  26228  plyco0  26251  elply  26254  ply1termlem  26262  eltayl  26419  tayl0  26421  taylplem1  26422  taylplem2  26423  dvtaylp  26430  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  abelth  26503  cxpcn3  26809  rlimcnp  27026  fsumharmonic  27073  dchrelbas  27298  pntrsumbnd2  27629  ostth2lem2  27696  nolesgn2ores  27735  nogesgn1ores  27737  nosupprefixmo  27763  noinfprefixmo  27764  nosupcbv  27765  nosupdm  27767  nosupfv  27769  nosupres  27770  nosupbnd1lem1  27771  nosupbnd1lem3  27773  nosupbnd1lem5  27775  nosupbnd2lem1  27778  noinfcbv  27780  noinfdm  27782  noinffv  27784  noinfres  27785  noinfbnd1lem1  27786  noinfbnd1lem3  27788  noinfbnd1lem5  27790  noinfbnd2lem1  27793  elmade  27924  elold  27926  ssltleft  27927  ssltright  27928  oldlim  27943  madebday  27956  newbday  27958  sltlpss  27963  cofcutr  27976  cofcutrtime  27979  lrrecval  27990  lrrecval2  27991  addsval  28013  precsexlem9  28257  precsexlem11  28259  sltonold  28301  noseqrdgfn  28330  istrkgb  28481  istrkgcb  28482  istrkge  28483  istrkgl  28484  istrkgld  28485  axtgsegcon  28490  axtg5seg  28491  axtgbtwnid  28492  axtgpasch  28493  axtgupdim2  28497  axtgeucl  28498  tgdim01  28533  iscgrg  28538  isismt  28560  tglnunirn  28574  tglngval  28577  tgellng  28579  legval  28610  legov  28611  legov2  28612  ishlg  28628  mirreu3  28680  mirval  28681  mirfv  28682  mircgr  28683  mirbtwn  28684  ismir  28685  mireq  28691  symquadlem  28715  israg  28723  perpln1  28736  perpln2  28737  isperp  28738  islnopp  28765  outpasch  28781  ishpg  28785  iscgra  28835  dfcgra2  28856  isinag  28864  isleag  28873  iseqlg  28893  f1otrgitv  28896  f1otrg  28897  f1otrge  28898  ttgval  28901  ttgvalOLD  28902  ttgelitv  28915  elee  28927  brbtwn  28932  brcgr  28933  axlowdimlem16  28990  ebtwntg  29015  elntg2  29018  upgrex  29127  edgupgr  29169  upgredg  29172  edglnl  29178  numedglnl  29179  uhgr2edg  29243  umgr2edg1  29246  usgredg2vlem1  29260  usgredg2vlem2  29261  ushgredgedg  29264  ushgredgedgloop  29266  uhgrspansubgrlem  29325  fusgrfisstep  29364  nbgrval  29371  nbgrel  29375  nbupgrel  29380  nbgr2vtx1edg  29385  nbuhgr2vtx1edgblem  29386  nbuhgr2vtx1edgb  29387  nbusgreledg  29388  usgrnbcnvfv  29400  uvtxval  29422  uvtxel  29423  uvtx01vtx  29432  uvtxusgrel  29438  nbcplgr  29469  cplgr3v  29470  cusgrexi  29478  structtocusgr  29481  vtxdgfval  29503  vtxdg0v  29509  vtxdeqd  29513  vtxdun  29517  1loopgrnb0  29538  1loopgrvd0  29540  1hevtxdg0  29541  1hevtxdg1  29542  1egrvtxdg1  29545  umgr2v2evtxel  29558  umgr2v2enb1  29562  umgr2v2evd2  29563  vtxdginducedm1lem4  29578  vtxdginducedm1  29579  finsumvtxdg2sstep  29585  ewlksfval  29637  isewlk  29638  wksfval  29645  iswlk  29646  uspgr2wlkeq  29682  wlkres  29706  usgr2pthlem  29799  clwlkcompim  29816  uspgrn2crct  29841  wwlks  29868  iswwlksn  29871  wwlknvtx  29878  wlkiswwlks2  29908  wwlksm1edg  29914  wwlksnred  29925  wwlksnext  29926  wwlksnredwwlkn  29928  wwlksnredwwlkn0  29929  wwlksnwwlksnon  29948  wspn0  29957  usgr2wspthons3  29997  rusgrnumwwlkb0  30004  clwwlk  30015  clwwlkccatlem  30021  clwlkclwwlklem2a4  30029  clwlkclwwlk  30034  clwwisshclwwslem  30046  clwwlkinwwlk  30072  clwwlkel  30078  clwwlkf  30079  clwwlkext2edg  30088  wwlksext2clwwlk  30089  wwlksubclwwlk  30090  clwwnisshclwwsn  30091  eleclclwwlknlem2  30093  erclwwlknsym  30102  erclwwlkntr  30103  umgrhashecclwwlk  30110  clwwlkvbij  30145  eupth2lem3lem3  30262  eupth2lem3lem4  30263  eupth2lem3lem6  30265  eupth2lemb  30269  eucrct2eupth  30277  fusgreg2wsplem  30365  2clwwlklem  30375  2clwwlk2clwwlklem  30378  2clwwlkel  30381  2clwwlk2clwwlk  30382  extwwlkfabel  30385  clwwlknonclwlknonf1o  30394  dlwwlknondlwlknonf1olem1  30396  numclwwlk2lem1  30408  numclwlk2lem2f  30409  numclwlk2lem2f1o  30411  ex-res  30473  isssp  30756  sspn  30768  islno  30785  isblo  30814  nmlno0  30827  ishmo  30843  dipdir  30874  dipass  30877  ubthlem1  30902  ubthlem2  30903  htthlem  30949  htth  30950  ocel  31313  ocnel  31330  shsel  31346  shsel2  31354  shmodsi  31421  pjhtheu  31426  pjeq  31431  axpjpj  31452  pjoc2  31471  elspani  31575  h1de2ctlem  31587  elspansn  31598  elspansn2  31599  elnlfn  31960  eleigvec  31989  riesz3i  32094  cbviunf  32578  iuneq12daf  32579  iunrdx  32586  iunrnmptss  32588  cbvdisjf  32593  disjorf  32601  disjabrex  32604  disjabrexf  32605  iundisjf  32611  disjrdx  32613  brab2d  32629  2ndresdju  32667  abfmpunirn  32670  abfmpeld  32672  abfmpel  32673  fmptcof2  32675  acunirnmpt2  32678  acunirnmpt2f  32679  aciunf1lem  32680  funcnvmpt  32685  suppss3  32738  fpwrelmap  32747  xrofsup  32774  iundisjfi  32801  eliccioo  32895  s3f1  32913  ccatf1  32915  ccatws1f1o  32918  swrdrn3  32922  ismnt  32956  mgcoval  32959  gsummpt2co  33031  gsumpart  33038  gsumhashmul  33040  xrge0tsmsbi  33042  cycpmco2  33126  cyc3co2  33133  inftmrel  33160  isinftm  33161  isslmd  33181  urpropd  33212  erlval  33230  rlocval  33231  rloccring  33242  rloc1r  33244  isdrng4  33264  fracfld  33275  resv1r  33333  ellspds  33361  ellpi  33366  lbslsp  33370  rhmimaidl  33425  isprmidl  33431  qsidomlem1  33445  qsidomlem2  33446  ismxidl  33455  crngmxidl  33462  drng0mxidl  33469  opprqus0g  33483  qsfld  33491  isrprm  33510  rsprprmprmidlb  33516  ply1mulrtss  33571  dimpropd  33621  lbslsat  33629  extdg1id  33676  elirng  33686  ply1annidllem  33694  constrsuc  33728  constrconj  33735  smatrcl  33742  smatcl  33748  ist0cld  33779  txomap  33780  locfinreflem  33786  zarclsiin  33817  zart0  33825  rhmpreimacnlem  33830  metidval  33836  cnre2csqima  33857  ordtrest2NEW  33869  fmcncfil  33877  fsumcvg4  33896  ofcfval  34062  measvuni  34178  meascnbl  34183  faeval  34210  ismbfm  34215  elunirnmbfm  34216  imambfm  34227  elcarsg  34270  itgeq12dv  34291  issibf  34298  eulerpartlems  34325  eulerpartlemgc  34327  eulerpartlemgvv  34341  eulerpartlemgu  34342  eulerpart  34347  rrvmbfm  34407  elorvc  34424  elorrvc  34428  dstfrvunirn  34439  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemsima  34480  ballotlemrv  34484  fzssfzo  34516  signstfvn  34546  signstfvneq0  34549  signstres  34552  repr0  34588  reprinrn  34595  reprdifc  34604  hgt750lemg  34631  hgt750lemb  34633  istrkg2d  34643  axtgupdim2ALTV  34645  afsval  34648  brafs  34649  bnj945  34749  bnj1400  34811  bnj18eq1  34903  bnj916  34909  bnj1014  34937  bnj1015  34938  bnj1110  34958  bnj1417  35017  revpfxsfxrev  35083  cplgredgex  35088  pfxwlk  35091  revwlk  35092  subfacp1lem2b  35149  subfacp1lem4  35151  subfacp1lem5  35152  subfacp1lem6  35153  ptpconn  35201  cvmscbv  35226  iscvm  35227  cvmsi  35233  cvmsval  35234  cvmliftmolem1  35249  cvmlift2lem12  35282  cvmlift2lem13  35283  cvmlift3lem7  35293  snmlval  35299  satfv1  35331  satfvsucsuc  35333  satfrnmapom  35338  satf0op  35345  satf0n0  35346  sat1el2xp  35347  fmlafvel  35353  isfmlasuc  35356  fmlaomn0  35358  gonan0  35360  goaln0  35361  gonar  35363  goalr  35365  satffunlem1lem2  35371  satffunlem2lem2  35374  satfv0fvfmla0  35381  satef  35384  satefvfmla0  35386  sategoelfvb  35387  satfv1fvfmla1  35391  mrsubfval  35476  mrsubvrs  35490  mclsrcl  35529  mclsval  35531  mppsval  35540  mclsppslem  35551  opelco3  35738  wsuclem  35789  funtransport  35995  fvtransport  35996  brcolinear  36023  colineardim1  36025  funray  36104  fvray  36105  funline  36106  fvline  36108  lineelsb2  36112  fwddifval  36126  fwddifnval  36127  rankelg  36132  rankeq1o  36135  elhf2  36139  0hf  36141  rmoeqbidv  36177  reueqbidv  36179  disjeq12dv  36181  ixpeq12dv  36182  prodeq12sdv  36184  itgeq12sdv  36185  cbvralvw2  36192  cbvrexvw2  36193  cbvrmovw2  36194  cbvreuvw2  36195  cbvcsbvw2  36197  cbviunvw2  36198  cbviinvw2  36199  cbvmptvw2  36200  cbvdisjvw2  36201  cbvmpo1vw2  36209  cbvmpo2vw2  36210  cbvsbcdavw  36223  cbvcsbdavw  36225  cbvcsbdavw2  36226  cbviundavw  36228  cbviindavw  36229  cbvdisjdavw  36234  cbvrabdavw2  36251  cbviundavw2  36252  cbviindavw2  36253  cbvmptdavw2  36254  cbvdisjdavw2  36255  cbvriotadavw2  36256  cbvmpo1davw2  36258  cbvmpo2davw2  36259  cbvsumdavw2  36261  neibastop2lem  36326  neibastop3  36328  eltail  36340  bj-projeq  36958  bj-projval  36962  bj-restsn  37048  opelopabbv  37109  brabd0  37113  bj-eldiag  37142  bj-eldiag2  37143  mptsnunlem  37304  dissneqlem  37306  iooelexlt  37328  relowlssretop  37329  rdgellim  37342  exrecfnlem  37345  finxpeq1  37352  finxpreclem6  37362  pibp21  37381  curf  37558  uncf  37559  curunc  37562  unccur  37563  fin2so  37567  lindsadd  37573  lindsdom  37574  lindsenlbs  37575  matunitlindflem1  37576  matunitlindflem2  37577  matunitlindf  37578  ptrest  37579  ptrecube  37580  poimirlem2  37582  poimirlem8  37588  poimirlem17  37597  poimirlem18  37598  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem24  37604  poimirlem26  37606  poimirlem29  37609  heicant  37615  mblfinlem1  37617  mblfinlem2  37618  volsupnfl  37625  itg2addnclem  37631  itg2gt0cn  37635  indexdom  37694  incsequz  37708  istotbnd  37729  istotbnd3  37731  0totbnd  37733  sstotbnd  37735  sstotbnd3  37736  isbnd  37740  prdstotbnd  37754  cntotbnd  37756  isismty  37761  heibor1lem  37769  heiborlem2  37772  heiborlem3  37773  heibor  37781  isass  37806  exidcl  37836  exidreslem  37837  elghomlem2OLD  37846  rngoidmlem  37896  rngo1cl  37899  divrngcl  37917  isdrngo2  37918  isrngohom  37925  isrngoiso  37938  isriscg  37944  iscom2  37955  iscringd  37958  isidl  37974  ispridl  37994  ismaxidl  38000  ac6s6  38132  dmecd  38260  releldmqs  38614  releldmqscoss  38616  erimeq2  38634  eldisjlem19  38766  membpartlem19  38767  prter3  38838  islshp  38935  islsat  38947  lcvfbr  38976  islfl  39016  ellkr  39045  islshpkrN  39076  ldual1dim  39122  isopos  39136  cmtfvalN  39166  cvrfval  39224  isat  39242  islln  39463  islpln  39487  islvol  39530  isline  39696  ispointN  39699  ispsubsp  39702  elpmap  39715  elpmapat  39721  elpadd  39756  paddclN  39799  elpclN  39849  elpcliN  39850  pclfinN  39857  pclcmpatN  39858  ispsubclN  39894  iswatN  39951  islhp  39953  islaut  40040  ispautN  40056  isldil  40067  isltrn  40076  isdilN  40111  istrnN  40114  istendo  40717  dvhb1dimN  40943  erng1lem  40944  erngdvlem4-rN  40956  diaelval  40990  diaeldm  40993  dia1dimid  41020  cdlemm10N  41075  dibopelvalN  41100  dibopelval2  41102  dibelval3  41104  dibelval1st  41106  dibelval2nd  41109  dibeldmN  41115  dibvalrel  41120  dibglbN  41123  dicffval  41131  dicfval  41132  dicopelval  41134  dicelvalN  41135  dicelval3  41137  dicvalrelN  41142  dicelval1sta  41144  diclspsn  41151  dihopelvalbN  41195  dihopelvalcqat  41203  dihopelvalcpre  41205  dihvalrel  41236  dih1  41243  dihmeetlem4preN  41263  dihmeetlem13N  41276  dih1dimatlem  41286  dochnel2  41349  dihjatcclem4  41378  dvh2dim  41402  dvh3dim  41403  dvh4dimN  41404  dochfln0  41434  lpolsetN  41439  islpolN  41440  lcfrvalsnN  41498  lcfrlem21  41520  lcfrlem27  41526  lcfrlem37  41536  lcfr  41542  lcdlss  41576  mapdcv  41617  hdmap1fval  41753  hdmapffval  41783  hdmapfval  41784  hdmapval  41785  hgmapffval  41842  hgmapfval  41843  hdmapellkr  41871  hlhilhillem  41921  fzsplitnd  41939  isprimroot  42050  primrootsunit1  42054  primrootscoprmpow  42056  primrootscoprbij  42059  aks6d1c1p2  42066  aks6d1c1p3  42067  aks6d1c1p4  42068  aks6d1c1p5  42069  aks6d1c1p6  42071  aks6d1c1  42073  evl1gprodd  42074  sticksstones11  42113  sticksstones12a  42114  rhmqusspan  42142  grpods  42151  fzosumm1  42245  frlmfielbas  42455  frlmsnic  42495  psrmnd  42500  isnacs  42660  mrefg2  42663  elmzpcl  42682  mzpcompact2  42708  eldiophb  42713  elpell1qr  42803  elpell14qr  42805  elpell1234qr  42807  pw2f1ocnv  42994  pw2f1o2val2  42997  aomclem4  43014  aomclem6  43016  islssfg2  43028  imasgim  43057  lnr2i  43073  elmnc  43093  rngunsnply  43130  onexomgt  43202  onexlimgt  43204  onexoegt  43205  oaordnr  43258  omnord1  43267  oenord1  43278  cantnfresb  43286  tfsconcatun  43299  tfsconcat0i  43307  ofoaf  43317  naddcnff  43324  naddcnffo  43326  naddcnfcom  43328  naddcnfid1  43329  naddcnfid2  43330  naddcnfass  43331  naddwordnexlem4  43363  fiinfi  43535  sqrtcvallem1  43593  elintima  43615  eliunov2  43641  ov2ssiunov2  43662  brtrclfv2  43689  rfovcnvf1od  43966  rfovcnvfvd  43969  fsovrfovd  43971  fsovfvd  43972  fsovcnvlem  43975  ntrclsfv1  44017  ntrclselnel1  44019  ntrclsneine0lem  44026  ntrneifv1  44041  ntrneifv2  44042  ntrneiel  44043  gneispace2  44094  gneispacess2  44108  extoimad  44126  mnringelbased  44183  dvconstbi  44303  bccbc  44314  eliin2f  45006  iineq12dv  45008  rabbida2  45034  disjinfi  45099  unirnmap  45115  elmptima  45167  iuneqfzuzlem  45249  iooiinioc  45474  fsumiunss  45496  fsumsupp0  45499  lptre2pt  45561  icccncfext  45808  cncfiooicclem1  45814  dvnprodlem2  45868  stoweidlem27  45948  stoweidlem29  45950  stoweidlem31  45952  stoweidlem34  45955  stoweidlem48  45969  stoweidlem59  45980  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem2  46030  fourierdlem3  46031  fourierdlem25  46053  fourierdlem32  46060  fourierdlem33  46061  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem62  46089  fourierdlem70  46097  fourierdlem80  46107  fourierdlem92  46119  fourierdlem93  46120  fourierdlem101  46128  etransclem37  46192  sge0val  46287  sge0f1o  46303  sge0iunmptlemre  46336  sge0iunmpt  46339  iundjiun  46381  caragenel  46416  ovncvrrp  46485  ovnsubaddlem1  46491  ovnsubadd  46493  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hoidmvle  46521  ovncvr2  46532  hspdifhsp  46537  hoiqssbl  46546  hspmbllem2  46548  hspmbl  46550  opnvonmbllem1  46553  isvonmbl  46559  ovnovollem1  46577  issmflem  46648  smflimlem3  46694  smflimlem4  46695  smflim  46698  smfmullem2  46713  smflimmpt  46731  smfsuplem1  46732  smflimsuplem1  46741  smflimsuplem3  46743  smflimsuplem4  46744  smflimsuplem7  46747  smflimsup  46749  tworepnotupword  46805  fcores  46982  fcoresf1  46984  afvelrnb  47078  afvelrnb0  47079  afv2co2  47172  el1fzopredsuc  47240  iccpart  47290  iccpartgtprec  47294  iccpartiltu  47296  iccpartigtl  47297  iccpartltu  47299  iccpartgtl  47300  iccpartgt  47301  iccpartleu  47302  iccpartgel  47303  iccelpart  47307  iccpartiun  47308  icceuelpart  47310  fargshiftfv  47313  fargshiftfo  47316  sprel  47358  prprelb  47390  prprelprb  47391  fpprel  47602  sbgoldbo  47661  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  bgoldbtbndlem3  47681  bgoldbtbnd  47683  clnbgrval  47696  clnbgrel  47701  clnbupgrel  47707  vopnbgrel  47726  uspgrimprop  47757  grtriprop  47792  isgrtri  47794  grtriclwlk3  47796  upwlksfval  47858  isupwlk  47859  intop  47926  isclintop  47930  assintop  47932  isassintop  47933  assintopcllaw  47935  uzlidlring  47958  elrngchomALTV  47992  rngccatidALTV  47995  rngcsectALTV  47998  rngcisoALTV  48000  rhmsubcALTVlem3  48006  rhmsubcALTVlem4  48007  funcringcsetcALTV2lem7  48019  funcringcsetcALTV2lem9  48021  elringchomALTV  48026  ringccatidALTV  48029  ringcsectALTV  48032  ringcisoALTV  48034  ringcbasbasALTV  48035  funcringcsetclem7ALTV  48042  funcringcsetclem9ALTV  48044  srhmsubcALTV  48048  opeliun2xp  48057  cbvmpox2  48060  ply1sclrmsm  48112  dmatALTbasel  48131  lcoval  48141  lindslinindsimp1  48186  lindslinindsimp2  48192  lmod1  48221  elbigo  48285  elbigo2  48286  elbigolo1  48291  dig2nn0ld  48338  naryfvalel  48364  rrxlines  48467  rrxlinesc  48469  rrxlinec  48470  eenglngeehlnm  48473  elrrx2linest2  48479  rrxsphere  48482  itsclc0  48505  itsclc0b  48506  itsclinecirc0  48507  itsclinecirc0b  48508  itscnhlinecirc02p  48519  f1omo  48574  lubeldm2d  48638  glbeldm2d  48639  catprs  48678  isthinc  48688  isthincd2lem1  48694  thincmoALT  48697  thincmod  48698  isthincd  48704  prsthinc  48721  elsetrecslem  48791