Theorem eleq2d 2817

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

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

This theorem is referenced by:  eleq2  2820  eleq12d  2825  eleqtrd  2833  neleqtrd  2853  eqabrd  2873  raleqbidv  3312  rexeqbidv  3313  reueqbidv  3384  rabeqbidva  3411  elabd2  3620  sbcbid  3791  csbeq2d  3851  csbeq2dv  3852  cbvcsbw  3855  cbvcsb  3856  cbvcsbv  3857  csbie  3880  csbied  3881  csbie2g  3885  cbvralcsf  3887  cbvreucsf  3889  cbvrabcsf  3890  sbcel12  4356  sbcel1g  4361  sbcel2  4363  prel12g  4811  eliuni  4942  iuneqconst  4948  iuneq12df  4963  iuneq12d  4966  cbviun  4980  cbviin  4981  cbviung  4982  cbviing  4983  cbviunv  4984  cbviinv  4985  iinxsng  5031  iinxprg  5032  iunxsng  5033  iunxsngf  5035  cbvdisj  5063  cbvdisjv  5064  disjor  5068  disjiund  5077  mpteq12da  5169  mpteq12f  5171  mpteq12dva  5172  axpweq  5284  rabxfrd  5350  rbropapd  5497  opeliunxp  5678  opeliun2xp  5679  opeliunxp2  5773  iunxpf  5783  elimampt  5987  elrelimasn  6030  elimasni  6035  imadifssran  6093  xpdifid  6110  ressn  6227  funfni  6582  fnbr  6584  dffv3  6813  elfv2ex  6860  fvelrnb  6877  foelcdmi  6878  fvun1  6908  fvco2  6914  elfvmptrab1w  6951  elfvmptrab1  6952  elfvmptrab  6953  elpreima  6986  dff3  7028  fmptco  7057  fnelfp  7104  fnelnfp  7106  tpres  7130  fnprb  7137  fntpb  7138  funfvima3  7165  eluniima  7179  dff13  7183  f1ounsn  7201  f1eqcocnv  7230  isoini  7267  riotaeqdv  7299  mpoeq123dva  7415  cbvmpox  7434  elimampo  7478  ovelrn  7517  elovmpod  7585  elovmpo  7586  elovmporab  7587  elovmporab1w  7588  elovmporab1  7589  elovmpt3rab1  7601  fiun  7870  f1iun  7871  zfrep6  7882  fmpox  7994  el2mpocsbcl  8010  el2mpocl  8011  bropopvvv  8015  bropfvvvv  8017  xpord2indlem  8072  xpord3inddlem  8079  elsuppfng  8094  elsuppfn  8095  suppfnss  8114  opeliunxp2f  8135  mpoxopn0yelv  8138  mpoxopovel  8145  rntpos  8164  mpocurryd  8194  fpr2  8229  wfr2  8252  onoviun  8258  smoel  8275  smoiso  8277  smoel2  8278  smo11  8279  tfrlem9  8299  oalimcl  8470  oaass  8471  omordi  8476  omordlim  8487  omlimcl  8488  odi  8489  omeulem1  8492  omeulem2  8493  oen0  8496  oeordi  8497  oeordsuc  8504  oelimcl  8510  oeeulem  8511  oeeui  8512  nnmordi  8541  oaabs2  8559  omabs  8561  omsmolem  8567  ereldm  8670  iiner  8708  elmapg  8758  elpmg  8762  elixpsn  8856  ixpsnf1o  8857  boxriin  8859  omxpenlem  8986  pw2f1olem  8989  phplem2  9109  php3  9113  infn0  9181  elfi  9292  dffi3  9310  marypha2lem2  9315  ordiso2  9396  wemapsolem  9431  elharval  9442  inf3lemd  9512  inf3lem1  9513  inf3lem2  9514  inf3lem3  9515  cantnfs  9551  cantnfp1lem3  9565  cantnflem1b  9571  cantnflem1  9574  ttrclselem2  9611  trcl  9613  frr2  9648  r1sdom  9662  r1ordg  9666  r1pwss  9672  tz9.12lem3  9677  tz9.12  9678  r1elwf  9684  rankr1ai  9686  rankidb  9688  rankr1bg  9691  rankval2  9706  rankunb  9738  tcrank  9772  acni  9931  acni2  9932  acndom  9937  infpwfien  9948  alephnbtwn  9957  cardaleph  9975  cardinfima  9983  iunfictbso  10000  dfac3  10007  dfac5lem5  10013  dfac5  10015  dfac9  10023  dfac12r  10033  kmlem2  10038  kmlem12  10048  kmlem13  10049  kmlem14  10050  ackbij2lem3  10126  ackbij2  10128  cofsmo  10155  alephsing  10162  fin23lem30  10228  isf32lem9  10247  itunisuc  10305  axcc2lem  10322  axcc3  10324  domtriomlem  10328  axdc2lem  10334  axdc2  10335  axdc3lem2  10337  axdc3lem4  10339  axdc4lem  10341  ac6c4  10367  zorn2lem1  10382  ttukeylem6  10400  pwcfsdom  10469  axregndlem2  10489  axinfndlem1  10491  axacndlem4  10496  axacnd  10498  pwfseqlem1  10544  inar1  10661  inatsk  10664  gruurn  10684  grur1  10706  eltskm  10729  genpelv  10886  eluz1  12731  eluzaddOLD  12762  eluzsubOLD  12763  elixx1  13249  elixx3g  13253  elioo2  13281  elfz1  13407  elfz2  13409  elfzp1  13469  fzpr  13474  fzsuc2  13477  fzrev3  13485  elfzp12  13498  fzm1  13502  elfzo  13556  fz0add1fz1  13630  elfzo0l  13651  elfzom1b  13661  fzosplitsni  13674  elfzr  13676  elfzlmr  13677  zmodidfzo  13799  seqp1  13918  seqf1o  13945  bcval  14206  bcpasc  14223  hashf1lem1  14357  fundmge2nop0  14404  wrdmap  14448  elovmpowrd  14460  ccatfval  14475  elfzelfzccat  14482  ccatlid  14489  ccatass  14491  ccatrn  14492  ccatalpha  14496  swrdfv2  14564  ccatswrd  14571  swrdccat2  14572  pfxfv  14585  pfxeq  14598  ccatpfx  14603  swrdswrd  14607  swrdpfx  14609  pfxpfx  14610  cats1un  14623  swrdccatfn  14626  swrdccatin1  14627  pfxccatin12lem4  14628  pfxccatin12lem1  14630  swrdccatin2  14631  pfxccatin12lem2c  14632  pfxccatin12lem2  14633  swrdccat3blem  14641  swrdccatin1d  14645  swrdccatin2d  14646  pfxccatin12d  14647  revccat  14668  revrev  14669  repswpfx  14687  repswccat  14688  cshwidxmod  14705  2cshw  14715  cshwcshid  14729  cshwcsh2id  14730  cshimadifsn  14731  cshimadifsn0  14732  revco  14736  ccatco  14737  cshco  14738  swrdco  14739  ofccat  14871  shftfn  14975  shftval  14976  limsupgle  15379  ello12  15418  elo12  15429  isercolllem3  15569  sumeq1  15591  fsumsplit  15643  sumsplit  15670  fsum2dlem  15672  fsumcom2  15676  fsumparts  15708  explecnv  15767  pwdif  15770  fprodser  15851  fprodsplit  15868  fprod2dlem  15882  fprodcom2  15886  eftlub  16013  divalgmod  16312  bitsval  16330  bitsp1e  16338  bitsp1o  16339  sadfval  16358  sadcp1  16361  sadval  16362  sadcadd  16364  sadadd2  16366  saddisjlem  16370  sadadd  16373  sadass  16377  smufval  16383  smuval  16387  smuval2  16388  smupvallem  16389  smu01lem  16391  smueqlem  16396  smumul  16399  bezoutlem2  16446  bezoutlem4  16448  algfx  16486  eucalgcvga  16492  reumodprminv  16711  nnnn0modprm0  16713  unbenlem  16815  prmreclem5  16827  vdwapval  16880  vdwapun  16881  vdwnnlem1  16902  vdwnn  16905  ramval  16915  0ram  16927  ramub1lem2  16934  prmgaplem7  16964  prmlem0  17012  elrest  17326  prdsbasmpt  17369  prdsleval  17376  prdsbasmpt2  17381  pwselbasb  17387  imasaddfnlem  17427  imasvscafn  17436  divsfval  17446  ismre  17487  mreunirn  17498  mrisval  17531  ismri  17532  isacs  17552  catidd  17581  iscatd2  17582  ismon  17635  isepi  17642  sectffval  17652  sectfval  17653  dfiso2  17674  cicsym  17706  issubc  17737  catsubcat  17741  isfunc  17766  funcres  17798  funcpropd  17804  ffthiso  17833  isnat  17852  isnat2  17853  fuciso  17880  initoval  17895  termoval  17896  isinito  17898  istermo  17899  iszeroo  17900  isinitoi  17901  istermoi  17902  initoid  17903  termoid  17904  iszeroi  17911  2initoinv  17912  initoeu1  17913  initoeu2  17918  2termoinv  17919  termoeu1  17920  arwhoma  17947  elsetchom  17983  setcmon  17989  setcepi  17990  setciso  17993  catciso  18013  elestrchom  18029  estrcbasbas  18032  funcestrcsetclem7  18047  funcestrcsetclem8  18048  funcestrcsetclem9  18049  fthestrcsetc  18051  fullestrcsetc  18052  equivestrcsetc  18053  setc1strwun  18054  funcsetcestrclem7  18062  funcsetcestrclem8  18063  funcsetcestrclem9  18064  fthsetcestrc  18066  fullsetcestrc  18067  hofcl  18160  hofpropd  18168  yonedalem4c  18178  yonedainv  18182  yonffthlem  18183  lubeldm  18252  glbeldm  18265  joindef  18275  meetdef  18289  poslubdg  18313  acsficl2d  18453  acsmapd  18455  psref  18475  psss  18481  dirge  18504  chnccats1  18526  chnccat  18527  chnrev  18528  mgmpropd  18554  issstrmgm  18556  grpidval  18564  grpidpropd  18565  grpidd  18574  ismgmhm  18599  issubmgm  18605  issgrpd  18633  sgrppropd  18634  ismndd  18659  mndpropd  18662  imasmnd2  18677  imasmnd  18678  xpsmnd0  18681  ismhm  18688  issubm  18706  gsumsgrpccat  18743  elefmndbas2  18777  smndex1mndlem  18812  imasgrp2  18963  imasgrp  18964  issubg  19034  subginv  19041  isnsg  19062  eqg0el  19090  quselbas  19091  isghm  19122  isghmOLD  19123  resghm2b  19141  conjnmzb  19160  conjnsg  19161  ghmpropd  19163  isga  19198  elcntz  19229  elcntzsn  19232  cntzrcl  19234  resscntz  19240  symgextf1  19328  gsmsymgreqlem2  19338  f1otrspeq  19354  pmtrfrn  19365  pmtrdifellem3  19385  pmtrdifellem4  19386  psgnunilem1  19400  psgnunilem5  19401  psgnunilem2  19402  psgnunilem3  19403  psgneldm2  19411  psgnfitr  19424  psgnsn  19427  gexdvds  19491  gex1  19498  isslw  19515  sylow3lem2  19535  lsmelvalx  19547  pj1ghm  19610  efgtlen  19633  efgsfo  19646  efgredlemc  19652  frgp0  19667  frgpmhm  19672  qusabl  19772  frgpnabllem1  19780  imasabl  19783  cycsubmcmn  19796  0cyg  19800  cycsubgcyg  19808  gsumval3  19814  gsumcllem  19815  gsumzaddlem  19828  gsumzsplit  19834  gsummptfzcl  19876  eldprd  19913  dprdcntz2  19947  dprd2d2  19953  dmdprdsplit2lem  19954  dmdprdsplit2  19955  dprdsplit  19957  ablfac2  19998  isrngd  20086  rngpropd  20087  imasrng  20090  qusrng  20093  ringurd  20098  isringd  20204  imasring  20243  xpsring1d  20246  dvdsrval  20274  isunit  20286  dvdsrpropd  20329  isirred  20332  isrnghm  20354  isrngim  20358  c0ghm  20374  c0snghm  20377  isrhm  20391  isrim0  20395  islring  20450  issubrng  20457  opprsubrng  20469  issubrg  20481  opprsubrg  20503  resrhm2b  20512  rhmpropd  20519  rnghmresel  20530  elrngchom  20534  rnghmsubcsetclem1  20541  rnghmsubcsetclem2  20542  rngcid  20545  rngcsect  20546  rngciso  20548  funcrngcsetcALT  20551  zrinitorngc  20552  zrtermorngc  20553  rhmresel  20559  elringchom  20563  rhmsubcsetclem1  20570  rhmsubcsetclem2  20571  ringcid  20574  rhmsscrnghm  20575  rhmsubcrngclem1  20576  rhmsubcrngclem2  20577  ringcsect  20580  ringciso  20582  ringcbasbas  20583  zrtermoringc  20585  srhmsubc  20590  rhmsubclem3  20597  rhmsubclem4  20598  drngunit  20644  isdrngd  20675  isdrngdOLD  20677  issdrg  20698  sdrgunit  20706  isabv  20721  issrngd  20765  islmod  20792  lmodprop2d  20852  islss  20862  islssd  20863  lssats2  20928  ellspsn  20931  islmhm  20956  lmhmf1o  20975  lmhmima  20976  lmhmpreima  20977  reslmhm  20981  pwssplit3  20990  lmhmpropd  21002  islbs  21005  lspprel  21023  lspfixed  21060  lbsacsbs  21088  lbsextlem1  21090  lbsextlem2  21091  lbsextlem3  21092  lbsextlem4  21093  ixpsnbasval  21137  isridlrng  21151  rnglidlmmgm  21177  isridl  21184  quscrng  21215  rngqiprngimfolem  21222  rngqiprngimf1lem  21226  rngqiprngimfo  21233  islpidl  21257  lidldvgen  21266  irinitoringc  21411  pzriprnglem13  21425  pzriprnglem14  21426  zrhrhmb  21442  znf1o  21483  frgpcyg  21505  psgnevpmb  21519  isphld  21586  phlssphl  21591  elocv  21600  iscss  21615  isobs  21652  obs2ss  21661  dsmmfi  21670  dsmmelbas  21671  dsmmlss  21676  frlmelbas  21688  frlmlbs  21729  frlmup1  21730  ellspd  21734  islinds  21741  islindf2  21746  f1lindf  21754  islindf4  21770  assamulgscmlem2  21832  psrgrp  21888  mplsubglem  21931  mpllsslem  21932  mplmonmul  21966  subrgascl  21996  subrgasclcl  21997  mpfind  22037  ismhp  22050  gsumply1subr  22141  lply1binomsc  22221  matbas2d  22333  matecl  22335  matvscl  22341  mat1  22357  mat0dim0  22377  mat0dimid  22378  mat0dimscm  22379  mat1dimelbas  22381  dmatel  22403  scmatel  22415  scmateALT  22422  scmataddcl  22426  scmatsubcl  22427  smatvscl  22434  scmatghm  22443  mat1scmat  22449  mdetunilem7  22528  mdetunilem9  22530  smadiadetr  22585  cramerimplem2  22594  cramer0  22600  pmatcoe1fsupp  22611  cpmatpmat  22620  cpmatel  22621  cpmatacl  22626  cpmatinvcl  22627  mat2pmatghm  22640  mat2pmatmul  22641  decpmatmullem  22681  pmatcollpwlem  22690  pmatcollpw3fi1lem1  22696  pmatcollpwscmatlem1  22699  monmat2matmon  22734  chfacfscmul0  22768  chfacfscmulgsum  22770  chfacfpmmulgsum  22774  cayhamlem1  22776  cpmadugsumlemB  22784  cpmadugsumlemC  22785  cpmadugsumlemF  22786  cayhamlem2  22794  istopon  22822  eltg  22867  eltg2  22868  eltop  22884  eltop2  22885  eltop3  22886  pptbas  22918  iscld  22937  neiss2  23011  isnei  23013  neiptopnei  23042  neiptopreu  23043  lpfval  23048  lpval  23049  islp  23050  maxlp  23057  islpi  23059  neitr  23090  restlp  23093  ordtbas2  23101  ordtrest2  23114  lmfval  23142  cnfval  23143  iscn  23145  iscnp  23147  tgcn  23162  tgcnp  23163  lmbrf  23170  cnpresti  23198  ist1  23231  ist1-2  23257  cnt1  23260  haust1  23262  cmpfi  23318  cmpfii  23319  1stcfb  23355  2ndc1stc  23361  1stcrest  23363  2ndcdisj  23366  1stcelcls  23371  nllyi  23385  subislly  23391  islocfin  23427  lfinpfin  23434  locfindis  23440  locfincf  23441  comppfsc  23442  kgenval  23445  elkgen  23446  kgencn2  23467  txbas  23477  eltx  23478  ptval  23480  ptpjpre1  23481  ptopn2  23494  ptpjopn  23522  ptclsg  23525  xkoccn  23529  txdis  23542  txdis1cn  23545  ptrescn  23549  hausdiag  23555  hauseqlcld  23556  txhaus  23557  xkohaus  23563  elqtop  23607  qtopeu  23626  kqcldsat  23643  hmeofval  23668  ptuncnv  23717  ptunhmeo  23718  elmptrab  23737  fbdmn0  23744  elfg  23781  elfilss  23786  filunirn  23792  fixufil  23832  elfm  23857  rnelfmlem  23862  rnelfm  23863  fmfnfmlem4  23867  elflim2  23874  flimtopon  23880  elflim  23881  hausflim  23891  flimcls  23895  flfnei  23901  isflf  23903  hausflf  23907  cnpflf  23911  cnflf  23912  txflf  23916  isfcls  23919  fclstopon  23922  isfcls2  23923  fclssscls  23928  fclsnei  23929  fclsfnflim  23937  flimfnfcls  23938  isfcf  23944  fcfelbas  23946  cnpfcf  23951  cnfcf  23952  flfcntr  23953  alexsublem  23954  alexsubALTlem3  23959  cnextfun  23974  cnextfvval  23975  cnextf  23976  cnextcn  23977  tmdgsum2  24006  tgpconncomp  24023  ghmcnp  24025  qustgplem  24031  eltsms  24043  haustsms  24046  tsmsgsum  24049  tsmssubm  24053  tsmssplit  24062  isust  24114  ustbas  24137  elutop  24143  ustuqtoplem  24149  ustuqtop4  24154  ustuqtop  24156  utopsnneiplem  24157  utopsnneip  24158  utopsnnei  24159  isusp  24171  isucn  24187  ucncn  24194  iscfilu  24197  neipcfilu  24205  iscusp  24208  cnextucn  24212  ispsmet  24214  ismet  24233  isxmet  24234  elblps  24297  elbl  24298  elmopn  24352  prdsbl  24401  neibl  24411  met1stc  24431  metrest  24434  prdsxmslem2  24439  txmetcnp  24457  txmetcn  24458  metustsym  24465  cfilucfil2  24471  elbl4  24473  metuel  24474  psmetutop  24477  restmetu  24480  metucn  24481  tngngp  24564  isnmhm  24656  zcld  24724  metnrmlem1a  24769  elcncf  24804  cncfcnvcn  24841  cnheibor  24876  lebnumlem1  24882  ishtpy  24893  isphtpy  24902  om1elbas  24954  elpi1  24967  pi1xfr  24977  pi1coghm  24983  tcphcph  25159  lmmbrf  25184  iscfil  25187  iscau  25198  iscauf  25202  caucfil  25205  iscmet  25206  cmetcaulem  25210  iscmet3lem1  25213  iscmet3lem2  25214  iscmet3  25215  bcthlem1  25246  cmsss  25273  cmetcusp1  25275  cmetcusp  25276  cmscsscms  25295  rrxcph  25314  minveclem3b  25350  ovolfioo  25390  ovolficc  25391  ovolctb  25413  ovoliunnul  25430  ovolshftlem1  25432  sca2rab  25435  ovolscalem1  25436  ovolicc2lem1  25440  ovolicc2lem2  25441  ovolicc2lem4  25443  ovolicc2lem5  25444  iundisj  25471  iunmbl2  25480  uniioombllem3  25508  vitalilem2  25532  vitalilem3  25533  mbfss  25569  i1faddlem  25616  i1fmullem  25617  mbfi1fseqlem2  25639  mbfi1fseqlem4  25641  mbfi1fseq  25644  itg2splitlem  25671  itg2split  25672  itg2monolem1  25673  itg2gt0  25683  isibl  25688  iblss2  25729  itgss3  25738  itgsplit  25759  ellimc  25796  limcmo  25805  cnlimc  25811  limciun  25817  limcun  25818  eldv  25821  dvbsss  25825  dvreslem  25832  elcpn  25858  dvaddf  25867  dvmulf  25868  dvcof  25874  rolle  25916  dvlip2  25922  dvivthlem1  25935  lhop1  25941  lhop2  25942  ftc1cn  25972  fta1glem2  26096  plyco0  26119  elply  26122  ply1termlem  26130  eltayl  26289  tayl0  26291  taylplem1  26292  taylplem2  26293  dvtaylp  26300  taylthlem1  26303  taylthlem2  26304  taylthlem2OLD  26305  abelth  26373  cxpcn3  26680  rlimcnp  26897  fsumharmonic  26944  dchrelbas  27169  pntrsumbnd2  27500  ostth2lem2  27567  nolesgn2ores  27606  nogesgn1ores  27608  nosupprefixmo  27634  noinfprefixmo  27635  nosupcbv  27636  nosupdm  27638  nosupfv  27640  nosupres  27641  nosupbnd1lem1  27642  nosupbnd1lem3  27644  nosupbnd1lem5  27646  nosupbnd2lem1  27649  noinfcbv  27651  noinfdm  27653  noinffv  27655  noinfres  27656  noinfbnd1lem1  27657  noinfbnd1lem3  27659  noinfbnd1lem5  27661  noinfbnd2lem1  27664  elmade  27807  elold  27809  ssltleft  27810  ssltright  27811  oldlim  27827  madebday  27840  newbday  27842  sltlpss  27848  bdayiun  27855  cofcutr  27863  cofcutrtime  27866  lrrecval  27877  lrrecval2  27878  addsval  27900  precsexlem9  28148  precsexlem11  28150  sltonold  28193  onnolt  28198  onslt  28199  noseqrdgfn  28231  istrkgb  28428  istrkgcb  28429  istrkge  28430  istrkgl  28431  istrkgld  28432  axtgsegcon  28437  axtg5seg  28438  axtgbtwnid  28439  axtgpasch  28440  axtgupdim2  28444  axtgeucl  28445  tgdim01  28480  iscgrg  28485  isismt  28507  tglnunirn  28521  tglngval  28524  tgellng  28526  legval  28557  legov  28558  legov2  28559  ishlg  28575  mirreu3  28627  mirval  28628  mirfv  28629  mircgr  28630  mirbtwn  28631  ismir  28632  mireq  28638  symquadlem  28662  israg  28670  perpln1  28683  perpln2  28684  isperp  28685  islnopp  28712  outpasch  28728  ishpg  28732  iscgra  28782  dfcgra2  28803  isinag  28811  isleag  28820  iseqlg  28840  f1otrgitv  28843  f1otrg  28844  f1otrge  28845  ttgval  28848  ttgelitv  28856  elee  28867  brbtwn  28872  brcgr  28873  axlowdimlem16  28930  ebtwntg  28955  elntg2  28958  upgrex  29065  edgupgr  29107  upgredg  29110  edglnl  29116  numedglnl  29117  uhgr2edg  29181  umgr2edg1  29184  usgredg2vlem1  29198  usgredg2vlem2  29199  ushgredgedg  29202  ushgredgedgloop  29204  uhgrspansubgrlem  29263  fusgrfisstep  29302  nbgrval  29309  nbgrel  29313  nbupgrel  29318  nbgr2vtx1edg  29323  nbuhgr2vtx1edgblem  29324  nbuhgr2vtx1edgb  29325  nbusgreledg  29326  usgrnbcnvfv  29338  uvtxval  29360  uvtxel  29361  uvtx01vtx  29370  uvtxusgrel  29376  nbcplgr  29407  cplgr3v  29408  cusgrexi  29416  structtocusgr  29419  vtxdgfval  29441  vtxdg0v  29447  vtxdeqd  29451  vtxdun  29455  1loopgrnb0  29476  1loopgrvd0  29478  1hevtxdg0  29479  1hevtxdg1  29480  1egrvtxdg1  29483  umgr2v2evtxel  29496  umgr2v2enb1  29500  umgr2v2evd2  29501  vtxdginducedm1lem4  29516  vtxdginducedm1  29517  finsumvtxdg2sstep  29523  ewlksfval  29575  isewlk  29576  wksfval  29583  iswlk  29584  uspgr2wlkeq  29619  wlkres  29642  dfpth2  29702  usgr2pthlem  29736  clwlkcompim  29753  uspgrn2crct  29781  wwlks  29808  iswwlksn  29811  wwlknvtx  29818  wlkiswwlks2  29848  wwlksm1edg  29854  wwlksnred  29865  wwlksnext  29866  wwlksnredwwlkn  29868  wwlksnredwwlkn0  29869  wwlksnwwlksnon  29888  wspn0  29897  usgr2wspthons3  29937  rusgrnumwwlkb0  29944  clwwlk  29955  clwwlkccatlem  29961  clwlkclwwlklem2a4  29969  clwlkclwwlk  29974  clwwisshclwwslem  29986  clwwlkinwwlk  30012  clwwlkel  30018  clwwlkf  30019  clwwlkext2edg  30028  wwlksext2clwwlk  30029  wwlksubclwwlk  30030  clwwnisshclwwsn  30031  eleclclwwlknlem2  30033  erclwwlknsym  30042  erclwwlkntr  30043  umgrhashecclwwlk  30050  clwwlkvbij  30085  eupth2lem3lem3  30202  eupth2lem3lem4  30203  eupth2lem3lem6  30205  eupth2lemb  30209  eucrct2eupth  30217  fusgreg2wsplem  30305  2clwwlklem  30315  2clwwlk2clwwlklem  30318  2clwwlkel  30321  2clwwlk2clwwlk  30322  extwwlkfabel  30325  clwwlknonclwlknonf1o  30334  dlwwlknondlwlknonf1olem1  30336  numclwwlk2lem1  30348  numclwlk2lem2f  30349  numclwlk2lem2f1o  30351  ex-res  30413  isssp  30696  sspn  30708  islno  30725  isblo  30754  nmlno0  30767  ishmo  30783  dipdir  30814  dipass  30817  ubthlem1  30842  ubthlem2  30843  htthlem  30889  htth  30890  ocel  31253  ocnel  31270  shsel  31286  shsel2  31294  shmodsi  31361  pjhtheu  31366  pjeq  31371  axpjpj  31392  pjoc2  31411  elspani  31515  h1de2ctlem  31527  elspansn  31538  elspansn2  31539  elnlfn  31900  eleigvec  31929  riesz3i  32034  cbviunf  32527  iuneq12daf  32528  iunrdx  32535  iunrnmptss  32537  cbvdisjf  32543  disjorf  32551  disjabrex  32554  disjabrexf  32555  iundisjf  32561  disjrdx  32563  brab2d  32580  2ndresdju  32623  abfmpunirn  32626  abfmpeld  32628  abfmpel  32629  fmptcof2  32631  acunirnmpt2  32634  acunirnmpt2f  32635  aciunf1lem  32636  funcnvmpt  32641  suppss3  32698  fpwrelmap  32708  xrofsup  32742  iundisjfi  32770  eliccioo  32903  s3f1  32920  ccatf1  32922  ccatws1f1o  32924  swrdrn3  32928  ismnt  32956  mgcoval  32959  gsummpt2co  33020  gsumpart  33029  gsumhashmul  33033  xrge0tsmsbi  33035  gsumwrd2dccatlem  33038  gsumwrd2dccat  33039  cycpmco2  33094  cyc3co2  33101  isfxp  33129  cntrval2  33132  inftmrel  33141  isinftm  33142  isslmd  33163  urpropd  33191  elrgspn  33205  erlval  33217  rlocval  33218  rloccring  33229  rloc1r  33231  domnpropd  33235  isdrng4  33253  fracfld  33266  resv1r  33296  ellspds  33325  ellpi  33330  lbslsp  33334  rhmimaidl  33389  isprmidl  33395  qsidomlem1  33409  qsidomlem2  33410  ismxidl  33419  crngmxidl  33426  drng0mxidl  33433  opprqus0g  33447  qsfld  33455  isrprm  33474  rsprprmprmidlb  33480  ressply1evls1  33520  ply1mulrtss  33537  dimpropd  33613  lbslsat  33621  extdg1id  33671  fldextrspunlsplem  33678  fldextrspunlsp  33679  elirng  33691  ply1annidllem  33706  constrsuc  33743  constrconj  33750  constrllcllem  33757  constrlccllem  33758  constrcccllem  33759  nn0constr  33766  smatrcl  33801  smatcl  33807  ist0cld  33838  txomap  33839  locfinreflem  33845  zarclsiin  33876  zart0  33884  rhmpreimacnlem  33889  metidval  33895  cnre2csqima  33916  ordtrest2NEW  33928  fmcncfil  33936  fsumcvg4  33955  ofcfval  34103  measvuni  34219  meascnbl  34224  faeval  34251  ismbfm  34256  elunirnmbfm  34257  imambfm  34267  elcarsg  34310  itgeq12dv  34331  issibf  34338  eulerpartlems  34365  eulerpartlemgc  34367  eulerpartlemgvv  34381  eulerpartlemgu  34382  eulerpart  34387  rrvmbfm  34447  elorvc  34465  elorrvc  34469  dstfrvunirn  34480  ballotlemfc0  34498  ballotlemfcc  34499  ballotlemsima  34521  ballotlemrv  34525  fzssfzo  34544  signstfvn  34574  signstfvneq0  34577  signstres  34580  repr0  34616  reprinrn  34623  reprdifc  34632  hgt750lemg  34659  hgt750lemb  34661  istrkg2d  34671  axtgupdim2ALTV  34673  afsval  34676  brafs  34677  bnj945  34777  bnj1400  34839  bnj18eq1  34931  bnj916  34937  bnj1014  34965  bnj1015  34966  bnj1110  34986  bnj1417  35045  rankval2b  35102  r1filimi  35106  r1ssel  35110  onvf1odlem3  35141  vonf1owev  35144  revpfxsfxrev  35152  cplgredgex  35157  pfxwlk  35160  revwlk  35161  subfacp1lem2b  35217  subfacp1lem4  35219  subfacp1lem5  35220  subfacp1lem6  35221  ptpconn  35269  cvmscbv  35294  iscvm  35295  cvmsi  35301  cvmsval  35302  cvmliftmolem1  35317  cvmlift2lem12  35350  cvmlift2lem13  35351  cvmlift3lem7  35361  snmlval  35367  satfv1  35399  satfvsucsuc  35401  satfrnmapom  35406  satf0op  35413  satf0n0  35414  sat1el2xp  35415  fmlafvel  35421  isfmlasuc  35424  fmlaomn0  35426  gonan0  35428  goaln0  35429  gonar  35431  goalr  35433  satffunlem1lem2  35439  satffunlem2lem2  35442  satfv0fvfmla0  35449  satef  35452  satefvfmla0  35454  sategoelfvb  35455  satfv1fvfmla1  35459  mrsubfval  35544  mrsubvrs  35558  mclsrcl  35597  mclsval  35599  mppsval  35608  mclsppslem  35619  opelco3  35811  wsuclem  35859  funtransport  36065  fvtransport  36066  brcolinear  36093  colineardim1  36095  funray  36174  fvray  36175  funline  36176  fvline  36178  lineelsb2  36182  fwddifval  36196  fwddifnval  36197  rankelg  36202  rankeq1o  36205  elhf2  36209  0hf  36211  rmoeqbidv  36247  disjeq12dv  36249  ixpeq12dv  36250  prodeq12sdv  36252  itgeq12sdv  36253  cbvralvw2  36260  cbvrexvw2  36261  cbvrmovw2  36262  cbvreuvw2  36263  cbvcsbvw2  36265  cbviunvw2  36266  cbviinvw2  36267  cbvmptvw2  36268  cbvdisjvw2  36269  cbvmpo1vw2  36277  cbvmpo2vw2  36278  cbvsbcdavw  36291  cbvcsbdavw  36293  cbvcsbdavw2  36294  cbviundavw  36296  cbviindavw  36297  cbvdisjdavw  36302  cbvrabdavw2  36319  cbviundavw2  36320  cbviindavw2  36321  cbvmptdavw2  36322  cbvdisjdavw2  36323  cbvriotadavw2  36324  cbvmpo1davw2  36326  cbvmpo2davw2  36327  cbvsumdavw2  36329  neibastop2lem  36394  neibastop3  36396  eltail  36408  bj-projeq  37026  bj-projval  37030  bj-restsn  37116  opelopabbv  37177  brabd0  37181  bj-eldiag  37210  bj-eldiag2  37211  mptsnunlem  37372  dissneqlem  37374  iooelexlt  37396  relowlssretop  37397  rdgellim  37410  exrecfnlem  37413  finxpeq1  37420  finxpreclem6  37430  pibp21  37449  curf  37638  uncf  37639  curunc  37642  unccur  37643  fin2so  37647  lindsadd  37653  lindsdom  37654  lindsenlbs  37655  matunitlindflem1  37656  matunitlindflem2  37657  matunitlindf  37658  ptrest  37659  ptrecube  37660  poimirlem2  37662  poimirlem8  37668  poimirlem17  37677  poimirlem18  37678  poimirlem20  37680  poimirlem21  37681  poimirlem22  37682  poimirlem24  37684  poimirlem26  37686  poimirlem29  37689  heicant  37695  mblfinlem1  37697  mblfinlem2  37698  volsupnfl  37705  itg2addnclem  37711  itg2gt0cn  37715  indexdom  37774  incsequz  37788  istotbnd  37809  istotbnd3  37811  0totbnd  37813  sstotbnd  37815  sstotbnd3  37816  isbnd  37820  prdstotbnd  37834  cntotbnd  37836  isismty  37841  heibor1lem  37849  heiborlem2  37852  heiborlem3  37853  heibor  37861  isass  37886  exidcl  37916  exidreslem  37917  elghomlem2OLD  37926  rngoidmlem  37976  rngo1cl  37979  divrngcl  37997  isdrngo2  37998  isrngohom  38005  isrngoiso  38018  isriscg  38024  iscom2  38035  iscringd  38038  isidl  38054  ispridl  38074  ismaxidl  38080  ac6s6  38212  dmecd  38338  releldmqs  38696  releldmqscoss  38698  erimeq2  38716  eldisjlem19  38848  membpartlem19  38849  prter3  38921  islshp  39018  islsat  39030  lcvfbr  39059  islfl  39099  ellkr  39128  islshpkrN  39159  ldual1dim  39205  isopos  39219  cmtfvalN  39249  cvrfval  39307  isat  39325  islln  39545  islpln  39569  islvol  39612  isline  39778  ispointN  39781  ispsubsp  39784  elpmap  39797  elpmapat  39803  elpadd  39838  paddclN  39881  elpclN  39931  elpcliN  39932  pclfinN  39939  pclcmpatN  39940  ispsubclN  39976  iswatN  40033  islhp  40035  islaut  40122  ispautN  40138  isldil  40149  isltrn  40158  isdilN  40193  istrnN  40196  istendo  40799  dvhb1dimN  41025  erng1lem  41026  erngdvlem4-rN  41038  diaelval  41072  diaeldm  41075  dia1dimid  41102  cdlemm10N  41157  dibopelvalN  41182  dibopelval2  41184  dibelval3  41186  dibelval1st  41188  dibelval2nd  41191  dibeldmN  41197  dibvalrel  41202  dibglbN  41205  dicffval  41213  dicfval  41214  dicopelval  41216  dicelvalN  41217  dicelval3  41219  dicvalrelN  41224  dicelval1sta  41226  diclspsn  41233  dihopelvalbN  41277  dihopelvalcqat  41285  dihopelvalcpre  41287  dihvalrel  41318  dih1  41325  dihmeetlem4preN  41345  dihmeetlem13N  41358  dih1dimatlem  41368  dochnel2  41431  dihjatcclem4  41460  dvh2dim  41484  dvh3dim  41485  dvh4dimN  41486  dochfln0  41516  lpolsetN  41521  islpolN  41522  lcfrvalsnN  41580  lcfrlem21  41602  lcfrlem27  41608  lcfrlem37  41618  lcfr  41624  lcdlss  41658  mapdcv  41699  hdmap1fval  41835  hdmapffval  41865  hdmapfval  41866  hdmapval  41867  hgmapffval  41924  hgmapfval  41925  hdmapellkr  41953  hlhilhillem  41999  fzsplitnd  42015  isprimroot  42126  primrootsunit1  42130  primrootscoprmpow  42132  primrootscoprbij  42135  aks6d1c1p2  42142  aks6d1c1p3  42143  aks6d1c1p4  42144  aks6d1c1p5  42145  aks6d1c1p6  42147  aks6d1c1  42149  evl1gprodd  42150  sticksstones11  42189  sticksstones12a  42190  rhmqusspan  42218  grpods  42227  fzosumm1  42283  frlmfielbas  42533  frlmsnic  42573  psrmnd  42578  isnacs  42737  mrefg2  42740  elmzpcl  42759  mzpcompact2  42785  eldiophb  42790  elpell1qr  42880  elpell14qr  42882  elpell1234qr  42884  pw2f1ocnv  43070  pw2f1o2val2  43073  aomclem4  43090  aomclem6  43092  islssfg2  43104  imasgim  43133  lnr2i  43149  elmnc  43169  rngunsnply  43202  onexomgt  43274  onexlimgt  43276  onexoegt  43277  oaordnr  43329  omnord1  43338  oenord1  43349  cantnfresb  43357  tfsconcatun  43370  tfsconcat0i  43378  ofoaf  43388  naddcnff  43395  naddcnffo  43397  naddcnfcom  43399  naddcnfid1  43400  naddcnfid2  43401  naddcnfass  43402  naddwordnexlem4  43434  fiinfi  43606  sqrtcvallem1  43664  elintima  43686  eliunov2  43712  ov2ssiunov2  43733  brtrclfv2  43760  rfovcnvf1od  44037  rfovcnvfvd  44040  fsovrfovd  44042  fsovfvd  44043  fsovcnvlem  44046  ntrclsfv1  44088  ntrclselnel1  44090  ntrclsneine0lem  44097  ntrneifv1  44112  ntrneifv2  44113  ntrneiel  44114  gneispace2  44165  gneispacess2  44179  extoimad  44197  mnringelbased  44250  dvconstbi  44367  bccbc  44378  wfac8prim  45035  permaxrep  45039  permac8prim  45047  eliin2f  45141  iineq12dv  45143  rabbida2  45169  disjinfi  45229  unirnmap  45245  elmptima  45295  iuneqfzuzlem  45373  iooiinioc  45596  fsumiunss  45615  fsumsupp0  45618  lptre2pt  45678  icccncfext  45925  cncfiooicclem1  45931  dvnprodlem2  45985  stoweidlem27  46065  stoweidlem29  46067  stoweidlem31  46069  stoweidlem34  46072  stoweidlem48  46086  stoweidlem59  46097  dirkercncflem2  46142  dirkercncflem4  46144  fourierdlem2  46147  fourierdlem3  46148  fourierdlem25  46170  fourierdlem32  46177  fourierdlem33  46178  fourierdlem41  46186  fourierdlem48  46192  fourierdlem49  46193  fourierdlem62  46206  fourierdlem70  46214  fourierdlem80  46224  fourierdlem92  46236  fourierdlem93  46237  fourierdlem101  46245  etransclem37  46309  sge0val  46404  sge0f1o  46420  sge0iunmptlemre  46453  sge0iunmpt  46456  iundjiun  46498  caragenel  46533  ovncvrrp  46602  ovnsubaddlem1  46608  ovnsubadd  46610  hoidmvlelem2  46634  hoidmvlelem3  46635  hoidmvlelem4  46636  hoidmvle  46638  ovncvr2  46649  hspdifhsp  46654  hoiqssbl  46663  hspmbllem2  46665  hspmbl  46667  opnvonmbllem1  46670  isvonmbl  46676  ovnovollem1  46694  issmflem  46765  smflimlem3  46811  smflimlem4  46812  smflim  46815  smfmullem2  46830  smflimmpt  46848  smfsuplem1  46849  smflimsuplem1  46858  smflimsuplem3  46860  smflimsuplem4  46861  smflimsuplem7  46864  smflimsup  46866  fcores  47098  fcoresf1  47100  afvelrnb  47194  afvelrnb0  47195  afv2co2  47288  el1fzopredsuc  47356  iccpart  47447  iccpartgtprec  47451  iccpartiltu  47453  iccpartigtl  47454  iccpartltu  47456  iccpartgtl  47457  iccpartgt  47458  iccpartleu  47459  iccpartgel  47460  iccelpart  47464  iccpartiun  47465  icceuelpart  47467  fargshiftfv  47470  fargshiftfo  47473  sprel  47515  prprelb  47547  prprelprb  47548  fpprel  47759  sbgoldbo  47818  wtgoldbnnsum4prm  47833  bgoldbnnsum3prm  47835  bgoldbtbndlem3  47838  bgoldbtbnd  47840  clnbgrval  47853  elclnbgrelnbgr  47856  clnbgrel  47859  clnbupgrel  47865  vopnbgrel  47885  isubgredg  47897  upgrimwlklem3  47930  upgrimwlklem5  47932  upgrimpths  47940  grtriprop  47972  isgrtri  47974  grtriclwlk3  47976  stgredgel  47988  gpgvtxel  48078  gpgiedgdmel  48080  gpgedgel  48081  opgpgvtx  48086  gpg5nbgrvtx13starlem1  48102  gpg5nbgrvtx13starlem2  48103  gpg5nbgrvtx13starlem3  48104  gpg3kgrtriex  48120  grlimedgnedg  48162  upwlksfval  48166  isupwlk  48167  intop  48234  isclintop  48238  assintop  48240  isassintop  48241  assintopcllaw  48243  uzlidlring  48266  elrngchomALTV  48300  rngccatidALTV  48303  rngcsectALTV  48306  rngcisoALTV  48308  rhmsubcALTVlem3  48314  rhmsubcALTVlem4  48315  funcringcsetcALTV2lem7  48327  funcringcsetcALTV2lem9  48329  elringchomALTV  48334  ringccatidALTV  48337  ringcsectALTV  48340  ringcisoALTV  48342  ringcbasbasALTV  48343  funcringcsetclem7ALTV  48350  funcringcsetclem9ALTV  48352  srhmsubcALTV  48356  cbvmpox2  48367  ply1sclrmsm  48415  dmatALTbasel  48434  lcoval  48444  lindslinindsimp1  48489  lindslinindsimp2  48495  lmod1  48524  elbigo  48583  elbigo2  48584  elbigolo1  48589  dig2nn0ld  48636  naryfvalel  48662  rrxlines  48765  rrxlinesc  48767  rrxlinec  48768  eenglngeehlnm  48771  elrrx2linest2  48777  rrxsphere  48780  itsclc0  48803  itsclc0b  48804  itsclinecirc0  48805  itsclinecirc0b  48806  itscnhlinecirc02p  48817  brab2dd  48859  f1omo  48924  f1omoOLD  48925  lubeldm2d  48989  glbeldm2d  48990  catprs  49043  sectpropdlem  49068  nelsubc3lem  49102  initc  49123  imaid  49186  upfval  49208  upfval2  49209  upfval3  49210  uppropd  49213  oppcinito  49267  oppctermo  49268  oppczeroo  49269  initopropd  49275  termopropd  49276  isthinc  49451  isthincd2lem1  49457  thincmoALT  49461  thincmod  49462  isthincd  49468  thincpropd  49474  indcthing  49492  discthing  49493  prsthinc  49496  termcterm  49545  termc2  49550  isinito4  49579  2arwcatlem1  49627  setc1onsubc  49634  cnelsubclem  49635  ranval3  49663  lmdfval2  49687  cmdfval2  49688  termolmd  49702  elsetrecslem  49731