Theorem eleq2d 2824

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1534   = wceq 1536  ∃wex 1775   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  eleq2  2827  eleq12d  2832  eleqtrd  2840  neleqtrd  2860  eqabrd  2881  raleqbidv  3343  rexeqbidv  3344  rabeqbidva  3449  elabd2  3669  sbcbid  3849  csbeq2d  3913  csbeq2dv  3914  cbvcsbw  3917  cbvcsb  3918  cbvcsbv  3919  csbie  3943  csbied  3945  csbie2g  3950  cbvralcsf  3952  cbvreucsf  3954  cbvrabcsf  3955  sbcel12  4416  sbcel1g  4421  sbcel2  4423  prel12g  4868  eliuni  5001  iuneqconst  5007  iuneq12df  5022  iuneq12d  5025  cbviun  5040  cbviin  5041  cbviung  5042  cbviing  5043  cbviunv  5044  cbviinv  5045  iinxsng  5092  iinxprg  5093  iunxsng  5094  iunxsngf  5096  cbvdisj  5124  cbvdisjv  5125  disjor  5129  disjiund  5138  mpteq12da  5232  mpteq12dfOLD  5234  mpteq12f  5235  mpteq12dva  5236  axpweq  5356  rabxfrd  5422  rbropapd  5573  opeliunxp  5755  opeliunxp2  5851  iunxpf  5861  elimampt  6062  elrelimasn  6105  elimasngOLD  6110  elimasni  6111  xpdifid  6189  ressn  6306  funfni  6674  fnbr  6676  dffv3  6902  elfv2ex  6952  fvelrnb  6968  foelcdmi  6969  fvun1  6999  fvco2  7005  elfvmptrab1w  7042  elfvmptrab1  7043  elfvmptrab  7044  elpreima  7077  dff3  7119  fmptco  7148  fnelfp  7194  fnelnfp  7196  tpres  7220  fnprb  7227  fntpb  7228  funfvima3  7255  eluniima  7269  elunirn2OLD  7272  dff13  7274  f1ounsn  7291  f1eqcocnv  7320  isoini  7357  riotaeqdv  7388  mpoeq123dva  7506  cbvmpox  7525  elimampo  7569  ovelrn  7608  elovmpod  7676  elovmpo  7677  elovmporab  7678  elovmporab1w  7679  elovmporab1  7680  elovmpt3rab1  7692  fiun  7965  f1iun  7966  zfrep6  7977  fmpox  8090  el2mpocsbcl  8108  el2mpocl  8109  bropopvvv  8113  bropfvvvv  8115  xpord2indlem  8170  xpord3inddlem  8177  elsuppfng  8192  elsuppfn  8193  suppfnss  8212  opeliunxp2f  8233  mpoxopn0yelv  8236  mpoxopovel  8243  rntpos  8262  mpocurryd  8292  fpr2  8327  wfrdmclOLD  8355  wfrlem12OLD  8358  wfr2  8374  onoviun  8381  smoel  8398  smoiso  8400  smoel2  8401  smo11  8402  tfrlem9  8423  oalimcl  8596  oaass  8597  omordi  8602  omordlim  8613  omlimcl  8614  odi  8615  omeulem1  8618  omeulem2  8619  oen0  8622  oeordi  8623  oeordsuc  8630  oelimcl  8636  oeeulem  8637  oeeui  8638  nnmordi  8667  oaabs2  8685  omabs  8687  omsmolem  8693  ereldm  8793  iiner  8827  elmapg  8877  elpmg  8881  elixpsn  8975  ixpsnf1o  8976  boxriin  8978  omxpenlem  9111  pw2f1olem  9114  phplem2  9242  php3  9246  phplem4OLD  9254  php3OLD  9258  infn0  9337  elfi  9450  dffi3  9468  marypha2lem2  9473  ordiso2  9552  wemapsolem  9587  elharval  9598  inf3lemd  9664  inf3lem1  9665  inf3lem2  9666  inf3lem3  9667  cantnfs  9703  cantnfp1lem3  9717  cantnflem1b  9723  cantnflem1  9726  ttrclselem2  9763  trcl  9765  frr2  9797  r1sdom  9811  r1ordg  9815  r1pwss  9821  tz9.12lem3  9826  tz9.12  9827  r1elwf  9833  rankr1ai  9835  rankidb  9837  rankr1bg  9840  rankval2  9855  rankunb  9887  tcrank  9921  acni  10082  acni2  10083  acndom  10088  infpwfien  10099  alephnbtwn  10108  cardaleph  10126  cardinfima  10134  iunfictbso  10151  dfac3  10158  dfac5lem5  10164  dfac5  10166  dfac9  10174  dfac12r  10184  kmlem2  10189  kmlem12  10199  kmlem13  10200  kmlem14  10201  ackbij2lem3  10277  ackbij2  10279  cofsmo  10306  alephsing  10313  fin23lem30  10379  isf32lem9  10398  itunisuc  10456  axcc2lem  10473  axcc3  10475  domtriomlem  10479  axdc2lem  10485  axdc2  10486  axdc3lem2  10488  axdc3lem4  10490  axdc4lem  10492  ac6c4  10518  zorn2lem1  10533  ttukeylem6  10551  pwcfsdom  10620  axregndlem2  10640  axinfndlem1  10642  axacndlem4  10647  axacnd  10649  pwfseqlem1  10695  inar1  10812  inatsk  10815  gruurn  10835  grur1  10857  eltskm  10880  genpelv  11037  eluz1  12879  eluzaddOLD  12910  eluzsubOLD  12911  elixx1  13392  elixx3g  13396  elioo2  13424  elfz1  13548  elfz2  13550  elfzp1  13610  fzpr  13615  fzsuc2  13618  fzrev3  13626  elfzp12  13639  fzm1  13643  elfzo  13697  fz0add1fz1  13770  elfzo0l  13791  elfzom1b  13801  fzosplitsni  13813  elfzr  13815  elfzlmr  13816  zmodidfzo  13936  seqp1  14053  seqf1o  14080  bcval  14339  bcpasc  14356  hashf1lem1  14490  fundmge2nop0  14537  wrdmap  14580  elovmpowrd  14592  ccatfval  14607  elfzelfzccat  14614  ccatlid  14620  ccatass  14622  ccatrn  14623  ccatalpha  14627  swrdfv2  14695  ccatswrd  14702  swrdccat2  14703  pfxfv  14716  pfxeq  14730  ccatpfx  14735  swrdswrd  14739  swrdpfx  14741  pfxpfx  14742  cats1un  14755  swrdccatfn  14758  swrdccatin1  14759  pfxccatin12lem4  14760  pfxccatin12lem1  14762  swrdccatin2  14763  pfxccatin12lem2c  14764  pfxccatin12lem2  14765  swrdccat3blem  14773  swrdccatin1d  14777  swrdccatin2d  14778  pfxccatin12d  14779  revccat  14800  revrev  14801  repswpfx  14819  repswccat  14820  cshwidxmod  14837  2cshw  14847  cshwcshid  14862  cshwcsh2id  14863  cshimadifsn  14864  cshimadifsn0  14865  revco  14869  ccatco  14870  cshco  14871  swrdco  14872  ofccat  15004  shftfn  15108  shftval  15109  limsupgle  15509  ello12  15548  elo12  15559  isercolllem3  15699  sumeq1  15721  fsumsplit  15773  sumsplit  15800  fsum2dlem  15802  fsumcom2  15806  fsumparts  15838  explecnv  15897  pwdif  15900  fprodser  15981  fprodsplit  15998  fprod2dlem  16012  fprodcom2  16016  eftlub  16141  divalgmod  16439  bitsval  16457  bitsp1e  16465  bitsp1o  16466  sadfval  16485  sadcp1  16488  sadval  16489  sadcadd  16491  sadadd2  16493  saddisjlem  16497  sadadd  16500  sadass  16504  smufval  16510  smuval  16514  smuval2  16515  smupvallem  16516  smu01lem  16518  smueqlem  16523  smumul  16526  bezoutlem2  16573  bezoutlem4  16575  algfx  16613  eucalgcvga  16619  reumodprminv  16837  nnnn0modprm0  16839  unbenlem  16941  prmreclem5  16953  vdwapval  17006  vdwapun  17007  vdwnnlem1  17028  vdwnn  17031  ramval  17041  0ram  17053  ramub1lem2  17060  prmgaplem7  17090  prmlem0  17139  elrest  17473  prdsbasmpt  17516  prdsleval  17523  prdsbasmpt2  17528  pwselbasb  17534  imasaddfnlem  17574  imasvscafn  17583  divsfval  17593  ismre  17634  mreunirn  17645  mrisval  17674  ismri  17675  isacs  17695  catidd  17724  iscatd2  17725  ismon  17780  isepi  17787  sectffval  17797  sectfval  17798  dfiso2  17819  cicsym  17851  issubc  17885  catsubcat  17889  isfunc  17914  funcres  17946  funcpropd  17953  ffthiso  17982  isnat  18001  isnat2  18002  fuciso  18031  initoval  18046  termoval  18047  isinito  18049  istermo  18050  iszeroo  18051  isinitoi  18052  istermoi  18053  initoid  18054  termoid  18055  iszeroi  18062  2initoinv  18063  initoeu1  18064  initoeu2  18069  2termoinv  18070  termoeu1  18071  arwhoma  18098  elsetchom  18134  setcmon  18140  setcepi  18141  setciso  18144  catciso  18164  elestrchom  18182  estrcbasbas  18185  funcestrcsetclem7  18201  funcestrcsetclem8  18202  funcestrcsetclem9  18203  fthestrcsetc  18205  fullestrcsetc  18206  equivestrcsetc  18207  setc1strwun  18208  funcsetcestrclem7  18216  funcsetcestrclem8  18217  funcsetcestrclem9  18218  fthsetcestrc  18220  fullsetcestrc  18221  hofcl  18315  hofpropd  18323  yonedalem4c  18333  yonedainv  18337  yonffthlem  18338  lubeldm  18410  glbeldm  18423  joindef  18433  meetdef  18447  poslubdg  18471  acsficl2d  18609  acsmapd  18611  psref  18631  psss  18637  dirge  18660  mgmpropd  18676  issstrmgm  18678  grpidval  18686  grpidpropd  18687  grpidd  18696  ismgmhm  18721  issubmgm  18727  issgrpd  18755  sgrppropd  18756  ismndd  18781  mndpropd  18784  imasmnd2  18799  imasmnd  18800  xpsmnd0  18803  ismhm  18810  issubm  18828  gsumsgrpccat  18865  elefmndbas2  18899  smndex1mndlem  18934  imasgrp2  19085  imasgrp  19086  issubg  19156  subginv  19163  isnsg  19185  eqg0el  19213  quselbas  19214  isghm  19245  isghmOLD  19246  resghm2b  19264  conjnmzb  19283  conjnsg  19284  ghmpropd  19286  isga  19321  elcntz  19352  elcntzsn  19355  cntzrcl  19357  resscntz  19363  symgextf1  19453  gsmsymgreqlem2  19463  f1otrspeq  19479  pmtrfrn  19490  pmtrdifellem3  19510  pmtrdifellem4  19511  psgnunilem1  19525  psgnunilem5  19526  psgnunilem2  19527  psgnunilem3  19528  psgneldm2  19536  psgnfitr  19549  psgnsn  19552  gexdvds  19616  gex1  19623  isslw  19640  sylow3lem2  19660  lsmelvalx  19672  pj1ghm  19735  efgtlen  19758  efgsfo  19771  efgredlemc  19777  frgp0  19792  frgpmhm  19797  qusabl  19897  frgpnabllem1  19905  imasabl  19908  cycsubmcmn  19921  0cyg  19925  cycsubgcyg  19933  gsumval3  19939  gsumcllem  19940  gsumzaddlem  19953  gsumzsplit  19959  gsummptfzcl  20001  eldprd  20038  dprdcntz2  20072  dprd2d2  20078  dmdprdsplit2lem  20079  dmdprdsplit2  20080  dprdsplit  20082  ablfac2  20123  isrngd  20190  rngpropd  20191  imasrng  20194  qusrng  20197  ringurd  20202  isringd  20304  imasring  20343  xpsring1d  20346  dvdsrval  20377  isunit  20389  dvdsrpropd  20432  isirred  20435  isrnghm  20457  isrngim  20461  c0ghm  20477  c0snghm  20480  isrhm  20494  isrim0OLD  20497  isrim0  20499  islring  20556  issubrng  20563  opprsubrng  20575  issubrg  20587  opprsubrg  20609  resrhm2b  20618  rhmpropd  20625  rnghmresel  20636  elrngchom  20640  rnghmsubcsetclem1  20647  rnghmsubcsetclem2  20648  rngcid  20651  rngcsect  20652  rngciso  20654  funcrngcsetcALT  20657  zrinitorngc  20658  zrtermorngc  20659  rhmresel  20665  elringchom  20669  rhmsubcsetclem1  20676  rhmsubcsetclem2  20677  ringcid  20680  rhmsscrnghm  20681  rhmsubcrngclem1  20682  rhmsubcrngclem2  20683  ringcsect  20686  ringciso  20688  ringcbasbas  20689  zrtermoringc  20691  srhmsubc  20696  rhmsubclem3  20703  rhmsubclem4  20704  drngunit  20750  isdrngd  20781  isdrngdOLD  20783  issdrg  20805  sdrgunit  20813  isabv  20828  issrngd  20872  islmod  20878  lmodprop2d  20938  islss  20949  islssd  20950  lssats2  21015  ellspsn  21018  islmhm  21043  lmhmf1o  21062  lmhmima  21063  lmhmpreima  21064  reslmhm  21068  pwssplit3  21077  lmhmpropd  21089  islbs  21092  lspprel  21110  lspfixed  21147  lbsacsbs  21175  lbsextlem1  21177  lbsextlem2  21178  lbsextlem3  21179  lbsextlem4  21180  ixpsnbasval  21232  isridlrng  21246  rnglidlmmgm  21272  isridl  21279  quscrng  21310  rngqiprngimfolem  21317  rngqiprngimf1lem  21321  rngqiprngimfo  21328  islpidl  21352  lidldvgen  21361  irinitoringc  21507  pzriprnglem13  21521  pzriprnglem14  21522  zrhrhmb  21538  znf1o  21587  frgpcyg  21609  psgnevpmb  21622  isphld  21689  phlssphl  21694  elocv  21703  iscss  21718  isobs  21757  obs2ss  21766  dsmmfi  21775  dsmmelbas  21776  dsmmlss  21781  frlmelbas  21793  frlmlbs  21834  frlmup1  21835  ellspd  21839  islinds  21846  islindf2  21851  f1lindf  21859  islindf4  21875  assamulgscmlem2  21937  psrgrp  21993  mplsubglem  22036  mpllsslem  22037  mplmonmul  22071  subrgascl  22107  subrgasclcl  22108  mpfind  22148  ismhp  22161  gsumply1subr  22250  lply1binomsc  22330  matbas2d  22444  matecl  22446  matvscl  22452  mat1  22468  mat0dim0  22488  mat0dimid  22489  mat0dimscm  22490  mat1dimelbas  22492  dmatel  22514  scmatel  22526  scmateALT  22533  scmataddcl  22537  scmatsubcl  22538  smatvscl  22545  scmatghm  22554  mat1scmat  22560  mdetunilem7  22639  mdetunilem9  22641  smadiadetr  22696  cramerimplem2  22705  cramer0  22711  pmatcoe1fsupp  22722  cpmatpmat  22731  cpmatel  22732  cpmatacl  22737  cpmatinvcl  22738  mat2pmatghm  22751  mat2pmatmul  22752  decpmatmullem  22792  pmatcollpwlem  22801  pmatcollpw3fi1lem1  22807  pmatcollpwscmatlem1  22810  monmat2matmon  22845  chfacfscmul0  22879  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  cayhamlem1  22887  cpmadugsumlemB  22895  cpmadugsumlemC  22896  cpmadugsumlemF  22897  cayhamlem2  22905  istopon  22933  eltg  22979  eltg2  22980  eltop  22996  eltop2  22997  eltop3  22998  pptbas  23030  iscld  23050  neiss2  23124  isnei  23126  neiptopnei  23155  neiptopreu  23156  lpfval  23161  lpval  23162  islp  23163  maxlp  23170  islpi  23172  neitr  23203  restlp  23206  ordtbas2  23214  ordtrest2  23227  lmfval  23255  cnfval  23256  iscn  23258  iscnp  23260  tgcn  23275  tgcnp  23276  lmbrf  23283  cnpresti  23311  ist1  23344  ist1-2  23370  cnt1  23373  haust1  23375  cmpfi  23431  cmpfii  23432  1stcfb  23468  2ndc1stc  23474  1stcrest  23476  2ndcdisj  23479  1stcelcls  23484  nllyi  23498  subislly  23504  islocfin  23540  lfinpfin  23547  locfindis  23553  locfincf  23554  comppfsc  23555  kgenval  23558  elkgen  23559  kgencn2  23580  txbas  23590  eltx  23591  ptval  23593  ptpjpre1  23594  ptopn2  23607  ptpjopn  23635  ptclsg  23638  xkoccn  23642  txdis  23655  txdis1cn  23658  ptrescn  23662  hausdiag  23668  hauseqlcld  23669  txhaus  23670  xkohaus  23676  elqtop  23720  qtopeu  23739  kqcldsat  23756  hmeofval  23781  ptuncnv  23830  ptunhmeo  23831  elmptrab  23850  fbdmn0  23857  elfg  23894  elfilss  23899  filunirn  23905  fixufil  23945  elfm  23970  rnelfmlem  23975  rnelfm  23976  fmfnfmlem4  23980  elflim2  23987  flimtopon  23993  elflim  23994  hausflim  24004  flimcls  24008  flfnei  24014  isflf  24016  hausflf  24020  cnpflf  24024  cnflf  24025  txflf  24029  isfcls  24032  fclstopon  24035  isfcls2  24036  fclssscls  24041  fclsnei  24042  fclsfnflim  24050  flimfnfcls  24051  isfcf  24057  fcfelbas  24059  cnpfcf  24064  cnfcf  24065  flfcntr  24066  alexsublem  24067  alexsubALTlem3  24072  cnextfun  24087  cnextfvval  24088  cnextf  24089  cnextcn  24090  tmdgsum2  24119  tgpconncomp  24136  ghmcnp  24138  qustgplem  24144  eltsms  24156  haustsms  24159  tsmsgsum  24162  tsmssubm  24166  tsmssplit  24175  isust  24227  ustbas  24251  elutop  24257  ustuqtoplem  24263  ustuqtop4  24268  ustuqtop  24270  utopsnneiplem  24271  utopsnneip  24272  utopsnnei  24273  isusp  24285  isucn  24302  ucncn  24309  iscfilu  24312  neipcfilu  24320  iscusp  24323  cnextucn  24327  ispsmet  24329  ismet  24348  isxmet  24349  elblps  24412  elbl  24413  elmopn  24467  prdsbl  24519  neibl  24529  met1stc  24549  metrest  24552  prdsxmslem2  24557  txmetcnp  24575  txmetcn  24576  metustsym  24583  cfilucfil2  24589  elbl4  24591  metuel  24592  psmetutop  24595  restmetu  24598  metucn  24599  tngngp  24690  isnmhm  24782  zcld  24848  metnrmlem1a  24893  elcncf  24928  cncfcnvcn  24965  cnheibor  25000  lebnumlem1  25006  ishtpy  25017  isphtpy  25026  om1elbas  25078  elpi1  25091  pi1xfr  25101  pi1coghm  25107  tcphcph  25284  lmmbrf  25309  iscfil  25312  iscau  25323  iscauf  25327  caucfil  25330  iscmet  25331  cmetcaulem  25335  iscmet3lem1  25338  iscmet3lem2  25339  iscmet3  25340  bcthlem1  25371  cmsss  25398  cmetcusp1  25400  cmetcusp  25401  cmscsscms  25420  rrxcph  25439  minveclem3b  25475  ovolfioo  25515  ovolficc  25516  ovolctb  25538  ovoliunnul  25555  ovolshftlem1  25557  sca2rab  25560  ovolscalem1  25561  ovolicc2lem1  25565  ovolicc2lem2  25566  ovolicc2lem4  25568  ovolicc2lem5  25569  iundisj  25596  iunmbl2  25605  uniioombllem3  25633  vitalilem2  25657  vitalilem3  25658  mbfss  25694  i1faddlem  25741  i1fmullem  25742  mbfi1fseqlem2  25765  mbfi1fseqlem4  25767  mbfi1fseq  25770  itg2splitlem  25797  itg2split  25798  itg2monolem1  25799  itg2gt0  25809  isibl  25814  iblss2  25855  itgss3  25864  itgsplit  25885  ellimc  25922  limcmo  25931  cnlimc  25937  limciun  25943  limcun  25944  eldv  25947  dvbsss  25951  dvreslem  25958  elcpn  25984  dvaddf  25993  dvmulf  25994  dvcof  26000  rolle  26042  dvlip2  26048  dvivthlem1  26061  lhop1  26067  lhop2  26068  ftc1cn  26098  fta1glem2  26222  plyco0  26245  elply  26248  ply1termlem  26256  eltayl  26415  tayl0  26417  taylplem1  26418  taylplem2  26419  dvtaylp  26426  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  abelth  26499  cxpcn3  26805  rlimcnp  27022  fsumharmonic  27069  dchrelbas  27294  pntrsumbnd2  27625  ostth2lem2  27692  nolesgn2ores  27731  nogesgn1ores  27733  nosupprefixmo  27759  noinfprefixmo  27760  nosupcbv  27761  nosupdm  27763  nosupfv  27765  nosupres  27766  nosupbnd1lem1  27767  nosupbnd1lem3  27769  nosupbnd1lem5  27771  nosupbnd2lem1  27774  noinfcbv  27776  noinfdm  27778  noinffv  27780  noinfres  27781  noinfbnd1lem1  27782  noinfbnd1lem3  27784  noinfbnd1lem5  27786  noinfbnd2lem1  27789  elmade  27920  elold  27922  ssltleft  27923  ssltright  27924  oldlim  27939  madebday  27952  newbday  27954  sltlpss  27959  cofcutr  27972  cofcutrtime  27975  lrrecval  27986  lrrecval2  27987  addsval  28009  precsexlem9  28253  precsexlem11  28255  sltonold  28297  noseqrdgfn  28326  istrkgb  28477  istrkgcb  28478  istrkge  28479  istrkgl  28480  istrkgld  28481  axtgsegcon  28486  axtg5seg  28487  axtgbtwnid  28488  axtgpasch  28489  axtgupdim2  28493  axtgeucl  28494  tgdim01  28529  iscgrg  28534  isismt  28556  tglnunirn  28570  tglngval  28573  tgellng  28575  legval  28606  legov  28607  legov2  28608  ishlg  28624  mirreu3  28676  mirval  28677  mirfv  28678  mircgr  28679  mirbtwn  28680  ismir  28681  mireq  28687  symquadlem  28711  israg  28719  perpln1  28732  perpln2  28733  isperp  28734  islnopp  28761  outpasch  28777  ishpg  28781  iscgra  28831  dfcgra2  28852  isinag  28860  isleag  28869  iseqlg  28889  f1otrgitv  28892  f1otrg  28893  f1otrge  28894  ttgval  28897  ttgvalOLD  28898  ttgelitv  28911  elee  28923  brbtwn  28928  brcgr  28929  axlowdimlem16  28986  ebtwntg  29011  elntg2  29014  upgrex  29123  edgupgr  29165  upgredg  29168  edglnl  29174  numedglnl  29175  uhgr2edg  29239  umgr2edg1  29242  usgredg2vlem1  29256  usgredg2vlem2  29257  ushgredgedg  29260  ushgredgedgloop  29262  uhgrspansubgrlem  29321  fusgrfisstep  29360  nbgrval  29367  nbgrel  29371  nbupgrel  29376  nbgr2vtx1edg  29381  nbuhgr2vtx1edgblem  29382  nbuhgr2vtx1edgb  29383  nbusgreledg  29384  usgrnbcnvfv  29396  uvtxval  29418  uvtxel  29419  uvtx01vtx  29428  uvtxusgrel  29434  nbcplgr  29465  cplgr3v  29466  cusgrexi  29474  structtocusgr  29477  vtxdgfval  29499  vtxdg0v  29505  vtxdeqd  29509  vtxdun  29513  1loopgrnb0  29534  1loopgrvd0  29536  1hevtxdg0  29537  1hevtxdg1  29538  1egrvtxdg1  29541  umgr2v2evtxel  29554  umgr2v2enb1  29558  umgr2v2evd2  29559  vtxdginducedm1lem4  29574  vtxdginducedm1  29575  finsumvtxdg2sstep  29581  ewlksfval  29633  isewlk  29634  wksfval  29641  iswlk  29642  uspgr2wlkeq  29678  wlkres  29702  usgr2pthlem  29795  clwlkcompim  29812  uspgrn2crct  29837  wwlks  29864  iswwlksn  29867  wwlknvtx  29874  wlkiswwlks2  29904  wwlksm1edg  29910  wwlksnred  29921  wwlksnext  29922  wwlksnredwwlkn  29924  wwlksnredwwlkn0  29925  wwlksnwwlksnon  29944  wspn0  29953  usgr2wspthons3  29993  rusgrnumwwlkb0  30000  clwwlk  30011  clwwlkccatlem  30017  clwlkclwwlklem2a4  30025  clwlkclwwlk  30030  clwwisshclwwslem  30042  clwwlkinwwlk  30068  clwwlkel  30074  clwwlkf  30075  clwwlkext2edg  30084  wwlksext2clwwlk  30085  wwlksubclwwlk  30086  clwwnisshclwwsn  30087  eleclclwwlknlem2  30089  erclwwlknsym  30098  erclwwlkntr  30099  umgrhashecclwwlk  30106  clwwlkvbij  30141  eupth2lem3lem3  30258  eupth2lem3lem4  30259  eupth2lem3lem6  30261  eupth2lemb  30265  eucrct2eupth  30273  fusgreg2wsplem  30361  2clwwlklem  30371  2clwwlk2clwwlklem  30374  2clwwlkel  30377  2clwwlk2clwwlk  30378  extwwlkfabel  30381  clwwlknonclwlknonf1o  30390  dlwwlknondlwlknonf1olem1  30392  numclwwlk2lem1  30404  numclwlk2lem2f  30405  numclwlk2lem2f1o  30407  ex-res  30469  isssp  30752  sspn  30764  islno  30781  isblo  30810  nmlno0  30823  ishmo  30839  dipdir  30870  dipass  30873  ubthlem1  30898  ubthlem2  30899  htthlem  30945  htth  30946  ocel  31309  ocnel  31326  shsel  31342  shsel2  31350  shmodsi  31417  pjhtheu  31422  pjeq  31427  axpjpj  31448  pjoc2  31467  elspani  31571  h1de2ctlem  31583  elspansn  31594  elspansn2  31595  elnlfn  31956  eleigvec  31985  riesz3i  32090  cbviunf  32575  iuneq12daf  32576  iunrdx  32583  iunrnmptss  32585  cbvdisjf  32590  disjorf  32598  disjabrex  32601  disjabrexf  32602  iundisjf  32608  disjrdx  32610  brab2d  32626  2ndresdju  32665  abfmpunirn  32668  abfmpeld  32670  abfmpel  32671  fmptcof2  32673  acunirnmpt2  32676  acunirnmpt2f  32677  aciunf1lem  32678  funcnvmpt  32683  suppss3  32741  fpwrelmap  32750  xrofsup  32777  iundisjfi  32803  eliccioo  32897  s3f1  32915  ccatf1  32917  ccatws1f1o  32920  swrdrn3  32924  ismnt  32957  mgcoval  32960  gsummpt2co  33033  gsumpart  33042  gsumhashmul  33046  xrge0tsmsbi  33048  gsumwrd2dccatlem  33051  gsumwrd2dccat  33052  cycpmco2  33135  cyc3co2  33142  inftmrel  33169  isinftm  33170  isslmd  33190  urpropd  33221  elrgspn  33235  erlval  33244  rlocval  33245  rloccring  33256  rloc1r  33258  isdrng4  33278  fracfld  33289  resv1r  33347  ellspds  33375  ellpi  33380  lbslsp  33384  rhmimaidl  33439  isprmidl  33445  qsidomlem1  33459  qsidomlem2  33460  ismxidl  33469  crngmxidl  33476  drng0mxidl  33483  opprqus0g  33497  qsfld  33505  isrprm  33524  rsprprmprmidlb  33530  ply1mulrtss  33585  dimpropd  33635  lbslsat  33643  extdg1id  33690  elirng  33700  ply1annidllem  33708  constrsuc  33742  constrconj  33749  smatrcl  33756  smatcl  33762  ist0cld  33793  txomap  33794  locfinreflem  33800  zarclsiin  33831  zart0  33839  rhmpreimacnlem  33844  metidval  33850  cnre2csqima  33871  ordtrest2NEW  33883  fmcncfil  33891  fsumcvg4  33910  ofcfval  34078  measvuni  34194  meascnbl  34199  faeval  34226  ismbfm  34231  elunirnmbfm  34232  imambfm  34243  elcarsg  34286  itgeq12dv  34307  issibf  34314  eulerpartlems  34341  eulerpartlemgc  34343  eulerpartlemgvv  34357  eulerpartlemgu  34358  eulerpart  34363  rrvmbfm  34423  elorvc  34440  elorrvc  34444  dstfrvunirn  34455  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemsima  34496  ballotlemrv  34500  fzssfzo  34532  signstfvn  34562  signstfvneq0  34565  signstres  34568  repr0  34604  reprinrn  34611  reprdifc  34620  hgt750lemg  34647  hgt750lemb  34649  istrkg2d  34659  axtgupdim2ALTV  34661  afsval  34664  brafs  34665  bnj945  34765  bnj1400  34827  bnj18eq1  34919  bnj916  34925  bnj1014  34953  bnj1015  34954  bnj1110  34974  bnj1417  35033  revpfxsfxrev  35099  cplgredgex  35104  pfxwlk  35107  revwlk  35108  subfacp1lem2b  35165  subfacp1lem4  35167  subfacp1lem5  35168  subfacp1lem6  35169  ptpconn  35217  cvmscbv  35242  iscvm  35243  cvmsi  35249  cvmsval  35250  cvmliftmolem1  35265  cvmlift2lem12  35298  cvmlift2lem13  35299  cvmlift3lem7  35309  snmlval  35315  satfv1  35347  satfvsucsuc  35349  satfrnmapom  35354  satf0op  35361  satf0n0  35362  sat1el2xp  35363  fmlafvel  35369  isfmlasuc  35372  fmlaomn0  35374  gonan0  35376  goaln0  35377  gonar  35379  goalr  35381  satffunlem1lem2  35387  satffunlem2lem2  35390  satfv0fvfmla0  35397  satef  35400  satefvfmla0  35402  sategoelfvb  35403  satfv1fvfmla1  35407  mrsubfval  35492  mrsubvrs  35506  mclsrcl  35545  mclsval  35547  mppsval  35556  mclsppslem  35567  opelco3  35755  wsuclem  35806  funtransport  36012  fvtransport  36013  brcolinear  36040  colineardim1  36042  funray  36121  fvray  36122  funline  36123  fvline  36125  lineelsb2  36129  fwddifval  36143  fwddifnval  36144  rankelg  36149  rankeq1o  36152  elhf2  36156  0hf  36158  rmoeqbidv  36194  reueqbidv  36195  disjeq12dv  36197  ixpeq12dv  36198  prodeq12sdv  36200  itgeq12sdv  36201  cbvralvw2  36208  cbvrexvw2  36209  cbvrmovw2  36210  cbvreuvw2  36211  cbvcsbvw2  36213  cbviunvw2  36214  cbviinvw2  36215  cbvmptvw2  36216  cbvdisjvw2  36217  cbvmpo1vw2  36225  cbvmpo2vw2  36226  cbvsbcdavw  36239  cbvcsbdavw  36241  cbvcsbdavw2  36242  cbviundavw  36244  cbviindavw  36245  cbvdisjdavw  36250  cbvrabdavw2  36267  cbviundavw2  36268  cbviindavw2  36269  cbvmptdavw2  36270  cbvdisjdavw2  36271  cbvriotadavw2  36272  cbvmpo1davw2  36274  cbvmpo2davw2  36275  cbvsumdavw2  36277  neibastop2lem  36342  neibastop3  36344  eltail  36356  bj-projeq  36974  bj-projval  36978  bj-restsn  37064  opelopabbv  37125  brabd0  37129  bj-eldiag  37158  bj-eldiag2  37159  mptsnunlem  37320  dissneqlem  37322  iooelexlt  37344  relowlssretop  37345  rdgellim  37358  exrecfnlem  37361  finxpeq1  37368  finxpreclem6  37378  pibp21  37397  curf  37584  uncf  37585  curunc  37588  unccur  37589  fin2so  37593  lindsadd  37599  lindsdom  37600  lindsenlbs  37601  matunitlindflem1  37602  matunitlindflem2  37603  matunitlindf  37604  ptrest  37605  ptrecube  37606  poimirlem2  37608  poimirlem8  37614  poimirlem17  37623  poimirlem18  37624  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem24  37630  poimirlem26  37632  poimirlem29  37635  heicant  37641  mblfinlem1  37643  mblfinlem2  37644  volsupnfl  37651  itg2addnclem  37657  itg2gt0cn  37661  indexdom  37720  incsequz  37734  istotbnd  37755  istotbnd3  37757  0totbnd  37759  sstotbnd  37761  sstotbnd3  37762  isbnd  37766  prdstotbnd  37780  cntotbnd  37782  isismty  37787  heibor1lem  37795  heiborlem2  37798  heiborlem3  37799  heibor  37807  isass  37832  exidcl  37862  exidreslem  37863  elghomlem2OLD  37872  rngoidmlem  37922  rngo1cl  37925  divrngcl  37943  isdrngo2  37944  isrngohom  37951  isrngoiso  37964  isriscg  37970  iscom2  37981  iscringd  37984  isidl  38000  ispridl  38020  ismaxidl  38026  ac6s6  38158  dmecd  38285  releldmqs  38639  releldmqscoss  38641  erimeq2  38659  eldisjlem19  38791  membpartlem19  38792  prter3  38863  islshp  38960  islsat  38972  lcvfbr  39001  islfl  39041  ellkr  39070  islshpkrN  39101  ldual1dim  39147  isopos  39161  cmtfvalN  39191  cvrfval  39249  isat  39267  islln  39488  islpln  39512  islvol  39555  isline  39721  ispointN  39724  ispsubsp  39727  elpmap  39740  elpmapat  39746  elpadd  39781  paddclN  39824  elpclN  39874  elpcliN  39875  pclfinN  39882  pclcmpatN  39883  ispsubclN  39919  iswatN  39976  islhp  39978  islaut  40065  ispautN  40081  isldil  40092  isltrn  40101  isdilN  40136  istrnN  40139  istendo  40742  dvhb1dimN  40968  erng1lem  40969  erngdvlem4-rN  40981  diaelval  41015  diaeldm  41018  dia1dimid  41045  cdlemm10N  41100  dibopelvalN  41125  dibopelval2  41127  dibelval3  41129  dibelval1st  41131  dibelval2nd  41134  dibeldmN  41140  dibvalrel  41145  dibglbN  41148  dicffval  41156  dicfval  41157  dicopelval  41159  dicelvalN  41160  dicelval3  41162  dicvalrelN  41167  dicelval1sta  41169  diclspsn  41176  dihopelvalbN  41220  dihopelvalcqat  41228  dihopelvalcpre  41230  dihvalrel  41261  dih1  41268  dihmeetlem4preN  41288  dihmeetlem13N  41301  dih1dimatlem  41311  dochnel2  41374  dihjatcclem4  41403  dvh2dim  41427  dvh3dim  41428  dvh4dimN  41429  dochfln0  41459  lpolsetN  41464  islpolN  41465  lcfrvalsnN  41523  lcfrlem21  41545  lcfrlem27  41551  lcfrlem37  41561  lcfr  41567  lcdlss  41601  mapdcv  41642  hdmap1fval  41778  hdmapffval  41808  hdmapfval  41809  hdmapval  41810  hgmapffval  41867  hgmapfval  41868  hdmapellkr  41896  hlhilhillem  41946  fzsplitnd  41963  isprimroot  42074  primrootsunit1  42078  primrootscoprmpow  42080  primrootscoprbij  42083  aks6d1c1p2  42090  aks6d1c1p3  42091  aks6d1c1p4  42092  aks6d1c1p5  42093  aks6d1c1p6  42095  aks6d1c1  42097  evl1gprodd  42098  sticksstones11  42137  sticksstones12a  42138  rhmqusspan  42166  grpods  42175  fzosumm1  42269  frlmfielbas  42486  frlmsnic  42526  psrmnd  42531  isnacs  42691  mrefg2  42694  elmzpcl  42713  mzpcompact2  42739  eldiophb  42744  elpell1qr  42834  elpell14qr  42836  elpell1234qr  42838  pw2f1ocnv  43025  pw2f1o2val2  43028  aomclem4  43045  aomclem6  43047  islssfg2  43059  imasgim  43088  lnr2i  43104  elmnc  43124  rngunsnply  43157  onexomgt  43229  onexlimgt  43231  onexoegt  43232  oaordnr  43285  omnord1  43294  oenord1  43305  cantnfresb  43313  tfsconcatun  43326  tfsconcat0i  43334  ofoaf  43344  naddcnff  43351  naddcnffo  43353  naddcnfcom  43355  naddcnfid1  43356  naddcnfid2  43357  naddcnfass  43358  naddwordnexlem4  43390  fiinfi  43562  sqrtcvallem1  43620  elintima  43642  eliunov2  43668  ov2ssiunov2  43689  brtrclfv2  43716  rfovcnvf1od  43993  rfovcnvfvd  43996  fsovrfovd  43998  fsovfvd  43999  fsovcnvlem  44002  ntrclsfv1  44044  ntrclselnel1  44046  ntrclsneine0lem  44053  ntrneifv1  44068  ntrneifv2  44069  ntrneiel  44070  gneispace2  44121  gneispacess2  44135  extoimad  44153  mnringelbased  44209  dvconstbi  44329  bccbc  44340  eliin2f  45043  iineq12dv  45045  rabbida2  45071  disjinfi  45134  unirnmap  45150  elmptima  45202  iuneqfzuzlem  45283  iooiinioc  45508  fsumiunss  45530  fsumsupp0  45533  lptre2pt  45595  icccncfext  45842  cncfiooicclem1  45848  dvnprodlem2  45902  stoweidlem27  45982  stoweidlem29  45984  stoweidlem31  45986  stoweidlem34  45989  stoweidlem48  46003  stoweidlem59  46014  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem2  46064  fourierdlem3  46065  fourierdlem25  46087  fourierdlem32  46094  fourierdlem33  46095  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  fourierdlem62  46123  fourierdlem70  46131  fourierdlem80  46141  fourierdlem92  46153  fourierdlem93  46154  fourierdlem101  46162  etransclem37  46226  sge0val  46321  sge0f1o  46337  sge0iunmptlemre  46370  sge0iunmpt  46373  iundjiun  46415  caragenel  46450  ovncvrrp  46519  ovnsubaddlem1  46525  ovnsubadd  46527  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  hoidmvle  46555  ovncvr2  46566  hspdifhsp  46571  hoiqssbl  46580  hspmbllem2  46582  hspmbl  46584  opnvonmbllem1  46587  isvonmbl  46593  ovnovollem1  46611  issmflem  46682  smflimlem3  46728  smflimlem4  46729  smflim  46732  smfmullem2  46747  smflimmpt  46765  smfsuplem1  46766  smflimsuplem1  46775  smflimsuplem3  46777  smflimsuplem4  46778  smflimsuplem7  46781  smflimsup  46783  tworepnotupword  46839  fcores  47016  fcoresf1  47018  afvelrnb  47112  afvelrnb0  47113  afv2co2  47206  el1fzopredsuc  47274  iccpart  47340  iccpartgtprec  47344  iccpartiltu  47346  iccpartigtl  47347  iccpartltu  47349  iccpartgtl  47350  iccpartgt  47351  iccpartleu  47352  iccpartgel  47353  iccelpart  47357  iccpartiun  47358  icceuelpart  47360  fargshiftfv  47363  fargshiftfo  47366  sprel  47408  prprelb  47440  prprelprb  47441  fpprel  47652  sbgoldbo  47711  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  bgoldbtbndlem3  47731  bgoldbtbnd  47733  clnbgrval  47746  elclnbgrelnbgr  47749  clnbgrel  47752  clnbupgrel  47758  vopnbgrel  47777  isubgredg  47789  uspgrimprop  47810  grtriprop  47845  isgrtri  47847  grtriclwlk3  47849  stgredgel  47859  gpgvtxel  47940  gpgedgel  47942  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  upwlksfval  47978  isupwlk  47979  intop  48046  isclintop  48050  assintop  48052  isassintop  48053  assintopcllaw  48055  uzlidlring  48078  elrngchomALTV  48112  rngccatidALTV  48115  rngcsectALTV  48118  rngcisoALTV  48120  rhmsubcALTVlem3  48126  rhmsubcALTVlem4  48127  funcringcsetcALTV2lem7  48139  funcringcsetcALTV2lem9  48141  elringchomALTV  48146  ringccatidALTV  48149  ringcsectALTV  48152  ringcisoALTV  48154  ringcbasbasALTV  48155  funcringcsetclem7ALTV  48162  funcringcsetclem9ALTV  48164  srhmsubcALTV  48168  opeliun2xp  48177  cbvmpox2  48180  ply1sclrmsm  48228  dmatALTbasel  48247  lcoval  48257  lindslinindsimp1  48302  lindslinindsimp2  48308  lmod1  48337  elbigo  48400  elbigo2  48401  elbigolo1  48406  dig2nn0ld  48453  naryfvalel  48479  rrxlines  48582  rrxlinesc  48584  rrxlinec  48585  eenglngeehlnm  48588  elrrx2linest2  48594  rrxsphere  48597  itsclc0  48620  itsclc0b  48621  itsclinecirc0  48622  itsclinecirc0b  48623  itscnhlinecirc02p  48634  f1omo  48690  lubeldm2d  48754  glbeldm2d  48755  catprs  48799  isthinc  48820  isthincd2lem1  48826  thincmoALT  48829  thincmod  48830  isthincd  48836  prsthinc  48854  elsetrecslem  48929