Theorem eqeq1d 2738

Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)

Hypothesis

Ref	Expression
eqeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eqeq1d	⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Proof of Theorem eqeq1d

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		dfcleq 2729	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	biimpi 216	. . 3 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		bibi1 351	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	alimi 1812	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		albi 1819	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)) → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
7	1, 3, 5, 6	4syl 19	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
8		dfcleq 2729	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
9		dfcleq 2729	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
10	7, 8, 9	3bitr4g 314	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   = wceq 1541   ∈ wcel 2113

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-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  eqeq1  2740  eqcomd  2742  eqeq2d  2747  eqeqan12d  2750  neeq1d  2991  rspcedeq1vd  3583  csbconstg  3868  csbhypf  3877  csbiebt  3878  csbiebg  3881  sbceq2g  4371  csbie2df  4395  disjeq0  4408  disjssun  4420  mosneq  4798  preq12b  4806  preq12bg  4809  elpreqprlem  4822  disji2  5082  invdisjrab  5085  disjprg  5094  disjxun  5096  iin0  5307  opthg  5425  opeqsng  5451  propeqop  5455  wefrc  5618  xpcan  6134  xpcan2  6135  dmsnopg  6171  rnmpt0f  6201  reuop  6251  dfpo2  6254  sspred  6268  onfr  6356  unisucg  6397  nsuceq0  6402  iotaeq  6460  iotabi  6461  fneq1  6583  fnun  6606  fnresdisj  6612  fnimadisj  6624  fnimaeq0  6625  foeq1  6742  fveqeq2d  6842  fvun1  6925  fvmptdv2  6959  fndmdifeq0  6989  fneqeql  6991  dffo3  7047  dffo3f  7051  fnnfpeq0  7124  foeqcnvco  7246  f1eqcocnv  7247  isofrlem  7286  eqfunresadj  7306  ovanraleqv  7382  f1opr  7414  eloprabga  7467  ovmpodv2  7516  ov3  7521  ovelimab  7536  caovcang  7559  caovcan  7562  caovmo  7595  caofinvl  7654  caofid1  7657  caofid2  7658  caofidlcan  7660  caonncan  7666  tfisi  7801  mptcnfimad  7930  oteqimp  7952  br1steqg  7955  br2ndeqg  7956  eqop  7975  reldm  7988  mposn  8045  fparlem1  8054  fparlem2  8055  fsplit  8059  frxp  8068  xporderlem  8069  fnwelem  8073  xpord2lem  8084  xpord3lem  8091  poseq  8100  soseq  8101  fnsuppeq0  8134  suppssov1  8139  suppssov2  8140  suppofss1d  8146  suppofss2d  8147  tposfo2  8191  mpocurryd  8211  iinon  8272  onnseq  8276  tz7.49  8376  seqomlem2  8382  oe0m1  8448  om0r  8466  oe1m  8472  oawordeulem  8481  oawordeu  8482  oarec  8489  omord  8495  oneo  8508  omeu  8512  oeeui  8530  nnm0r  8538  nnmord  8560  nnawordex  8565  nnaordex2  8567  nnneo  8583  nneob  8584  omopth  8590  nnasmo  8591  ereq1  8642  eqerlem  8670  qsdisj  8731  erov  8751  eceqoveq  8759  mapsnd  8824  endisj  8992  pw2f1olem  9009  enfixsn  9014  disjenex  9063  domssex2  9065  xpf1o  9067  mapxpen  9071  unxpdomlem2  9157  enp1ilem  9178  fodomfib  9229  fodomfibOLD  9231  fipreima  9258  opthreg  9527  cantnfp1lem3  9589  ssttrcl  9624  ttrcltr  9625  ttrclss  9629  ttrclselem2  9635  frmin  9661  updjud  9846  pm54.43  9913  dfac5  10039  dfacacn  10052  kmlem9  10069  cfeq0  10166  cfss  10175  cfslb  10176  fin23lem22  10237  fin23lem12  10241  fin23lem19  10246  fin23lem30  10252  fin23lem33  10255  fin1a2lem6  10315  axcc2lem  10346  axdc3lem2  10361  axdc3lem3  10362  axdc3lem4  10363  axdc3  10364  axdc4lem  10365  zorn2lem7  10412  ttukeylem3  10421  ttukeylem6  10424  ttukey2g  10426  fodomb  10436  axacndlem5  10522  fpwwe2cbv  10541  fpwwe2lem2  10543  fpwwe2lem3  10544  fpwwe2lem11  10552  fpwwe2lem12  10553  fpwwe  10557  pwfseqlem2  10570  pwxpndom2  10576  addnidpi  10812  ltexpi  10813  recmulnq  10875  ltexnq  10886  halfnq  10887  archnq  10891  ltexpri  10954  recexpr  10962  addsrpr  10986  mulsrpr  10987  00sr  11010  negexsr  11013  recexsrlem  11014  recexsr  11018  axrnegex  11073  axrrecex  11074  00id  11308  mul02  11311  addrid  11313  cnegex  11314  cnegex2  11315  subval  11371  subadd  11383  subadd2  11384  subsub23  11385  addsubeq4  11395  subcan2  11406  negcon1  11433  subcan  11436  addrsub  11554  ltordlem  11662  ltord1  11663  recex  11769  mul0or  11777  muleqadd  11781  receu  11782  mulcan1g  11790  divval  11798  divmul  11799  rec11  11839  ldiv  11975  rdiv  11976  zdiv  12562  uzin  12787  xaddval  13138  xmulval  13140  xnn0xadd0  13162  xnegdi  13163  ioo0  13286  ico0  13307  ioc0  13308  icc0  13309  1fv  13563  fzon  13596  fvinim0ffz  13705  flbi  13736  mod0  13796  modmuladdnn0  13838  modirr  13865  addmodlteq  13869  uzrdgfni  13881  axdc4uzlem  13906  fsuppmapnn0fiubex  13915  mptnn0fsupp  13920  seqid  13970  seqz  13973  expval  13986  expeq0  14015  sqeqor  14139  nn0opth2  14195  hashdom  14302  elprchashprn2  14319  hashbc  14376  hashf1lem1  14378  hash2pwpr  14399  ccat0  14499  wrdl1s1  14538  ccatws1lenp1b  14545  pfxsuff1eqwrdeq  14622  swrdccatin2  14652  pfxccatin12lem2  14654  2cshwcshw  14748  scshwfzeqfzo  14749  cshimadifsn  14752  cshimadifsn0  14753  s2f1o  14839  wrdlen2i  14865  2swrd2eqwrdeq  14876  wwlktovf  14879  wwlktovf1  14880  wwlktovfo  14881  wrd2f1tovbij  14883  relexp0g  14945  relexpsucnnr  14948  dfrtrcl2  14985  mulre  15044  rennim  15162  cnpart  15163  01sqrex  15172  resqrex  15173  sqrmo  15174  resqrtcl  15176  resqrtthlem  15177  sqrtgt0  15181  sqrtneg  15190  sqrtsq2  15191  absmod0  15226  sqreulem  15283  sqreu  15284  sqrtthlem  15286  eqsqrtd  15291  reusq0  15388  fsum00  15721  telfsumo  15725  prodss  15870  fprodle  15919  tanaddlem  16091  absefib  16123  efieq1re  16124  divides  16181  dvdsval2  16182  nndivides  16189  dvds0lem  16193  dvds1lem  16194  dvds2lem  16195  negdvdsb  16199  muldvds1  16207  muldvds2  16208  dvdscmulr  16211  dvdsmulcr  16212  difmod0  16214  dvdstr  16221  dvdsabseq  16240  divconjdvds  16242  odd2np1lem  16267  odd2np1  16268  even2n  16269  oddm1even  16270  2tp1odd  16279  opeo  16292  omeo  16293  m1exp1  16303  divalglem4  16323  divalglem8  16327  divalgb  16331  bitsuz  16401  smupvallem  16410  gcdaddmlem  16451  gcdabs1  16456  bezoutlem3  16468  rplpwr  16485  rprpwr  16486  alginv  16502  algcvga  16506  algfx  16507  eucalgval2  16508  coprmdvds  16580  qredeq  16584  qredeu  16585  coprmprod  16588  coprmproddvdslem  16589  divgcdcoprm0  16592  divgcdcoprmex  16593  cncongr1  16594  rpexp  16649  rpexp12i  16651  cncongrprm  16656  qnumdenbi  16671  phival  16694  phicl2  16695  dfphi2  16701  phiprmpw  16703  phimullem  16706  eulerthlem1  16708  eulerthlem2  16709  eulerth  16710  fermltl  16711  hashgcdlem  16715  phisum  16718  odzval  16719  odzdvds  16723  reumodprminv  16732  modprm0  16733  nnnn0modprm0  16734  modprmn0modprm0  16735  coprimeprodsq  16736  coprimeprodsq2  16737  pythagtriplem2  16745  pythagtrip  16762  pcval  16772  pceulem  16773  pcqmul  16781  pcqcl  16784  pcabs  16803  pcgcd1  16805  pc2dvds  16807  pcaddlem  16816  pcadd  16817  pcmpt  16820  prmpwdvds  16832  pockthi  16835  unbenlem  16836  4sqlem12  16884  ramz  16953  ramcl  16957  cshwrepswhash1  17030  imasval  17432  fvprif  17482  iscat  17595  iscatd  17596  catidex  17597  catideu  17598  cidfval  17599  cidval  17600  catidd  17603  catlid  17606  catrid  17607  catpropd  17632  cidpropd  17633  issect  17677  dfiso2  17696  invcoisoid  17716  isocoinvid  17717  setcepi  18012  latleeqj2  18375  latleeqm2  18391  oduclatb  18430  mgmidmo  18585  grpidval  18586  grpidpropd  18587  ismgmid  18590  ismgmid2  18593  mgmidsssn0  18597  grpinvalem  18598  grprida  18600  gsumvalx  18601  gsumpropd  18603  gsumpropd2lem  18604  gsumress  18607  gsumval2  18611  ismnddef  18661  sgrpidmnd  18664  ismndd  18681  mndpropd  18684  mndinvmod  18689  mnd1  18704  ismhm  18710  gsumvallem2  18759  frmdgsum  18787  frmdup3  18792  efmndmnd  18814  smndex1mnd  18835  sgrp2rid2  18851  sgrp2rid2ex  18852  pwmnd  18862  grpinvex  18873  isgrpd2  18886  isgrpd  18888  dfgrp2  18892  grpinveu  18904  grpinvval  18910  grplinv  18919  isgrpinv  18923  grplrinv  18926  grpidinv2  18927  grpidinv  18928  grplmulf1o  18943  grpraddf1o  18944  grpsubeq0  18956  grpsubadd  18958  dfgrp3lem  18968  dfgrp3  18969  grp1  18977  imasgrp2  18985  qusgrp2  18988  mhmmnd  18994  ghmgrp  18996  mulgval  19001  mulgaddcom  19028  eqg0el  19112  cycsubmel  19129  ghmeqker  19172  ghmf1  19175  conjnmzb  19182  ghmqusker  19216  isga  19220  subgga  19229  gaorb  19236  gaorber  19237  gastacl  19238  gastacos  19239  orbsta  19242  symgfix2  19345  gsmsymgrfixlem1  19356  gsmsymgrfix  19357  gsmsymgreq  19361  symgfixelq  19362  f1omvdconj  19375  pmtrdifwrdel2  19415  psgnunilem1  19422  psgnunilem2  19424  psgnunilem3  19425  psgnunilem4  19426  odval  19463  odid  19467  odlem2  19468  oddvdsnn0  19473  odnncl  19474  oddvds  19476  odcong  19478  odeq  19479  odmulgid  19483  odmulgeq  19486  gexval  19507  gexid  19510  gexlem2  19511  gexdvdsi  19512  gexdvds  19513  subgpgp  19526  sylow1lem1  19527  sylow1lem4  19530  sylow2alem1  19546  sylow2alem2  19547  sylow2blem2  19550  sylow3lem6  19561  lsmdisj3a  19618  lsmdisj3b  19619  pj1val  19624  pj1eq  19629  efgredlemd  19673  efgredlem  19676  efgred  19677  efgrelexlema  19678  frgpup3  19707  ablsubadd  19738  ablsubsub23  19753  iscyggen  19809  cyggenod  19813  gsumval3lem2  19835  gsumval3  19836  gsummptnn0fz  19915  dmdprd  19929  dprddisj  19940  dprdfeq0  19953  dprdf11  19954  dmdprdpr  19980  dpjeq  19990  ablfacrp  19997  pgpfac1lem2  20006  pgpfac1lem3  20008  pgpfac1lem5  20010  pgpfac1  20011  pgpfaclem1  20012  pgpfaclem2  20013  pgpfaclem3  20014  ablfaclem2  20017  ablfaclem3  20018  ablfac2  20020  rngmneg1  20102  rngmneg2  20103  ringurd  20120  srgrz  20142  srglz  20143  srgisid  20144  srg1zr  20150  ringid  20209  qusring2  20270  opprring  20283  dvdsrval  20297  dvdsrmul  20300  dvdsr01  20307  dvdsr02  20308  crngunit  20314  ringunitnzdiv  20334  dvreq1  20347  dvdsrpropd  20352  irredn0  20359  irredrmul  20363  irredmul  20365  rngisomring  20403  rhmdvdsr  20441  lringuplu  20477  subrg1  20515  subrgdvds  20519  isrrg  20631  rrgeq0i  20632  rrgeq0  20633  domneq0  20641  isdomn4  20649  domnlcanb  20653  domnrcanb  20655  drngid2  20685  drngmul0orOLD  20694  isdrngd  20698  isdrngdOLD  20700  fidomndrnglem  20705  isabv  20744  issrngd  20788  islmod  20815  islmodd  20817  lmodprop2d  20875  mptscmfsupp0  20878  lss1d  20914  lspextmo  21008  lvecvs0or  21063  lvecvscan  21066  lvecvscan2  21067  lbsacsbs  21111  rngqiprngimf1lem  21249  rng2idl1cntr  21260  prmirredlem  21427  pzriprnglem7  21442  pzriprnglem13  21448  chrdvds  21481  chrnzr  21485  domnchr  21487  znval  21490  zncyg  21503  znfld  21515  znunit  21518  znrrg  21520  frgpcyg  21528  psgndiflemB  21555  psgndiflemA  21556  ipeq0  21593  ip2eq  21608  elocv  21623  ocvi  21624  obsne0  21680  dsmmacl  21696  dsmmlss  21699  frlmphl  21736  frlmup4  21756  islindf4  21793  islindf5  21794  mplsubrglem  21959  mplmon2  22016  evlslem1  22037  evlseu  22038  evlsval  22041  evlsval2  22042  evlsval3  22044  ismhp3  22085  mhpsclcl  22090  mhpvarcl  22091  mhpmulcl  22092  psdmul  22109  psdmvr  22112  cply1coe0bi  22246  gsummoncoe1  22252  evl1vsd  22288  dmatel  22437  dmatelnd  22440  dmatmulcl  22444  scmateALT  22456  mdetdiaglem  22542  mdetunilem1  22556  mdetunilem3  22558  mdetunilem4  22559  mdetunilem9  22564  symgmatr01lem  22597  symgmatr01  22598  gsummatr01lem1  22599  gsummatr01lem4  22602  gsummatr01  22603  smadiadetlem3  22612  cramerlem3  22633  pmatcoe1fsupp  22645  cpmatel  22655  1elcpmat  22659  cpmatmcllem  22662  cpmatmcl  22663  d1mat2pmat  22683  m2cpminvid2lem  22698  m2cpminvid2  22699  decpmatmulsumfsupp  22717  pmatcollpw2lem  22721  pmatcollpwscmatlem1  22733  mp2pm2mplem4  22753  pm2mpmhmlem1  22762  chpscmat  22786  cpmidpmatlem3  22816  cayleyhamilton0  22833  cayleyhamiltonALT  22835  cayleyhamilton1  22836  0ntr  23015  ntreq0  23021  cldlp  23094  pnrmopn  23287  hausnei2  23297  cnhaus  23298  nrmsep  23301  isnrm2  23302  regsep2  23320  dishaus  23326  ordthauslem  23327  iscmp  23332  cmpsublem  23343  cmpsub  23344  tgcmp  23345  sscmp  23349  hauscmplem  23350  cmpfi  23352  bwth  23354  connsuba  23364  nconnsubb  23367  isref  23453  islocfin  23461  elpt  23516  elptr  23517  pthaus  23582  txcmp  23587  hausdiag  23589  txhaus  23591  txkgen  23596  xkohaus  23597  xkococnlem  23603  regr1lem  23683  fbasrn  23828  fmfnfmlem3  23900  flimtopon  23914  fclstopon  23956  alexsubb  23990  symgtgp  24050  qustgpopn  24064  qustgphaus  24067  ustuqtop  24190  isusp  24205  ispsmet  24248  psmet0  24252  ismet  24267  isxmet  24268  xmeteq0  24282  metn0  24304  xmetres2  24305  imasf1oxmet  24319  xblss2ps  24345  xblss2  24346  xmseq0  24408  comet  24457  stdbdxmet  24459  methaus  24464  dscmet  24516  nrmmetd  24518  nmeq0  24562  tngngp  24598  tngngp3  24600  nlmmul0or  24627  cnmet  24715  xrsxmet  24754  metnrmlem3  24806  icopnfcnv  24896  iccpnfcnv  24898  ishtpy  24927  isphtpy  24936  phtpyi  24939  om1elbas  24988  elpi1i  25002  pi1grplem  25005  isclmp  25053  cphsqrtcl2  25142  tcphcph  25193  bcth3  25287  rrxcph  25348  rrxmet  25364  ivth2  25412  iundisj2  25506  dyaddisj  25553  volivth  25564  mbfinf  25622  i1f1lem  25646  i1fmullem  25651  i1fmulclem  25659  i1fres  25662  itg1climres  25671  mbfi1fseqlem4  25675  dvnres  25889  dvcobr  25905  dvcobrOLD  25906  rolle  25950  cmvth  25951  cmvthOLD  25952  deg1leb  26056  ismon1p  26104  q1peqb  26117  dvdsr1p  26125  ply1remlem  26126  fta1glem2  26130  idomrootle  26134  elply2  26157  ne0p  26168  coeeu  26186  coelem  26187  coeeq  26188  dgrle  26204  coeaddlem  26210  plymul0or  26244  ofmulrt  26245  plydivlem3  26259  plydivlem4  26260  plydivex  26261  plydiveu  26262  plydivalg  26263  quotlem  26264  plyremlem  26268  quotcan  26273  plyexmo  26277  elqaalem3  26285  qaa  26287  iaa  26289  aareccl  26290  aacjcl  26291  aannenlem2  26293  reeff1o  26413  sineq0  26489  coseq1  26490  efeq1  26493  recosf1o  26500  logeftb  26548  cosarg0d  26574  logtayl  26625  cxpval  26629  cxpeq0  26643  root1eq1  26721  cxpeq  26723  logbgcd1irr  26760  angrtmuld  26774  affineequiv  26789  affineequiv3  26791  angpieqvdlem2  26795  quad2  26805  dcubic1lem  26809  dcubic2  26810  dcubic  26812  mcubic  26813  cubic2  26814  dquartlem1  26817  dquart  26819  quart  26827  atandm2  26843  atandm4  26845  atantan  26889  wilthlem2  27035  wilthlem3  27036  muval2  27100  isnsqf  27101  mumullem2  27146  sqff1o  27148  muinv  27159  mpodvdsmulf1o  27160  dvdsmulf1o  27162  dchrelbas2  27204  dchrmullid  27219  dchrfi  27222  lgsval  27268  lgsdir  27299  lgsne0  27302  lgsprme0  27306  lgsdirnn0  27311  lgsqrlem1  27313  lgsqr  27318  gausslemma2dlem0c  27325  gausslemma2dlem0i  27331  gausslemma2dlem7  27340  gausslemma2d  27341  lgseisenlem2  27343  lgsquadlem1  27347  lgsquadlem2  27348  lgsquad2lem2  27352  lgsquad3  27354  m1lgs  27355  2lgs  27374  2sqlem7  27391  2sqlem8  27393  2sqlem9  27394  2sqlem11  27396  2sq  27397  2sq2  27400  2sqmo  27404  addsq2reu  27407  addsqn2reu  27408  addsqrexnreu  27409  addsqnreup  27410  addsq2nreurex  27411  2sqreulem1  27413  2sqreultlem  27414  2sqreunnlem1  27416  2sqreunnltlem  27417  2sqreulem4  27421  2sqreuop  27429  2sqreuopnn  27430  2sqreuoplt  27431  2sqreuopltb  27432  2sqreuopnnlt  27433  2sqreuopnnltb  27434  2sqreuopb  27435  dchrisumlem1  27456  dchrvmaeq0  27471  dchrisum0re  27480  ostth3  27605  ltsval  27615  nosepssdm  27654  nosupprefixmo  27668  noinfprefixmo  27669  nosupcbv  27670  nosupdm  27672  nosupfv  27674  nosupres  27675  nosupbnd1lem1  27676  nosupbnd1lem3  27678  nosupbnd1lem5  27680  noinfcbv  27685  noinfdm  27687  noinffv  27689  noinfres  27690  noinfbnd1lem3  27693  noinfbnd1lem5  27695  eqcuts  27781  cutbdaylt  27794  made0  27859  madecut  27879  negsid  28037  negsex  28039  subadds  28066  divsmo  28180  muls0ord  28181  divsval  28185  norecdiv  28186  recsne0  28188  divmulsw  28189  divs1  28200  precsexlem8  28210  precsexlem9  28211  precsexlem11  28213  precsex  28214  recsex  28215  abssor  28242  elons  28249  noseqrdgfn  28302  bdayn0sf1o  28366  eucliddivs  28372  zsoring  28405  n0seo  28417  zseo  28418  nohalf  28420  expsne0  28432  pw2recs  28434  halfcut  28454  z12negscl  28474  z12zsodd  28478  z12sge0  28479  renegscl  28494  istrkg3ld  28533  axtgcgrid  28535  axtgsegcon  28536  axtg5seg  28537  axtgupdim2  28543  tgjustc1  28547  tgjustc2  28548  iscgrg  28584  isismt  28606  legov  28657  legov2  28658  hlcgreu  28690  mirreu3  28726  mircgr  28729  mirbtwn  28730  ismir  28731  mireq  28737  ismidb  28850  lmiopp  28874  dfcgra2  28902  inaghl  28917  f1otrg  28943  ttgval  28947  ttgelitv  28955  brbtwn  28972  brcgr  28973  colinearalglem2  28980  colinearalg  28983  axsegconlem1  28990  axsegcon  29000  ax5seglem4  29005  ax5seglem5  29006  axpaschlem  29013  axpasch  29014  axlowdimlem16  29030  axeuclidlem  29035  axeuclid  29036  axcontlem2  29038  axcontlem4  29040  axcontlem5  29041  edglnl  29216  usgredg2ALT  29266  usgredgprvALT  29268  usgrnloopvALT  29274  ushgredgedgloop  29304  edg0usgr  29326  nb3grpr  29455  cplgr1v  29503  cusgrsize  29528  vtxdgfval  29541  vtxdeqd  29551  vtxdun  29555  vtxd0nedgb  29562  vtxdusgr0edgnelALT  29570  1loopgrvd2  29577  usgruvtxvdb  29603  usgrvd0nedg  29607  vtxdginducedm1  29617  rusgrpropedg  29658  wksfval  29683  wlklenvclwlk  29727  iswlkon  29729  ispth  29794  dfpth2  29802  upgrwlkdvdelem  29809  crctcshwlkn0lem6  29888  wwlknon  29930  wwlksm1edg  29954  wwlksnextbi  29967  wwlksnextfun  29971  wwlksnextinj  29972  wwlksnextsurj  29973  wwlksnextbij  29975  wlksnwwlknvbij  29981  wwlksnextproplem3  29984  wwlksnextprop  29985  wspn0  29997  umgr2adedgwlkonALT  30020  umgr2adedgspth  30021  umgr2wlkon  30023  rusgrnumwwlkslem  30045  rusgrnumwwlkb0  30047  rusgrnumwwlks  30050  clwlkclwwlklem2a4  30072  clwlknf1oclwwlknlem2  30157  clwlknf1oclwwlkn  30159  isclwwlknon  30166  clwwlknon1loop  30173  s2elclwwlknon2  30179  clwwlknonwwlknonb  30181  clwwlkvbij  30188  uhgr3cyclex  30257  fusgreg2wsplem  30408  fusgr2wsp2nb  30409  fusgreghash2wsp  30413  frrusgrord0  30415  2clwwlkel  30424  extwwlkfab  30427  extwwlkfabel  30428  clwwlknonclwlknonf1o  30437  dlwwlknondlwlknonf1o  30440  wlkl0  30442  numclwwlk2lem1  30451  numclwlk2lem2f  30452  numclwlk2lem2f1o  30454  numclwwlk5  30463  ex-opab  30507  isgrpo  30572  isgrpoi  30573  grpoidinvlem3  30581  grpoideu  30584  gidval  30587  grpoidinv2  30590  grpoinveu  30594  grpoinvval  30598  grpoinv  30600  vciOLD  30636  isvclem  30652  cnidOLD  30657  isnvlem  30685  nvmul0or  30725  imsmetlem  30765  diporthcom  30791  ipz  30794  nmlno0  30870  ajfval  30884  hmoval  30885  isphg  30892  isph  30897  ip2eqi  30931  ajval  30936  hvmul0or  31100  hvsubeq0  31143  hvaddeq0  31144  hvaddcan  31145  hvmulcan  31147  hvmulcan2  31148  hvsubadd  31152  his6  31174  hial0  31177  hial02  31178  hi2eq  31180  orthcom  31183  normlem7tALT  31194  normsub0  31211  normpyth  31220  hilid  31236  hhssnv  31339  ocel  31356  ocsh  31358  ocorth  31366  ocin  31371  occllem  31378  choc0  31401  pjpreeq  31473  omlsi  31479  pjoc1  31509  pjoml  31511  pjoc2  31514  chm0  31566  chocin  31570  chlejb1  31587  chlejb2  31588  chjo  31590  h1deoi  31624  h1de2i  31628  pjoml6i  31664  pjoml2  31686  pjoml3  31687  pjch  31769  hodsi  31850  hodid  31867  eigorth  31913  elunop  31947  adjeu  31964  adjval  31965  eigvecval  31971  unopf1o  31991  adj1  32008  adjeq  32010  hmdmadj  32015  lnopeq0i  32082  lnopeqi  32083  lnopeq  32084  lnfn0  32122  riesz4i  32138  riesz4  32139  riesz1  32140  cnlnadjlem3  32144  cnlnadjlem5  32146  cnlnadjeu  32153  cnlnssadj  32155  nmopadjlei  32163  opsqrlem1  32215  hmopidmpji  32227  pjimai  32251  isst  32288  ishst  32289  hstel2  32294  stadd3i  32323  stri  32332  largei  32342  golem2  32347  superpos  32429  sumdmdii  32490  mddmdin0i  32506  opreu2reuALT  32551  difeq  32593  elim2if  32619  disji2f  32652  disjif2  32656  disjxpin  32663  iundisj2f  32665  disjunsn  32669  fmptco1f1o  32711  ofpreima  32743  fnpreimac  32749  ressupprn  32769  curry2ima  32788  preiman0  32789  receqid  32824  xrofsup  32847  iundisj2fi  32877  f1ocnt  32880  fzo0opth  32883  elq2  32892  fprodex01  32906  sgn0bi  32921  ind1a  32938  prodindf  32944  xdivval  33000  xrecex  33001  xreceu  33003  xdivmul  33006  rexdiv  33007  wrdt2ind  33035  mndlrinvb  33107  mndlactfo  33109  mndractfo  33111  mndlactf1o  33112  mndractf1o  33113  gsummpt2d  33132  gsumwun  33158  fzo0pmtrlast  33174  cyc3genpm  33234  cycpmconjslem2  33237  fxpval  33247  fxpgaeq  33251  cntrval2  33253  isslmd  33284  slmdlema  33285  urpropd  33313  elrgspnlem4  33327  elrgspnsubrunlem2  33330  erlcl1  33342  erlcl2  33343  erldi  33344  erlbrd  33345  erler  33347  rloccring  33352  domnprodeq0  33358  domnlcanOLD  33362  isdrng4  33377  fracerl  33388  fracfld  33390  resv1r  33420  islinds5  33448  linds2eq  33462  dvdsruassoi  33465  dvdsruasso  33466  dvdsruasso2  33467  quslsm  33486  rhmimaidl  33513  qsidomlem2  33534  ssdifidllem  33537  ssdifidl  33538  ssdifidlprm  33539  opprqus0g  33571  qsdrngilem  33575  unitmulrprm  33609  1arithidom  33618  1arithufdlem3  33627  1arithufdlem4  33628  ply1dg1rt  33661  r1pid2OLD  33690  extvfvv  33699  extvfvcl  33701  evlextv  33707  esplysply  33729  esplyind  33731  lbsdiflsp0  33783  fedgmullem1  33786  fedgmullem2  33787  irngss  33844  irngnzply1lem  33847  extdgfialglem2  33850  ply1annidllem  33858  ply1annnr  33860  minplymindeg  33865  minplyann  33866  minplyirredlem  33867  minplyirred  33868  irngnminplynz  33869  minplyelirng  33872  irredminply  33873  algextdeglem6  33879  algextdeglem7  33880  rtelextdg2lem  33883  fldext2chn  33885  constrsuc  33895  constrsslem  33898  constrconj  33902  constrextdg2lem  33905  constrextdg2  33906  constrlccllem  33910  constrcccllem  33911  constrcbvlem  33912  constrext2chn  33916  constrcon  33931  1smat1  33961  iscref  34001  metidval  34047  metidv  34049  metider  34051  pstmxmet  34054  xrmulc1cn  34087  esumfsup  34227  esumpcvgval  34235  esumcvg  34243  inelsros  34335  diffiunisros  34336  ismeas  34356  isrnmeas  34357  brae  34398  braew  34399  dya2iocuni  34440  elcarsg  34462  eulerpartleme  34520  eulerpartlemv  34521  eulerpartlemb  34525  eulerpartgbij  34529  eulerpartlemr  34531  eulerpartlemgvv  34533  eulerpartlemgh  34535  eulerpartlemn  34538  elprob  34566  ballotlemi  34658  ballotlemi1  34660  ballotlemii  34661  ballotlemsima  34673  ballotlemfrcn0  34687  signsw0g  34713  signswmnd  34714  signstfvc  34731  prodfzo03  34760  reprval  34767  reprsum  34770  reprsuc  34772  reprpmtf1o  34783  axtgupdim2ALTV  34825  brafs  34829  bnj125  35028  bnj154  35034  bnj526  35044  bnj609  35073  bnj893  35084  bnj1321  35183  bnj1491  35213  nummin  35249  fineqvnttrclselem2  35278  fineqvnttrclselem3  35279  fineqvnttrclse  35280  noinfepfnregs  35288  subgrwlk  35326  loop1cycl  35331  subfacp1lem3  35376  subfacp1lem5  35378  subfacp1lem6  35379  cnpconn  35424  txpconn  35426  ptpconn  35427  indispconn  35428  connpconn  35429  cvxpconn  35436  cvmscbv  35452  cvmsi  35459  cvmsval  35460  cvmsdisj  35464  cvmsss2  35468  cvmliftmo  35478  cvmliftlem14  35491  cvmliftiota  35495  cvmlift2lem12  35508  cvmlift2lem13  35509  cvmlift2  35510  cvmliftphtlem  35511  cvmlift3lem2  35514  cvmlift3lem4  35516  cvmlift3lem6  35518  cvmlift3lem7  35519  cvmlift3lem9  35521  cvmlift3  35522  snmlval  35525  satffunlem  35595  prv1n  35625  mrsub0  35710  mrsubcn  35713  ismfs  35743  sinccvglem  35866  br6  35951  brbigcup  36090  imageval  36122  funpartlem  36136  dfrdg4  36145  altopthsn  36155  brsegle  36302  rankeq1o  36365  cbviotadavw  36463  subtr  36508  opnbnd  36519  cldbnd  36520  isfne  36533  topfneec  36549  neibastop3  36556  cnndvlem2  36738  bj-imdirval2  37388  bj-imdirid  37391  bj-imdirco  37395  bj-inftyexpiinj  37414  bj-isrvecd  37503  bj-isrvec2  37505  bj-bary1lem1  37516  bj-bary1  37517  finxp00  37607  nlpfvineqsn  37614  pibp19  37619  pibt2  37622  unccur  37804  matunitlindflem2  37818  ptrecube  37821  poimirlem4  37825  poimirlem19  37840  poimirlem23  37844  poimirlem25  37846  poimirlem27  37848  poimirlem28  37849  poimirlem31  37852  poimirlem32  37853  broucube  37855  mblfinlem2  37859  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  mbfresfi  37867  itg2addnclem  37872  itg2addnclem3  37874  itg2addnc  37875  ftc2nc  37903  cover2  37916  sdclem2  37943  fdc  37946  metf1o  37956  istotbnd3  37972  0totbnd  37974  sstotbnd2  37975  equivtotbnd  37979  totbndbnd  37990  prdstotbnd  37995  heibor1  38011  rrnmet  38030  isexid  38048  ismgmOLD  38051  opidonOLD  38053  exidu1  38057  cmpidelt  38060  exidreslem  38078  exidres  38079  exidresid  38080  grpoeqdivid  38082  elghomlem1OLD  38086  grpokerinj  38094  isrngo  38098  isrngod  38099  rngoideu  38104  isgrpda  38156  isdrngo2  38159  isdrngo3  38160  isrngohom  38166  divrngidl  38229  dmnnzd  38276  dmncan1  38277  disjeccnvep  38483  disjressuc2  38596  mopre  38645  qsdisjALTV  38872  dmqseqeq1  38901  unidmqseq  38914  disjdmqseq  39064  eldisjlem19  39069  riotasvd  39216  toycom  39233  islshpsm  39240  lshpnel2N  39245  lsatfixedN  39269  islshpat  39277  lcvexchlem4  39297  l1cvpat  39314  lkr0f  39354  lkrsc  39357  lshpkrlem1  39370  lkreqN  39430  isopos  39440  oposlem  39442  opcon2b  39457  cmtbr3N  39514  cvlcvrp  39600  hlrelat5N  39661  cvrval5  39675  cvrat4  39703  3atlem5  39747  2at0mat0  39785  psubclsetN  40196  4atex2  40337  isldil  40370  ltrnu  40381  ltrnid  40395  isdilN  40414  trlnid  40439  cdleme21k  40598  cdleme29b  40635  cdlemefrs29pre00  40655  cdlemefrs29bpre0  40656  cdlemefrs29cpre1  40658  cdleme32fva  40697  cdleme42b  40738  cdleme50ex  40819  cdleme  40820  cdlemg1a  40830  ltrniotaval  40841  cdlemeiota  40845  tendoid0  41085  cdlemksv2  41107  cdlemkuv2  41127  cdlemk36  41173  cdlemk42  41201  cdlemk  41234  tendoex  41235  cdleml3N  41238  cdleml5N  41240  tendospcanN  41283  cdlemm10N  41378  dihffval  41490  dihfval  41491  dihlsscpre  41494  islpolN  41743  mapdhval  41984  mapdheq  41988  hdmap1fval  42056  hdmap1val  42058  hdmap1eq  42061  hdmap1cbv  42062  hdmapval2lem  42091  hdmap11  42108  hdmap14lem2a  42127  hdmap14lem6  42133  hgmapval  42147  hlhillcs  42218  hlhilphllem  42219  aks4d1  42343  isprimroot  42347  mndmolinv  42349  linvh  42350  primrootsunit1  42351  primrootsunit  42352  primrootscoprmpow  42353  primrootscoprbij  42356  primrootlekpowne0  42359  primrootspoweq0  42360  ringexp0nn  42388  aks6d1c5lem1  42390  sticksstones8  42407  sticksstones9  42408  sticksstones10  42409  sticksstones11  42410  sticksstones12a  42411  sticksstones12  42412  sticksstones16  42416  sticksstones17  42417  sticksstones18  42418  sticksstones19  42419  aks6d1c6lem4  42427  aks6d1c6isolem3  42430  rhmqusspan  42439  grpods  42448  unitscyglem1  42449  unitscyglem2  42450  unitscyglem3  42451  unitscyglem5  42453  expeq1d  42579  zdivgd  42592  ef11d  42594  resubval  42622  renegadd  42627  resubeu  42632  resubadd  42634  sn-remul0ord  42663  sn-negex12  42672  addinvcom  42687  redivvald  42697  rediveud  42698  redivmuld  42700  sn-mul02  42707  mulgt0con1d  42725  mulgt0con2d  42726  fimgmcyclem  42788  fidomncyc  42790  fsuppind  42833  mhphflem  42839  prjspnfv01  42867  prjspner01  42868  prjspner1  42869  prjcrvval  42875  dffltz  42877  flt4lem7  42902  nna4b4nsq  42903  negexpidd  42924  mzpcompact2lem  42993  eldioph  43000  eldioph2lem1  43002  eldioph2lem2  43003  eldioph2  43004  eldioph2b  43005  eldioph3  43008  diophin  43014  diophun  43015  eq0rabdioph  43018  dvdsrabdioph  43052  eldioph4i  43054  diophren  43055  rabren3dioph  43057  fphpd  43058  pellexlem5  43075  pellexlem6  43076  pellex  43077  pell1qrval  43088  pell14qrval  43090  pell1234qrval  43092  pell1234qrreccl  43096  pell1234qrmulcl  43097  pell1234qrdich  43103  pell14qrdich  43111  pell1qr1  43113  pellqrexplicit  43119  rmxycomplete  43159  jm2.27  43250  rmydioph  43256  rmxdiophlem  43257  rmxdioph  43258  pw2f1ocnv  43279  pwssplit4  43331  elmnc  43378  dgraalem  43387  dgraaub  43390  dgraa0p  43391  mpaaeu  43392  mpaaval  43393  mpaalem  43394  aaitgo  43404  rngunsnply  43411  proot1ex  43438  cantnfresb  43566  tfsconcatfv  43583  tfsconcatb0  43586  tfsconcat0i  43587  tfsconcat0b  43588  tfsconcat00  43589  tfsconcatrev  43590  naddwordnexlem4  43643  sqrtcval  43882  relexpnul  43919  relexpxpnnidm  43944  relexpiidm  43945  trclfvdecomr  43969  rfovcnvf1od  44245  ntrkbimka  44279  ntrk0kbimka  44280  clsk3nimkb  44281  clsk1independent  44287  ntrclsfveq1  44301  ntrclsfveq2  44302  ntrclskb  44310  k0004val  44391  k0004val0  44395  mnringmulrcld  44469  expgrowth  44576  bcc0  44581  relpfrlem  45194  permac8prim  45255  disjinfi  45436  fsumf1of  45820  limsupmnflem  45964  liminfpnfuz  46060  climxlim2lem  46089  coseq0  46108  icccncfext  46131  dvnmptconst  46185  dvnprodlem1  46190  dvnprodlem2  46191  dvnprodlem3  46192  dvnprod  46193  stoweidlem15  46259  stoweidlem31  46275  stoweidlem35  46279  stoweidlem36  46280  stoweidlem37  46281  stoweidlem43  46287  stoweidlem44  46288  stoweidlem46  46290  stoweidlem55  46299  stoweidlem59  46303  dirkerval2  46338  dirkertrigeqlem1  46342  dirkeritg  46346  dirkercncf  46351  fourierdlem2  46353  fourierdlem3  46354  fourierdlem42  46393  fourierdlem48  46398  fourierdlem49  46399  fourierdlem71  46421  fourierdlem112  46462  fourierdlem113  46463  elaa2lem  46477  etransclem11  46489  etransclem24  46502  etransclem26  46504  etransclem28  46506  etransclem35  46513  ioorrnopnxr  46551  salgenval  46565  intsaluni  46573  salgenn0  46575  salgencl  46576  sssalgen  46579  salgenss  46580  salgenuni  46581  issalgend  46582  dfsalgen2  46585  subsaliuncl  46602  sge0f1o  46626  sge0fodjrnlem  46660  ismea  46695  nnfoctbdjlem  46699  iundjiun  46704  isome  46738  caragenel  46739  ovn0lem  46809  ovnsubaddlem1  46814  smflimlem4  47018  smflim  47021  sigarcol  47108  chnsubseqwl  47123  nthrucw  47130  cfsetsnfsetf  47304  cfsetsnfsetfo  47306  fnbrafvb  47400  afv2fv0  47511  readdcnnred  47549  resubcnnred  47550  cndivrenred  47552  ceilbi  47579  minusmodnep2tmod  47599  modmkpkne  47607  fargshiftf1  47687  fargshiftfo  47688  ichexmpl2  47716  ichnreuop  47718  ichreuopeq  47719  elsprel  47721  prproropf1olem4  47752  reupr  47768  reuopreuprim  47772  goldbachthlem2  47792  fmtnoprmfac2lem1  47812  fmtnofac2lem  47814  prmdvdsfmtnof1lem2  47831  mod42tp1mod8  47848  lighneallem2  47852  lighneallem3  47853  lighneallem4  47856  proththd  47860  41prothprm  47865  requad01  47867  requad2  47869  dfeven2  47895  dfeven5  47912  dfodd7  47913  fpprel  47974  fppr2odd  47977  fpprwppr  47985  fpprwpprb  47986  nnsum3primesgbe  48038  isubgredg  48112  upgrimpths  48155  ushggricedg  48173  uhgrimisgrgric  48177  isubgr3stgrlem3  48214  isubgr3stgrlem4  48215  isubgr3stgrlem6  48217  grlimprclnbgr  48242  grlimgrtrilem2  48248  gpgedgvtx0  48307  gpgedgvtx1  48308  gpgvtxedg0  48309  gpgvtxedg1  48310  gpg3kgrtriexlem5  48333  gpgprismgr4cycllem3  48343  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  upwlksfval  48381  0nodd  48416  2nodd  48418  nnsgrpnmnd  48424  nn0mnd  48425  lidldomn1  48477  zlidlring  48480  uzlidlring  48481  2zrngamgm  48491  2zrngamnd  48493  2zrngagrp  48495  2zrngnmlid2  48503  ztprmneprm  48593  dmatALTbasel  48648  linindslinci  48694  lindslinindsimp1  48703  lindslinindimp2lem4  48707  lindslinindsimp2lem5  48708  linds0  48711  el0ldep  48712  lindsrng01  48714  snlindsntorlem  48716  snlindsntor  48717  ldepspr  48719  lincresunit3  48727  islindeps2  48729  isldepslvec2  48731  zlmodzxzldep  48750  blen1b  48834  dig2bits  48860  nn0sumshdiglem1  48867  0aryfvalelfv  48881  itcovalsuc  48913  prelrrx2b  48960  eenglngeehlnmlem1  48983  eenglngeehlnmlem2  48984  rrx2linest2  48990  elrrx2linest2  48991  spheres  48992  2sphere  48995  2sphere0  48996  line2ylem  48997  line2  48998  line2xlem  48999  line2x  49000  line2y  49001  itscnhlc0yqe  49005  itschlc0yqe  49006  itscnhlc0xyqsol  49011  itschlc0xyqsol1  49012  itsclc0xyqsolr  49015  itsclc0  49017  itsclc0b  49018  itsclinecirc0b  49020  itsclquadb  49022  itsclquadeu  49023  itscnhlinecirc02p  49031  resinsnALT  49118  sepnsepolem2  49168  sepnsepo  49169  sepfsepc  49173  iscnrm3rlem8  49192  iscnrm3r  49193  iscnrm3llem2  49195  iscnrm3l  49196  oppcendc  49263  isisod  49272  sectpropdlem  49281  ssccatid  49317  resccatlem  49318  imasubc  49396  uptrlem1  49455  oppcthinendcALT  49686  functhinclem2  49690  fullthinc2  49696  thincciso  49698  thinccisod  49699  termcpropd  49748  fulltermc2  49757  oduoppcciso  49811  discsnterm  49819  aacllem  50046