Theorem eleq2d 2814

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 2720	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	1, 2	sylib 217	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		anbi2 632	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	alexbii 1827	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	syl 17	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
7		dfclel 2806	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
8		dfclel 2806	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4g 313	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394  ∀wal 1531   = wceq 1533  ∃wex 1773   ∈ wcel 2098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2719  df-clel 2805

This theorem is referenced by:  eleq2  2817  eleq12d  2822  eleqtrd  2830  neleqtrd  2850  eqabrd  2871  nfceqdfOLD  2894  drnfc1OLD  2919  drnfc2OLD  2921  raleqbidv  3338  rexeqbidv  3339  elabd2  3658  sbcbid  3835  csbeq2d  3898  cbvcsbw  3902  cbvcsb  3903  csbie  3928  csbied  3930  csbie2g  3935  cbvralcsf  3937  cbvreucsf  3939  cbvrabcsf  3940  sbcel12  4410  sbcel1g  4415  sbcel2  4417  prel12g  4867  eliuni  5004  iuneqconst  5009  iuneq12df  5024  cbviun  5041  cbviin  5042  cbviung  5043  cbviing  5044  iinxsng  5093  iinxprg  5094  iunxsng  5095  iunxsngf  5097  cbvdisj  5125  disjor  5130  disjiund  5140  mpteq12da  5235  mpteq12dfOLD  5237  mpteq12f  5238  mpteq12dva  5239  axpweq  5352  rabxfrd  5419  rbropapd  5568  opeliunxp  5747  opeliunxp2  5843  iunxpf  5853  elrelimasn  6092  elimasngOLD  6097  elimasni  6098  xpdifid  6175  ressn  6292  predbrg  6330  funfni  6663  fnbr  6665  dffv3  6896  elfv2ex  6946  fvelrnb  6962  foelcdmi  6963  fvun1  6992  fvco2  6998  elfvmptrab1w  7035  elfvmptrab1  7036  elfvmptrab  7037  elpreima  7070  dff3  7113  fmptco  7142  fnelfp  7188  fnelnfp  7190  tpres  7217  fnprb  7224  fntpb  7225  funfvima3  7252  eluniima  7264  elunirn2OLD  7267  dff13  7269  f1eqcocnv  7314  f1eqcocnvOLD  7315  isoini  7350  riotaeqdv  7381  mpoeq123dva  7498  cbvmpox  7517  elimampo  7562  ovelrn  7601  elovmpod  7669  elovmpo  7670  elovmporab  7671  elovmporab1w  7672  elovmporab1  7673  elovmpt3rab1  7685  fiun  7950  f1iun  7951  zfrep6  7962  fmpox  8075  el2mpocsbcl  8094  el2mpocl  8095  bropopvvv  8099  bropfvvvv  8101  xpord2indlem  8156  xpord3inddlem  8163  elsuppfng  8178  elsuppfn  8179  suppfnss  8198  opeliunxp2f  8220  mpoxopn0yelv  8223  mpoxopovel  8230  rntpos  8249  mpocurryd  8279  fpr2  8314  wfrdmclOLD  8342  wfrlem12OLD  8345  wfr2  8361  onoviun  8368  smoel  8385  smoiso  8387  smoel2  8388  smo11  8389  tfrlem9  8410  oalimcl  8585  oaass  8586  omordi  8591  omordlim  8602  omlimcl  8603  odi  8604  omeulem1  8607  omeulem2  8608  oen0  8611  oeordi  8612  oeordsuc  8619  oelimcl  8625  oeeulem  8626  oeeui  8627  nnmordi  8656  oaabs2  8674  omabs  8676  omsmolem  8682  ereldm  8778  iiner  8812  elmapg  8862  elpmg  8866  elixpsn  8960  ixpsnf1o  8961  boxriin  8963  omxpenlem  9102  pw2f1olem  9105  phplem2  9237  php3  9241  phplem4OLD  9249  php3OLD  9253  infn0  9336  elfi  9442  dffi3  9460  marypha2lem2  9465  ordiso2  9544  wemapsolem  9579  elharval  9590  inf3lemd  9656  inf3lem1  9657  inf3lem2  9658  inf3lem3  9659  cantnfs  9695  cantnfp1lem3  9709  cantnflem1b  9715  cantnflem1  9718  ttrclselem2  9755  trcl  9757  frr2  9789  r1sdom  9803  r1ordg  9807  r1pwss  9813  tz9.12lem3  9818  tz9.12  9819  r1elwf  9825  rankr1ai  9827  rankidb  9829  rankr1bg  9832  rankval2  9847  rankunb  9879  tcrank  9913  acni  10074  acni2  10075  acndom  10080  infpwfien  10091  alephnbtwn  10100  cardaleph  10118  cardinfima  10126  iunfictbso  10143  dfac3  10150  dfac5lem5  10156  dfac5  10157  dfac9  10165  dfac12r  10175  kmlem2  10180  kmlem12  10190  kmlem13  10191  kmlem14  10192  ackbij2lem3  10270  ackbij2  10272  cofsmo  10298  alephsing  10305  fin23lem30  10371  isf32lem9  10390  itunisuc  10448  axcc2lem  10465  axcc3  10467  domtriomlem  10471  axdc2lem  10477  axdc2  10478  axdc3lem2  10480  axdc3lem4  10482  axdc4lem  10484  ac6c4  10510  zorn2lem1  10525  ttukeylem6  10543  pwcfsdom  10612  axregndlem2  10632  axinfndlem1  10634  axacndlem4  10639  axacnd  10641  pwfseqlem1  10687  inar1  10804  inatsk  10807  gruurn  10827  grur1  10849  eltskm  10872  genpelv  11029  eluz1  12862  eluzaddOLD  12893  eluzsubOLD  12894  elixx1  13371  elixx3g  13375  elioo2  13403  elfz1  13527  elfz2  13529  elfzp1  13589  fzpr  13594  fzsuc2  13597  fzrev3  13605  elfzp12  13618  fzm1  13619  elfzo  13672  fz0add1fz1  13740  elfzo0l  13760  elfzom1b  13769  fzosplitsni  13781  elfzr  13783  elfzlmr  13784  zmodidfzo  13903  seqp1  14019  seqf1o  14046  bcval  14301  bcpasc  14318  hashf1lem1  14453  hashf1lem1OLD  14454  fundmge2nop0  14491  wrdmap  14534  elovmpowrd  14546  ccatfval  14561  elfzelfzccat  14568  ccatlid  14574  ccatass  14576  ccatrn  14577  ccatalpha  14581  swrdfv2  14649  ccatswrd  14656  swrdccat2  14657  pfxfv  14670  pfxeq  14684  ccatpfx  14689  swrdswrd  14693  swrdpfx  14695  pfxpfx  14696  cats1un  14709  swrdccatfn  14712  swrdccatin1  14713  pfxccatin12lem4  14714  pfxccatin12lem1  14716  swrdccatin2  14717  pfxccatin12lem2c  14718  pfxccatin12lem2  14719  swrdccat3blem  14727  swrdccatin1d  14731  swrdccatin2d  14732  pfxccatin12d  14733  revccat  14754  revrev  14755  repswpfx  14773  repswccat  14774  cshwidxmod  14791  2cshw  14801  cshwcshid  14816  cshwcsh2id  14817  cshimadifsn  14818  cshimadifsn0  14819  revco  14823  ccatco  14824  cshco  14825  swrdco  14826  ofccat  14954  shftfn  15058  shftval  15059  limsupgle  15459  ello12  15498  elo12  15509  isercolllem3  15651  sumeq1  15673  fsumsplit  15725  sumsplit  15752  fsum2dlem  15754  fsumcom2  15758  fsumparts  15790  explecnv  15849  pwdif  15852  fprodser  15931  fprodsplit  15948  fprod2dlem  15962  fprodcom2  15966  eftlub  16091  divalgmod  16388  bitsval  16404  bitsp1e  16412  bitsp1o  16413  sadfval  16432  sadcp1  16435  sadval  16436  sadcadd  16438  sadadd2  16440  saddisjlem  16444  sadadd  16447  sadass  16451  smufval  16457  smuval  16461  smuval2  16462  smupvallem  16463  smu01lem  16465  smueqlem  16470  smumul  16473  bezoutlem2  16521  bezoutlem4  16523  algfx  16556  eucalgcvga  16562  reumodprminv  16778  nnnn0modprm0  16780  unbenlem  16882  prmreclem5  16894  vdwapval  16947  vdwapun  16948  vdwnnlem1  16969  vdwnn  16972  ramval  16982  0ram  16994  ramub1lem2  17001  prmgaplem7  17031  prmlem0  17080  elrest  17414  prdsbasmpt  17457  prdsleval  17464  prdsbasmpt2  17469  pwselbasb  17475  imasaddfnlem  17515  imasvscafn  17524  divsfval  17534  ismre  17575  mreunirn  17586  mrisval  17615  ismri  17616  isacs  17636  catidd  17665  iscatd2  17666  ismon  17721  isepi  17728  sectffval  17738  sectfval  17739  dfiso2  17760  cicsym  17792  issubc  17826  catsubcat  17830  isfunc  17855  funcres  17887  funcpropd  17894  ffthiso  17923  isnat  17942  isnat2  17943  fuciso  17972  initoval  17987  termoval  17988  isinito  17990  istermo  17991  iszeroo  17992  isinitoi  17993  istermoi  17994  initoid  17995  termoid  17996  iszeroi  18003  2initoinv  18004  initoeu1  18005  initoeu2  18010  2termoinv  18011  termoeu1  18012  arwhoma  18039  elsetchom  18075  setcmon  18081  setcepi  18082  setciso  18085  catciso  18105  elestrchom  18123  estrcbasbas  18126  funcestrcsetclem7  18142  funcestrcsetclem8  18143  funcestrcsetclem9  18144  fthestrcsetc  18146  fullestrcsetc  18147  equivestrcsetc  18148  setc1strwun  18149  funcsetcestrclem7  18157  funcsetcestrclem8  18158  funcsetcestrclem9  18159  fthsetcestrc  18161  fullsetcestrc  18162  hofcl  18256  hofpropd  18264  yonedalem4c  18274  yonedainv  18278  yonffthlem  18279  lubeldm  18350  glbeldm  18363  joindef  18373  meetdef  18387  poslubdg  18411  acsficl2d  18549  acsmapd  18551  psref  18571  psss  18577  dirge  18600  mgmpropd  18616  issstrmgm  18618  grpidval  18626  grpidpropd  18627  grpidd  18636  ismgmhm  18661  issubmgm  18667  issgrpd  18695  sgrppropd  18696  ismndd  18721  mndpropd  18724  imasmnd2  18736  imasmnd  18737  xpsmnd0  18740  ismhm  18747  issubm  18760  gsumsgrpccat  18797  elefmndbas2  18831  smndex1mndlem  18866  imasgrp2  19016  imasgrp  19017  issubg  19086  subginv  19093  isnsg  19115  eqg0el  19143  quselbas  19144  isghm  19175  resghm2b  19193  conjnmzb  19212  conjnsg  19213  ghmpropd  19215  isga  19247  elcntz  19278  elcntzsn  19281  cntzrcl  19283  resscntz  19289  symgextf1  19381  gsmsymgreqlem2  19391  f1otrspeq  19407  pmtrfrn  19418  pmtrdifellem3  19438  pmtrdifellem4  19439  psgnunilem1  19453  psgnunilem5  19454  psgnunilem2  19455  psgnunilem3  19456  psgneldm2  19464  psgnfitr  19477  psgnsn  19480  gexdvds  19544  gex1  19551  isslw  19568  sylow3lem2  19588  lsmelvalx  19600  pj1ghm  19663  efgtlen  19686  efgsfo  19699  efgredlemc  19705  frgp0  19720  frgpmhm  19725  qusabl  19825  frgpnabllem1  19833  imasabl  19836  cycsubmcmn  19849  0cyg  19853  cycsubgcyg  19861  gsumval3  19867  gsumcllem  19868  gsumzaddlem  19881  gsumzsplit  19887  gsummptfzcl  19929  eldprd  19966  dprdcntz2  20000  dprd2d2  20006  dmdprdsplit2lem  20007  dmdprdsplit2  20008  dprdsplit  20010  ablfac2  20051  isrngd  20118  rngpropd  20119  imasrng  20122  qusrng  20125  ringurd  20130  isringd  20232  imasring  20271  xpsring1d  20274  dvdsrval  20305  isunit  20317  dvdsrpropd  20360  isirred  20363  isrnghm  20385  isrngim  20389  c0ghm  20405  c0snghm  20408  isrhm  20422  isrim0OLD  20425  isrim0  20427  islring  20482  issubrng  20489  opprsubrng  20501  issubrg  20515  opprsubrg  20537  resrhm2b  20546  rhmpropd  20553  rnghmresel  20558  elrngchom  20562  rnghmsubcsetclem1  20569  rnghmsubcsetclem2  20570  rngcid  20573  rngcsect  20574  rngciso  20576  funcrngcsetcALT  20579  zrinitorngc  20580  zrtermorngc  20581  rhmresel  20587  elringchom  20591  rhmsubcsetclem1  20598  rhmsubcsetclem2  20599  ringcid  20602  rhmsscrnghm  20603  rhmsubcrngclem1  20604  rhmsubcrngclem2  20605  ringcsect  20608  ringciso  20610  ringcbasbas  20611  zrtermoringc  20613  srhmsubc  20618  rhmsubclem3  20625  rhmsubclem4  20626  drngunit  20634  isdrngd  20662  isdrngdOLD  20664  issdrg  20681  sdrgunit  20689  isabv  20704  issrngd  20746  islmod  20752  lmodprop2d  20812  islss  20823  islssd  20824  lssats2  20889  lspsnel  20892  islmhm  20917  lmhmf1o  20936  lmhmima  20937  lmhmpreima  20938  reslmhm  20942  pwssplit3  20951  lmhmpropd  20963  islbs  20966  lspprel  20984  lspfixed  21021  lbsacsbs  21049  lbsextlem1  21051  lbsextlem2  21052  lbsextlem3  21053  lbsextlem4  21054  ixpsnbasval  21106  isridlrng  21120  rnglidlmmgm  21145  isridl  21151  quscrng  21180  rngqiprngimfolem  21185  rngqiprngimf1lem  21189  rngqiprngimfo  21196  islpidl  21220  lidldvgen  21229  irinitoringc  21410  pzriprnglem13  21424  pzriprnglem14  21425  zrhrhmb  21441  znf1o  21490  frgpcyg  21512  psgnevpmb  21524  isphld  21591  phlssphl  21596  elocv  21605  iscss  21620  isobs  21659  obs2ss  21668  dsmmfi  21677  dsmmelbas  21678  dsmmlss  21683  frlmelbas  21695  frlmlbs  21736  frlmup1  21737  ellspd  21741  islinds  21748  islindf2  21753  f1lindf  21761  islindf4  21777  assamulgscmlem2  21838  psrgrp  21904  mplsubglem  21946  mpllsslem  21947  mplmonmul  21979  subrgascl  22015  subrgasclcl  22016  mpfind  22058  ismhp  22070  mhplss  22084  gsumply1subr  22157  lply1binomsc  22235  matbas2d  22343  matecl  22345  matvscl  22351  mat1  22367  mat0dim0  22387  mat0dimid  22388  mat0dimscm  22389  mat1dimelbas  22391  dmatel  22413  scmatel  22425  scmateALT  22432  scmataddcl  22436  scmatsubcl  22437  smatvscl  22444  scmatghm  22453  mat1scmat  22459  mdetunilem7  22538  mdetunilem9  22540  smadiadetr  22595  cramerimplem2  22604  cramer0  22610  pmatcoe1fsupp  22621  cpmatpmat  22630  cpmatel  22631  cpmatacl  22636  cpmatinvcl  22637  mat2pmatghm  22650  mat2pmatmul  22651  decpmatmullem  22691  pmatcollpwlem  22700  pmatcollpw3fi1lem1  22706  pmatcollpwscmatlem1  22709  monmat2matmon  22744  chfacfscmul0  22778  chfacfscmulgsum  22780  chfacfpmmulgsum  22784  cayhamlem1  22786  cpmadugsumlemB  22794  cpmadugsumlemC  22795  cpmadugsumlemF  22796  cayhamlem2  22804  istopon  22832  eltg  22878  eltg2  22879  eltop  22895  eltop2  22896  eltop3  22897  pptbas  22929  iscld  22949  neiss2  23023  isnei  23025  neiptopnei  23054  neiptopreu  23055  lpfval  23060  lpval  23061  islp  23062  maxlp  23069  islpi  23071  neitr  23102  restlp  23105  ordtbas2  23113  ordtrest2  23126  lmfval  23154  cnfval  23155  iscn  23157  iscnp  23159  tgcn  23174  tgcnp  23175  lmbrf  23182  cnpresti  23210  ist1  23243  ist1-2  23269  cnt1  23272  haust1  23274  cmpfi  23330  cmpfii  23331  1stcfb  23367  2ndc1stc  23373  1stcrest  23375  2ndcdisj  23378  1stcelcls  23383  nllyi  23397  subislly  23403  islocfin  23439  lfinpfin  23446  locfindis  23452  locfincf  23453  comppfsc  23454  kgenval  23457  elkgen  23458  kgencn2  23479  txbas  23489  eltx  23490  ptval  23492  ptpjpre1  23493  ptopn2  23506  ptpjopn  23534  ptclsg  23537  xkoccn  23541  txdis  23554  txdis1cn  23557  ptrescn  23561  hausdiag  23567  hauseqlcld  23568  txhaus  23569  xkohaus  23575  elqtop  23619  qtopeu  23638  kqcldsat  23655  hmeofval  23680  ptuncnv  23729  ptunhmeo  23730  elmptrab  23749  fbdmn0  23756  elfg  23793  elfilss  23798  filunirn  23804  fixufil  23844  elfm  23869  rnelfmlem  23874  rnelfm  23875  fmfnfmlem4  23879  elflim2  23886  flimtopon  23892  elflim  23893  hausflim  23903  flimcls  23907  flfnei  23913  isflf  23915  hausflf  23919  cnpflf  23923  cnflf  23924  txflf  23928  isfcls  23931  fclstopon  23934  isfcls2  23935  fclssscls  23940  fclsnei  23941  fclsfnflim  23949  flimfnfcls  23950  isfcf  23956  fcfelbas  23958  cnpfcf  23963  cnfcf  23964  flfcntr  23965  alexsublem  23966  alexsubALTlem3  23971  cnextfun  23986  cnextfvval  23987  cnextf  23988  cnextcn  23989  tmdgsum2  24018  tgpconncomp  24035  ghmcnp  24037  qustgplem  24043  eltsms  24055  haustsms  24058  tsmsgsum  24061  tsmssubm  24065  tsmssplit  24074  isust  24126  ustbas  24150  elutop  24156  ustuqtoplem  24162  ustuqtop4  24167  ustuqtop  24169  utopsnneiplem  24170  utopsnneip  24171  utopsnnei  24172  isusp  24184  isucn  24201  ucncn  24208  iscfilu  24211  neipcfilu  24219  iscusp  24222  cnextucn  24226  ispsmet  24228  ismet  24247  isxmet  24248  elblps  24311  elbl  24312  elmopn  24366  prdsbl  24418  neibl  24428  met1stc  24448  metrest  24451  prdsxmslem2  24456  txmetcnp  24474  txmetcn  24475  metustsym  24482  cfilucfil2  24488  elbl4  24490  metuel  24491  psmetutop  24494  restmetu  24497  metucn  24498  tngngp  24589  isnmhm  24681  zcld  24747  metnrmlem1a  24792  elcncf  24827  cncfcnvcn  24864  cnheibor  24899  lebnumlem1  24905  ishtpy  24916  isphtpy  24925  om1elbas  24977  elpi1  24990  pi1xfr  25000  pi1coghm  25006  tcphcph  25183  lmmbrf  25208  iscfil  25211  iscau  25222  iscauf  25226  caucfil  25229  iscmet  25230  cmetcaulem  25234  iscmet3lem1  25237  iscmet3lem2  25238  iscmet3  25239  bcthlem1  25270  cmsss  25297  cmetcusp1  25299  cmetcusp  25300  cmscsscms  25319  rrxcph  25338  minveclem3b  25374  ovolfioo  25414  ovolficc  25415  ovolctb  25437  ovoliunnul  25454  ovolshftlem1  25456  sca2rab  25459  ovolscalem1  25460  ovolicc2lem1  25464  ovolicc2lem2  25465  ovolicc2lem4  25467  ovolicc2lem5  25468  iundisj  25495  iunmbl2  25504  uniioombllem3  25532  vitalilem2  25556  vitalilem3  25557  mbfss  25593  i1faddlem  25640  i1fmullem  25641  mbfi1fseqlem2  25664  mbfi1fseqlem4  25666  mbfi1fseq  25669  itg2splitlem  25696  itg2split  25697  itg2monolem1  25698  itg2gt0  25708  isibl  25713  iblss2  25753  itgss3  25762  itgsplit  25783  ellimc  25820  limcmo  25829  cnlimc  25835  limciun  25841  limcun  25842  eldv  25845  dvbsss  25849  dvreslem  25856  elcpn  25882  dvaddf  25891  dvmulf  25892  dvcof  25898  rolle  25940  dvlip2  25946  dvivthlem1  25959  lhop1  25965  lhop2  25966  ftc1cn  25996  fta1glem2  26121  plyco0  26144  elply  26147  ply1termlem  26155  eltayl  26312  tayl0  26314  taylplem1  26315  taylplem2  26316  dvtaylp  26323  taylthlem1  26326  taylthlem2  26327  taylthlem2OLD  26328  abelth  26396  cxpcn3  26701  rlimcnp  26915  fsumharmonic  26962  dchrelbas  27187  pntrsumbnd2  27518  ostth2lem2  27585  nolesgn2ores  27623  nogesgn1ores  27625  nosupprefixmo  27651  noinfprefixmo  27652  nosupcbv  27653  nosupdm  27655  nosupfv  27657  nosupres  27658  nosupbnd1lem1  27659  nosupbnd1lem3  27661  nosupbnd1lem5  27663  nosupbnd2lem1  27666  noinfcbv  27668  noinfdm  27670  noinffv  27672  noinfres  27673  noinfbnd1lem1  27674  noinfbnd1lem3  27676  noinfbnd1lem5  27678  noinfbnd2lem1  27681  elmade  27812  elold  27814  ssltleft  27815  ssltright  27816  oldlim  27831  madebday  27844  newbday  27846  sltlpss  27851  cofcutr  27862  cofcutrtime  27865  lrrecval  27874  lrrecval2  27875  addsval  27897  precsexlem9  28131  precsexlem11  28133  sltonold  28171  noseqrdgfn  28197  istrkgb  28277  istrkgcb  28278  istrkge  28279  istrkgl  28280  istrkgld  28281  axtgsegcon  28286  axtg5seg  28287  axtgbtwnid  28288  axtgpasch  28289  axtgupdim2  28293  axtgeucl  28294  tgdim01  28329  iscgrg  28334  isismt  28356  tglnunirn  28370  tglngval  28373  tgellng  28375  legval  28406  legov  28407  legov2  28408  ishlg  28424  mirreu3  28476  mirval  28477  mirfv  28478  mircgr  28479  mirbtwn  28480  ismir  28481  mireq  28487  symquadlem  28511  israg  28519  perpln1  28532  perpln2  28533  isperp  28534  islnopp  28561  outpasch  28577  ishpg  28581  iscgra  28631  dfcgra2  28652  isinag  28660  isleag  28669  iseqlg  28689  f1otrgitv  28692  f1otrg  28693  f1otrge  28694  ttgval  28697  ttgvalOLD  28698  ttgelitv  28711  elee  28723  brbtwn  28728  brcgr  28729  axlowdimlem16  28786  ebtwntg  28811  elntg2  28814  upgrex  28923  edgupgr  28965  upgredg  28968  edglnl  28974  numedglnl  28975  uhgr2edg  29039  umgr2edg1  29042  usgredg2vlem1  29056  usgredg2vlem2  29057  ushgredgedg  29060  ushgredgedgloop  29062  uhgrspansubgrlem  29121  fusgrfisstep  29160  nbgrval  29167  nbgrel  29171  nbupgrel  29176  nbgr2vtx1edg  29181  nbuhgr2vtx1edgblem  29182  nbuhgr2vtx1edgb  29183  nbusgreledg  29184  usgrnbcnvfv  29196  uvtxval  29218  uvtxel  29219  uvtx01vtx  29228  uvtxusgrel  29234  nbcplgr  29265  cplgr3v  29266  cusgrexi  29274  structtocusgr  29277  vtxdgfval  29299  vtxdg0v  29305  vtxdeqd  29309  vtxdun  29313  1loopgrnb0  29334  1loopgrvd0  29336  1hevtxdg0  29337  1hevtxdg1  29338  1egrvtxdg1  29341  umgr2v2evtxel  29354  umgr2v2enb1  29358  umgr2v2evd2  29359  vtxdginducedm1lem4  29374  vtxdginducedm1  29375  finsumvtxdg2sstep  29381  ewlksfval  29433  isewlk  29434  wksfval  29441  iswlk  29442  uspgr2wlkeq  29478  wlkres  29502  usgr2pthlem  29595  clwlkcompim  29612  uspgrn2crct  29637  wwlks  29664  iswwlksn  29667  wwlknvtx  29674  wlkiswwlks2  29704  wwlksm1edg  29710  wwlksnred  29721  wwlksnext  29722  wwlksnredwwlkn  29724  wwlksnredwwlkn0  29725  wwlksnwwlksnon  29744  wspn0  29753  usgr2wspthons3  29793  rusgrnumwwlkb0  29800  clwwlk  29811  clwwlkccatlem  29817  clwlkclwwlklem2a4  29825  clwlkclwwlk  29830  clwwisshclwwslem  29842  clwwlkinwwlk  29868  clwwlkel  29874  clwwlkf  29875  clwwlkext2edg  29884  wwlksext2clwwlk  29885  wwlksubclwwlk  29886  clwwnisshclwwsn  29887  eleclclwwlknlem2  29889  erclwwlknsym  29898  erclwwlkntr  29899  umgrhashecclwwlk  29906  clwwlkvbij  29941  eupth2lem3lem3  30058  eupth2lem3lem4  30059  eupth2lem3lem6  30061  eupth2lemb  30065  eucrct2eupth  30073  fusgreg2wsplem  30161  2clwwlklem  30171  2clwwlk2clwwlklem  30174  2clwwlkel  30177  2clwwlk2clwwlk  30178  extwwlkfabel  30181  clwwlknonclwlknonf1o  30190  dlwwlknondlwlknonf1olem1  30192  numclwwlk2lem1  30204  numclwlk2lem2f  30205  numclwlk2lem2f1o  30207  ex-res  30269  isssp  30552  sspn  30564  islno  30581  isblo  30610  nmlno0  30623  ishmo  30639  dipdir  30670  dipass  30673  ubthlem1  30698  ubthlem2  30699  htthlem  30745  htth  30746  ocel  31109  ocnel  31126  shsel  31142  shsel2  31150  shmodsi  31217  pjhtheu  31222  pjeq  31227  axpjpj  31248  pjoc2  31267  elspani  31371  h1de2ctlem  31383  elspansn  31394  elspansn2  31395  elnlfn  31756  eleigvec  31785  riesz3i  31890  cbviunf  32364  iuneq12daf  32365  iunrdx  32372  iunrnmptss  32374  cbvdisjf  32379  disjorf  32387  disjabrex  32390  disjabrexf  32391  iundisjf  32397  disjrdx  32399  brab2d  32415  elimampt  32441  2ndresdju  32453  abfmpunirn  32456  abfmpeld  32458  abfmpel  32459  fmptcof2  32461  acunirnmpt2  32464  acunirnmpt2f  32465  aciunf1lem  32466  funcnvmpt  32471  suppss3  32524  fpwrelmap  32533  xrofsup  32555  iundisjfi  32582  eliccioo  32672  s3f1  32688  ccatf1  32690  swrdrn3  32694  ismnt  32728  mgcoval  32731  gsummpt2co  32780  gsumpart  32787  gsumhashmul  32788  xrge0tsmsbi  32790  cycpmco2  32872  cyc3co2  32879  inftmrel  32906  isinftm  32907  isslmd  32927  urpropd  32957  isdrng4  32980  erlval  32990  rlocval  32991  rloccring  33002  rloc1r  33004  fracfld  33012  resv1r  33071  ellspds  33098  lbslsp  33110  rhmimaidl  33166  isprmidl  33172  qsidomlem1  33186  qsidomlem2  33187  ismxidl  33193  crngmxidl  33200  drng0mxidl  33207  opprqus0g  33219  qsfld  33227  isrprm  33249  dimpropd  33311  lbslsat  33319  extdg1id  33360  elirng  33369  ply1annidllem  33377  smatrcl  33402  smatcl  33408  ist0cld  33439  txomap  33440  locfinreflem  33446  zarclsiin  33477  zart0  33485  rhmpreimacnlem  33490  metidval  33496  cnre2csqima  33517  ordtrest2NEW  33529  fmcncfil  33537  fsumcvg4  33556  ofcfval  33722  measvuni  33838  meascnbl  33843  faeval  33870  ismbfm  33875  elunirnmbfm  33876  imambfm  33887  elcarsg  33930  itgeq12dv  33951  issibf  33958  eulerpartlems  33985  eulerpartlemgc  33987  eulerpartlemgvv  34001  eulerpartlemgu  34002  eulerpart  34007  rrvmbfm  34067  elorvc  34084  elorrvc  34088  dstfrvunirn  34099  ballotlemfc0  34117  ballotlemfcc  34118  ballotlemsima  34140  ballotlemrv  34144  fzssfzo  34176  signstfvn  34206  signstfvneq0  34209  signstres  34212  repr0  34248  reprinrn  34255  reprdifc  34264  hgt750lemg  34291  hgt750lemb  34293  istrkg2d  34303  axtgupdim2ALTV  34305  afsval  34308  brafs  34309  bnj945  34409  bnj1400  34471  bnj18eq1  34563  bnj916  34569  bnj1014  34597  bnj1015  34598  bnj1110  34618  bnj1417  34677  revpfxsfxrev  34730  cplgredgex  34735  pfxwlk  34738  revwlk  34739  subfacp1lem2b  34796  subfacp1lem4  34798  subfacp1lem5  34799  subfacp1lem6  34800  ptpconn  34848  cvmscbv  34873  iscvm  34874  cvmsi  34880  cvmsval  34881  cvmliftmolem1  34896  cvmlift2lem12  34929  cvmlift2lem13  34930  cvmlift3lem7  34940  snmlval  34946  satfv1  34978  satfvsucsuc  34980  satfrnmapom  34985  satf0op  34992  satf0n0  34993  sat1el2xp  34994  fmlafvel  35000  isfmlasuc  35003  fmlaomn0  35005  gonan0  35007  goaln0  35008  gonar  35010  goalr  35012  satffunlem1lem2  35018  satffunlem2lem2  35021  satfv0fvfmla0  35028  satef  35031  satefvfmla0  35033  sategoelfvb  35034  satfv1fvfmla1  35038  mrsubfval  35123  mrsubvrs  35137  mclsrcl  35176  mclsval  35178  mppsval  35187  mclsppslem  35198  opelco3  35375  wsuclem  35426  funtransport  35632  fvtransport  35633  brcolinear  35660  colineardim1  35662  funray  35741  fvray  35742  funline  35743  fvline  35745  lineelsb2  35749  fwddifval  35763  fwddifnval  35764  rankelg  35769  rankeq1o  35772  elhf2  35776  0hf  35778  neibastop2lem  35849  neibastop3  35851  eltail  35863  bj-projeq  36476  bj-projval  36480  bj-restsn  36566  opelopabbv  36627  brabd0  36631  bj-eldiag  36660  bj-eldiag2  36661  mptsnunlem  36822  dissneqlem  36824  iooelexlt  36846  relowlssretop  36847  rdgellim  36860  exrecfnlem  36863  finxpeq1  36870  finxpreclem6  36880  pibp21  36899  curf  37076  uncf  37077  curunc  37080  unccur  37081  fin2so  37085  lindsadd  37091  lindsdom  37092  lindsenlbs  37093  matunitlindflem1  37094  matunitlindflem2  37095  matunitlindf  37096  ptrest  37097  ptrecube  37098  poimirlem2  37100  poimirlem8  37106  poimirlem17  37115  poimirlem18  37116  poimirlem20  37118  poimirlem21  37119  poimirlem22  37120  poimirlem24  37122  poimirlem26  37124  poimirlem29  37127  heicant  37133  mblfinlem1  37135  mblfinlem2  37136  volsupnfl  37143  itg2addnclem  37149  itg2gt0cn  37153  indexdom  37212  incsequz  37226  istotbnd  37247  istotbnd3  37249  0totbnd  37251  sstotbnd  37253  sstotbnd3  37254  isbnd  37258  prdstotbnd  37272  cntotbnd  37274  isismty  37279  heibor1lem  37287  heiborlem2  37290  heiborlem3  37291  heibor  37299  isass  37324  exidcl  37354  exidreslem  37355  elghomlem2OLD  37364  rngoidmlem  37414  rngo1cl  37417  divrngcl  37435  isdrngo2  37436  isrngohom  37443  isrngoiso  37456  isriscg  37462  iscom2  37473  iscringd  37476  isidl  37492  ispridl  37512  ismaxidl  37518  ac6s6  37650  dmecd  37780  releldmqs  38134  releldmqscoss  38136  erimeq2  38154  eldisjlem19  38286  membpartlem19  38287  prter3  38358  islshp  38455  islsat  38467  lcvfbr  38496  islfl  38536  ellkr  38565  islshpkrN  38596  ldual1dim  38642  isopos  38656  cmtfvalN  38686  cvrfval  38744  isat  38762  islln  38983  islpln  39007  islvol  39050  isline  39216  ispointN  39219  ispsubsp  39222  elpmap  39235  elpmapat  39241  elpadd  39276  paddclN  39319  elpclN  39369  elpcliN  39370  pclfinN  39377  pclcmpatN  39378  ispsubclN  39414  iswatN  39471  islhp  39473  islaut  39560  ispautN  39576  isldil  39587  isltrn  39596  isdilN  39631  istrnN  39634  istendo  40237  dvhb1dimN  40463  erng1lem  40464  erngdvlem4-rN  40476  diaelval  40510  diaeldm  40513  dia1dimid  40540  cdlemm10N  40595  dibopelvalN  40620  dibopelval2  40622  dibelval3  40624  dibelval1st  40626  dibelval2nd  40629  dibeldmN  40635  dibvalrel  40640  dibglbN  40643  dicffval  40651  dicfval  40652  dicopelval  40654  dicelvalN  40655  dicelval3  40657  dicvalrelN  40662  dicelval1sta  40664  diclspsn  40671  dihopelvalbN  40715  dihopelvalcqat  40723  dihopelvalcpre  40725  dihvalrel  40756  dih1  40763  dihmeetlem4preN  40783  dihmeetlem13N  40796  dih1dimatlem  40806  dochnel2  40869  dihjatcclem4  40898  dvh2dim  40922  dvh3dim  40923  dvh4dimN  40924  dochfln0  40954  lpolsetN  40959  islpolN  40960  lcfrvalsnN  41018  lcfrlem21  41040  lcfrlem27  41046  lcfrlem37  41056  lcfr  41062  lcdlss  41096  mapdcv  41137  hdmap1fval  41273  hdmapffval  41303  hdmapfval  41304  hdmapval  41305  hgmapffval  41362  hgmapfval  41363  hdmapellkr  41391  hlhilhillem  41441  fzsplitnd  41457  isprimroot  41568  primrootsunit1  41571  primrootscoprmpow  41574  primrootscoprbij  41577  aks6d1c1p2  41584  aks6d1c1p3  41585  aks6d1c1p4  41586  aks6d1c1p5  41587  aks6d1c1p6  41589  aks6d1c1  41591  evl1gprodd  41592  sticksstones11  41632  sticksstones12a  41633  fzosumm1  41737  frlmfielbas  41743  frlmsnic  41773  psrmnd  41778  isnacs  42127  mrefg2  42130  elmzpcl  42149  mzpcompact2  42175  eldiophb  42180  elpell1qr  42270  elpell14qr  42272  elpell1234qr  42274  pw2f1ocnv  42461  pw2f1o2val2  42464  aomclem4  42484  aomclem6  42486  islssfg2  42498  imasgim  42527  lnr2i  42543  elmnc  42563  rngunsnply  42600  onexomgt  42672  onexlimgt  42674  onexoegt  42675  oaordnr  42728  omnord1  42737  oenord1  42748  cantnfresb  42756  tfsconcatun  42769  tfsconcat0i  42777  ofoaf  42787  naddcnff  42794  naddcnffo  42796  naddcnfcom  42798  naddcnfid1  42799  naddcnfid2  42800  naddcnfass  42801  naddwordnexlem4  42834  fiinfi  43006  sqrtcvallem1  43064  elintima  43086  eliunov2  43112  ov2ssiunov2  43133  brtrclfv2  43160  rfovcnvf1od  43437  rfovcnvfvd  43440  fsovrfovd  43442  fsovfvd  43443  fsovcnvlem  43446  ntrclsfv1  43488  ntrclselnel1  43490  ntrclsneine0lem  43497  ntrneifv1  43512  ntrneifv2  43513  ntrneiel  43514  gneispace2  43565  gneispacess2  43579  extoimad  43597  mnringelbased  43654  dvconstbi  43774  bccbc  43785  eliin2f  44473  rabbida2  44501  disjinfi  44568  unirnmap  44584  elmptima  44636  iuneqfzuzlem  44718  iooiinioc  44943  fsumiunss  44965  fsumsupp0  44968  lptre2pt  45030  icccncfext  45277  cncfiooicclem1  45283  dvnprodlem2  45337  stoweidlem27  45417  stoweidlem29  45419  stoweidlem31  45421  stoweidlem34  45424  stoweidlem48  45438  stoweidlem59  45449  dirkercncflem2  45494  dirkercncflem4  45496  fourierdlem2  45499  fourierdlem3  45500  fourierdlem25  45522  fourierdlem32  45529  fourierdlem33  45530  fourierdlem41  45538  fourierdlem48  45544  fourierdlem49  45545  fourierdlem62  45558  fourierdlem70  45566  fourierdlem80  45576  fourierdlem92  45588  fourierdlem93  45589  fourierdlem101  45597  etransclem37  45661  sge0val  45756  sge0f1o  45772  sge0iunmptlemre  45805  sge0iunmpt  45808  iundjiun  45850  caragenel  45885  ovncvrrp  45954  ovnsubaddlem1  45960  ovnsubadd  45962  hoidmvlelem2  45986  hoidmvlelem3  45987  hoidmvlelem4  45988  hoidmvle  45990  ovncvr2  46001  hspdifhsp  46006  hoiqssbl  46015  hspmbllem2  46017  hspmbl  46019  opnvonmbllem1  46022  isvonmbl  46028  ovnovollem1  46046  issmflem  46117  smflimlem3  46163  smflimlem4  46164  smflim  46167  smfmullem2  46182  smflimmpt  46200  smfsuplem1  46201  smflimsuplem1  46210  smflimsuplem3  46212  smflimsuplem4  46213  smflimsuplem7  46216  smflimsup  46218  tworepnotupword  46274  fcores  46451  fcoresf1  46453  afvelrnb  46545  afvelrnb0  46546  afv2co2  46639  el1fzopredsuc  46707  iccpart  46758  iccpartgtprec  46762  iccpartiltu  46764  iccpartigtl  46765  iccpartltu  46767  iccpartgtl  46768  iccpartgt  46769  iccpartleu  46770  iccpartgel  46771  iccelpart  46775  iccpartiun  46776  icceuelpart  46778  fargshiftfv  46781  fargshiftfo  46784  sprel  46826  prprelb  46858  prprelprb  46859  fpprel  47070  sbgoldbo  47129  wtgoldbnnsum4prm  47144  bgoldbnnsum3prm  47146  bgoldbtbndlem3  47149  bgoldbtbnd  47151  clnbgrval  47164  clnbgrel  47169  clnbupgrel  47175  vopnbgrel  47191  uspgrimprop  47222  upwlksfval  47248  isupwlk  47249  intop  47316  isclintop  47320  assintop  47322  isassintop  47323  assintopcllaw  47325  uzlidlring  47348  elrngchomALTV  47382  rngccatidALTV  47385  rngcsectALTV  47388  rngcisoALTV  47390  rhmsubcALTVlem3  47396  rhmsubcALTVlem4  47397  funcringcsetcALTV2lem7  47409  funcringcsetcALTV2lem9  47411  elringchomALTV  47416  ringccatidALTV  47419  ringcsectALTV  47422  ringcisoALTV  47424  ringcbasbasALTV  47425  funcringcsetclem7ALTV  47432  funcringcsetclem9ALTV  47434  srhmsubcALTV  47438  opeliun2xp  47447  cbvmpox2  47450  ply1sclrmsm  47502  dmatALTbasel  47521  lcoval  47531  lindslinindsimp1  47576  lindslinindsimp2  47582  lmod1  47611  elbigo  47675  elbigo2  47676  elbigolo1  47681  dig2nn0ld  47728  naryfvalel  47754  rrxlines  47857  rrxlinesc  47859  rrxlinec  47860  eenglngeehlnm  47863  elrrx2linest2  47869  rrxsphere  47872  itsclc0  47895  itsclc0b  47896  itsclinecirc0  47897  itsclinecirc0b  47898  itscnhlinecirc02p  47909  f1omo  47964  lubeldm2d  48028  glbeldm2d  48029  catprs  48068  isthinc  48078  isthincd2lem1  48084  thincmoALT  48087  thincmod  48088  isthincd  48094  prsthinc  48111  elsetrecslem  48181