Theorem eqeq1d 2736

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 2727	. . . 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 2727	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
9		dfcleq 2727	. 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 2706

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

This theorem is referenced by:  eqeq1  2738  eqcomd  2740  eqeq2d  2745  eqeqan12d  2748  neeq1d  2989  rspcedeq1vd  3581  csbconstg  3866  csbhypf  3875  csbiebt  3876  csbiebg  3879  sbceq2g  4369  csbie2df  4393  disjeq0  4406  disjssun  4418  mosneq  4796  preq12b  4804  preq12bg  4807  elpreqprlem  4820  disji2  5080  invdisjrab  5083  disjprg  5092  disjxun  5094  iin0  5305  opthg  5423  opeqsng  5449  propeqop  5453  wefrc  5616  xpcan  6132  xpcan2  6133  dmsnopg  6169  rnmpt0f  6199  reuop  6249  dfpo2  6252  sspred  6266  onfr  6354  unisucg  6395  nsuceq0  6400  iotaeq  6458  iotabi  6459  fneq1  6581  fnun  6604  fnresdisj  6610  fnimadisj  6622  fnimaeq0  6623  foeq1  6740  fveqeq2d  6840  fvun1  6923  fvmptdv2  6957  fndmdifeq0  6987  fneqeql  6989  dffo3  7045  dffo3f  7049  fnnfpeq0  7122  foeqcnvco  7244  f1eqcocnv  7245  isofrlem  7284  eqfunresadj  7304  ovanraleqv  7380  f1opr  7412  eloprabga  7465  ovmpodv2  7514  ov3  7519  ovelimab  7534  caovcang  7557  caovcan  7560  caovmo  7593  caofinvl  7652  caofid1  7655  caofid2  7656  caofidlcan  7658  caonncan  7664  tfisi  7799  mptcnfimad  7928  oteqimp  7950  br1steqg  7953  br2ndeqg  7954  eqop  7973  reldm  7986  mposn  8043  fparlem1  8052  fparlem2  8053  fsplit  8057  frxp  8066  xporderlem  8067  fnwelem  8071  xpord2lem  8082  xpord3lem  8089  poseq  8098  soseq  8099  fnsuppeq0  8132  suppssov1  8137  suppssov2  8138  suppofss1d  8144  suppofss2d  8145  tposfo2  8189  mpocurryd  8209  iinon  8270  onnseq  8274  tz7.49  8374  seqomlem2  8380  oe0m1  8446  om0r  8464  oe1m  8470  oawordeulem  8479  oawordeu  8480  oarec  8487  omord  8493  oneo  8506  omeu  8510  oeeui  8528  nnm0r  8536  nnmord  8558  nnawordex  8563  nnaordex2  8565  nnneo  8581  nneob  8582  omopth  8588  nnasmo  8589  ereq1  8640  eqerlem  8668  qsdisj  8729  erov  8749  eceqoveq  8757  mapsnd  8822  endisj  8990  pw2f1olem  9007  enfixsn  9012  disjenex  9061  domssex2  9063  xpf1o  9065  mapxpen  9069  unxpdomlem2  9155  enp1ilem  9176  fodomfib  9227  fodomfibOLD  9229  fipreima  9256  opthreg  9525  cantnfp1lem3  9587  ssttrcl  9622  ttrcltr  9623  ttrclss  9627  ttrclselem2  9633  frmin  9659  updjud  9844  pm54.43  9911  dfac5  10037  dfacacn  10050  kmlem9  10067  cfeq0  10164  cfss  10173  cfslb  10174  fin23lem22  10235  fin23lem12  10239  fin23lem19  10244  fin23lem30  10250  fin23lem33  10253  fin1a2lem6  10313  axcc2lem  10344  axdc3lem2  10359  axdc3lem3  10360  axdc3lem4  10361  axdc3  10362  axdc4lem  10363  zorn2lem7  10410  ttukeylem3  10419  ttukeylem6  10422  ttukey2g  10424  fodomb  10434  axacndlem5  10520  fpwwe2cbv  10539  fpwwe2lem2  10541  fpwwe2lem3  10542  fpwwe2lem11  10550  fpwwe2lem12  10551  fpwwe  10555  pwfseqlem2  10568  pwxpndom2  10574  addnidpi  10810  ltexpi  10811  recmulnq  10873  ltexnq  10884  halfnq  10885  archnq  10889  ltexpri  10952  recexpr  10960  addsrpr  10984  mulsrpr  10985  00sr  11008  negexsr  11011  recexsrlem  11012  recexsr  11016  axrnegex  11071  axrrecex  11072  00id  11306  mul02  11309  addrid  11311  cnegex  11312  cnegex2  11313  subval  11369  subadd  11381  subadd2  11382  subsub23  11383  addsubeq4  11393  subcan2  11404  negcon1  11431  subcan  11434  addrsub  11552  ltordlem  11660  ltord1  11661  recex  11767  mul0or  11775  muleqadd  11779  receu  11780  mulcan1g  11788  divval  11796  divmul  11797  rec11  11837  ldiv  11973  rdiv  11974  zdiv  12560  uzin  12785  xaddval  13136  xmulval  13138  xnn0xadd0  13160  xnegdi  13161  ioo0  13284  ico0  13305  ioc0  13306  icc0  13307  1fv  13561  fzon  13594  fvinim0ffz  13703  flbi  13734  mod0  13794  modmuladdnn0  13836  modirr  13863  addmodlteq  13867  uzrdgfni  13879  axdc4uzlem  13904  fsuppmapnn0fiubex  13913  mptnn0fsupp  13918  seqid  13968  seqz  13971  expval  13984  expeq0  14013  sqeqor  14137  nn0opth2  14193  hashdom  14300  elprchashprn2  14317  hashbc  14374  hashf1lem1  14376  hash2pwpr  14397  ccat0  14497  wrdl1s1  14536  ccatws1lenp1b  14543  pfxsuff1eqwrdeq  14620  swrdccatin2  14650  pfxccatin12lem2  14652  2cshwcshw  14746  scshwfzeqfzo  14747  cshimadifsn  14750  cshimadifsn0  14751  s2f1o  14837  wrdlen2i  14863  2swrd2eqwrdeq  14874  wwlktovf  14877  wwlktovf1  14878  wwlktovfo  14879  wrd2f1tovbij  14881  relexp0g  14943  relexpsucnnr  14946  dfrtrcl2  14983  mulre  15042  rennim  15160  cnpart  15161  01sqrex  15170  resqrex  15171  sqrmo  15172  resqrtcl  15174  resqrtthlem  15175  sqrtgt0  15179  sqrtneg  15188  sqrtsq2  15189  absmod0  15224  sqreulem  15281  sqreu  15282  sqrtthlem  15284  eqsqrtd  15289  reusq0  15386  fsum00  15719  telfsumo  15723  prodss  15868  fprodle  15917  tanaddlem  16089  absefib  16121  efieq1re  16122  divides  16179  dvdsval2  16180  nndivides  16187  dvds0lem  16191  dvds1lem  16192  dvds2lem  16193  negdvdsb  16197  muldvds1  16205  muldvds2  16206  dvdscmulr  16209  dvdsmulcr  16210  difmod0  16212  dvdstr  16219  dvdsabseq  16238  divconjdvds  16240  odd2np1lem  16265  odd2np1  16266  even2n  16267  oddm1even  16268  2tp1odd  16277  opeo  16290  omeo  16291  m1exp1  16301  divalglem4  16321  divalglem8  16325  divalgb  16329  bitsuz  16399  smupvallem  16408  gcdaddmlem  16449  gcdabs1  16454  bezoutlem3  16466  rplpwr  16483  rprpwr  16484  alginv  16500  algcvga  16504  algfx  16505  eucalgval2  16506  coprmdvds  16578  qredeq  16582  qredeu  16583  coprmprod  16586  coprmproddvdslem  16587  divgcdcoprm0  16590  divgcdcoprmex  16591  cncongr1  16592  rpexp  16647  rpexp12i  16649  cncongrprm  16654  qnumdenbi  16669  phival  16692  phicl2  16693  dfphi2  16699  phiprmpw  16701  phimullem  16704  eulerthlem1  16706  eulerthlem2  16707  eulerth  16708  fermltl  16709  hashgcdlem  16713  phisum  16716  odzval  16717  odzdvds  16721  reumodprminv  16730  modprm0  16731  nnnn0modprm0  16732  modprmn0modprm0  16733  coprimeprodsq  16734  coprimeprodsq2  16735  pythagtriplem2  16743  pythagtrip  16760  pcval  16770  pceulem  16771  pcqmul  16779  pcqcl  16782  pcabs  16801  pcgcd1  16803  pc2dvds  16805  pcaddlem  16814  pcadd  16815  pcmpt  16818  prmpwdvds  16830  pockthi  16833  unbenlem  16834  4sqlem12  16882  ramz  16951  ramcl  16955  cshwrepswhash1  17028  imasval  17430  fvprif  17480  iscat  17593  iscatd  17594  catidex  17595  catideu  17596  cidfval  17597  cidval  17598  catidd  17601  catlid  17604  catrid  17605  catpropd  17630  cidpropd  17631  issect  17675  dfiso2  17694  invcoisoid  17714  isocoinvid  17715  setcepi  18010  latleeqj2  18373  latleeqm2  18389  oduclatb  18428  mgmidmo  18583  grpidval  18584  grpidpropd  18585  ismgmid  18588  ismgmid2  18591  mgmidsssn0  18595  grpinvalem  18596  grprida  18598  gsumvalx  18599  gsumpropd  18601  gsumpropd2lem  18602  gsumress  18605  gsumval2  18609  ismnddef  18659  sgrpidmnd  18662  ismndd  18679  mndpropd  18682  mndinvmod  18687  mnd1  18702  ismhm  18708  gsumvallem2  18757  frmdgsum  18785  frmdup3  18790  efmndmnd  18812  smndex1mnd  18833  sgrp2rid2  18849  sgrp2rid2ex  18850  pwmnd  18860  grpinvex  18871  isgrpd2  18884  isgrpd  18886  dfgrp2  18890  grpinveu  18902  grpinvval  18908  grplinv  18917  isgrpinv  18921  grplrinv  18924  grpidinv2  18925  grpidinv  18926  grplmulf1o  18941  grpraddf1o  18942  grpsubeq0  18954  grpsubadd  18956  dfgrp3lem  18966  dfgrp3  18967  grp1  18975  imasgrp2  18983  qusgrp2  18986  mhmmnd  18992  ghmgrp  18994  mulgval  18999  mulgaddcom  19026  eqg0el  19110  cycsubmel  19127  ghmeqker  19170  ghmf1  19173  conjnmzb  19180  ghmqusker  19214  isga  19218  subgga  19227  gaorb  19234  gaorber  19235  gastacl  19236  gastacos  19237  orbsta  19240  symgfix2  19343  gsmsymgrfixlem1  19354  gsmsymgrfix  19355  gsmsymgreq  19359  symgfixelq  19360  f1omvdconj  19373  pmtrdifwrdel2  19413  psgnunilem1  19420  psgnunilem2  19422  psgnunilem3  19423  psgnunilem4  19424  odval  19461  odid  19465  odlem2  19466  oddvdsnn0  19471  odnncl  19472  oddvds  19474  odcong  19476  odeq  19477  odmulgid  19481  odmulgeq  19484  gexval  19505  gexid  19508  gexlem2  19509  gexdvdsi  19510  gexdvds  19511  subgpgp  19524  sylow1lem1  19525  sylow1lem4  19528  sylow2alem1  19544  sylow2alem2  19545  sylow2blem2  19548  sylow3lem6  19559  lsmdisj3a  19616  lsmdisj3b  19617  pj1val  19622  pj1eq  19627  efgredlemd  19671  efgredlem  19674  efgred  19675  efgrelexlema  19676  frgpup3  19705  ablsubadd  19736  ablsubsub23  19751  iscyggen  19807  cyggenod  19811  gsumval3lem2  19833  gsumval3  19834  gsummptnn0fz  19913  dmdprd  19927  dprddisj  19938  dprdfeq0  19951  dprdf11  19952  dmdprdpr  19978  dpjeq  19988  ablfacrp  19995  pgpfac1lem2  20004  pgpfac1lem3  20006  pgpfac1lem5  20008  pgpfac1  20009  pgpfaclem1  20010  pgpfaclem2  20011  pgpfaclem3  20012  ablfaclem2  20015  ablfaclem3  20016  ablfac2  20018  rngmneg1  20100  rngmneg2  20101  ringurd  20118  srgrz  20140  srglz  20141  srgisid  20142  srg1zr  20148  ringid  20207  qusring2  20268  opprring  20281  dvdsrval  20295  dvdsrmul  20298  dvdsr01  20305  dvdsr02  20306  crngunit  20312  ringunitnzdiv  20332  dvreq1  20345  dvdsrpropd  20350  irredn0  20357  irredrmul  20361  irredmul  20363  rngisomring  20401  rhmdvdsr  20439  lringuplu  20475  subrg1  20513  subrgdvds  20517  isrrg  20629  rrgeq0i  20630  rrgeq0  20631  domneq0  20639  isdomn4  20647  domnlcanb  20651  domnrcanb  20653  drngid2  20683  drngmul0orOLD  20692  isdrngd  20696  isdrngdOLD  20698  fidomndrnglem  20703  isabv  20742  issrngd  20786  islmod  20813  islmodd  20815  lmodprop2d  20873  mptscmfsupp0  20876  lss1d  20912  lspextmo  21006  lvecvs0or  21061  lvecvscan  21064  lvecvscan2  21065  lbsacsbs  21109  rngqiprngimf1lem  21247  rng2idl1cntr  21258  prmirredlem  21425  pzriprnglem7  21440  pzriprnglem13  21446  chrdvds  21479  chrnzr  21483  domnchr  21485  znval  21488  zncyg  21501  znfld  21513  znunit  21516  znrrg  21518  frgpcyg  21526  psgndiflemB  21553  psgndiflemA  21554  ipeq0  21591  ip2eq  21606  elocv  21621  ocvi  21622  obsne0  21678  dsmmacl  21694  dsmmlss  21697  frlmphl  21734  frlmup4  21754  islindf4  21791  islindf5  21792  mplsubrglem  21957  mplmon2  22014  evlslem1  22035  evlseu  22036  evlsval  22039  evlsval2  22040  evlsval3  22042  ismhp3  22083  mhpsclcl  22088  mhpvarcl  22089  mhpmulcl  22090  psdmul  22107  psdmvr  22110  cply1coe0bi  22244  gsummoncoe1  22250  evl1vsd  22286  dmatel  22435  dmatelnd  22438  dmatmulcl  22442  scmateALT  22454  mdetdiaglem  22540  mdetunilem1  22554  mdetunilem3  22556  mdetunilem4  22557  mdetunilem9  22562  symgmatr01lem  22595  symgmatr01  22596  gsummatr01lem1  22597  gsummatr01lem4  22600  gsummatr01  22601  smadiadetlem3  22610  cramerlem3  22631  pmatcoe1fsupp  22643  cpmatel  22653  1elcpmat  22657  cpmatmcllem  22660  cpmatmcl  22661  d1mat2pmat  22681  m2cpminvid2lem  22696  m2cpminvid2  22697  decpmatmulsumfsupp  22715  pmatcollpw2lem  22719  pmatcollpwscmatlem1  22731  mp2pm2mplem4  22751  pm2mpmhmlem1  22760  chpscmat  22784  cpmidpmatlem3  22814  cayleyhamilton0  22831  cayleyhamiltonALT  22833  cayleyhamilton1  22834  0ntr  23013  ntreq0  23019  cldlp  23092  pnrmopn  23285  hausnei2  23295  cnhaus  23296  nrmsep  23299  isnrm2  23300  regsep2  23318  dishaus  23324  ordthauslem  23325  iscmp  23330  cmpsublem  23341  cmpsub  23342  tgcmp  23343  sscmp  23347  hauscmplem  23348  cmpfi  23350  bwth  23352  connsuba  23362  nconnsubb  23365  isref  23451  islocfin  23459  elpt  23514  elptr  23515  pthaus  23580  txcmp  23585  hausdiag  23587  txhaus  23589  txkgen  23594  xkohaus  23595  xkococnlem  23601  regr1lem  23681  fbasrn  23826  fmfnfmlem3  23898  flimtopon  23912  fclstopon  23954  alexsubb  23988  symgtgp  24048  qustgpopn  24062  qustgphaus  24065  ustuqtop  24188  isusp  24203  ispsmet  24246  psmet0  24250  ismet  24265  isxmet  24266  xmeteq0  24280  metn0  24302  xmetres2  24303  imasf1oxmet  24317  xblss2ps  24343  xblss2  24344  xmseq0  24406  comet  24455  stdbdxmet  24457  methaus  24462  dscmet  24514  nrmmetd  24516  nmeq0  24560  tngngp  24596  tngngp3  24598  nlmmul0or  24625  cnmet  24713  xrsxmet  24752  metnrmlem3  24804  icopnfcnv  24894  iccpnfcnv  24896  ishtpy  24925  isphtpy  24934  phtpyi  24937  om1elbas  24986  elpi1i  25000  pi1grplem  25003  isclmp  25051  cphsqrtcl2  25140  tcphcph  25191  bcth3  25285  rrxcph  25346  rrxmet  25362  ivth2  25410  iundisj2  25504  dyaddisj  25551  volivth  25562  mbfinf  25620  i1f1lem  25644  i1fmullem  25649  i1fmulclem  25657  i1fres  25660  itg1climres  25669  mbfi1fseqlem4  25673  dvnres  25887  dvcobr  25903  dvcobrOLD  25904  rolle  25948  cmvth  25949  cmvthOLD  25950  deg1leb  26054  ismon1p  26102  q1peqb  26115  dvdsr1p  26123  ply1remlem  26124  fta1glem2  26128  idomrootle  26132  elply2  26155  ne0p  26166  coeeu  26184  coelem  26185  coeeq  26186  dgrle  26202  coeaddlem  26208  plymul0or  26242  ofmulrt  26243  plydivlem3  26257  plydivlem4  26258  plydivex  26259  plydiveu  26260  plydivalg  26261  quotlem  26262  plyremlem  26266  quotcan  26271  plyexmo  26275  elqaalem3  26283  qaa  26285  iaa  26287  aareccl  26288  aacjcl  26289  aannenlem2  26291  reeff1o  26411  sineq0  26487  coseq1  26488  efeq1  26491  recosf1o  26498  logeftb  26546  cosarg0d  26572  logtayl  26623  cxpval  26627  cxpeq0  26641  root1eq1  26719  cxpeq  26721  logbgcd1irr  26758  angrtmuld  26772  affineequiv  26787  affineequiv3  26789  angpieqvdlem2  26793  quad2  26803  dcubic1lem  26807  dcubic2  26808  dcubic  26810  mcubic  26811  cubic2  26812  dquartlem1  26815  dquart  26817  quart  26825  atandm2  26841  atandm4  26843  atantan  26887  wilthlem2  27033  wilthlem3  27034  muval2  27098  isnsqf  27099  mumullem2  27144  sqff1o  27146  muinv  27157  mpodvdsmulf1o  27158  dvdsmulf1o  27160  dchrelbas2  27202  dchrmullid  27217  dchrfi  27220  lgsval  27266  lgsdir  27297  lgsne0  27300  lgsprme0  27304  lgsdirnn0  27309  lgsqrlem1  27311  lgsqr  27316  gausslemma2dlem0c  27323  gausslemma2dlem0i  27329  gausslemma2dlem7  27338  gausslemma2d  27339  lgseisenlem2  27341  lgsquadlem1  27345  lgsquadlem2  27346  lgsquad2lem2  27350  lgsquad3  27352  m1lgs  27353  2lgs  27372  2sqlem7  27389  2sqlem8  27391  2sqlem9  27392  2sqlem11  27394  2sq  27395  2sq2  27398  2sqmo  27402  addsq2reu  27405  addsqn2reu  27406  addsqrexnreu  27407  addsqnreup  27408  addsq2nreurex  27409  2sqreulem1  27411  2sqreultlem  27412  2sqreunnlem1  27414  2sqreunnltlem  27415  2sqreulem4  27419  2sqreuop  27427  2sqreuopnn  27428  2sqreuoplt  27429  2sqreuopltb  27430  2sqreuopnnlt  27431  2sqreuopnnltb  27432  2sqreuopb  27433  dchrisumlem1  27454  dchrvmaeq0  27469  dchrisum0re  27478  ostth3  27603  sltval  27613  nosepssdm  27652  nosupprefixmo  27666  noinfprefixmo  27667  nosupcbv  27668  nosupdm  27670  nosupfv  27672  nosupres  27673  nosupbnd1lem1  27674  nosupbnd1lem3  27676  nosupbnd1lem5  27678  noinfcbv  27683  noinfdm  27685  noinffv  27687  noinfres  27688  noinfbnd1lem3  27691  noinfbnd1lem5  27693  eqscut  27773  scutbdaylt  27786  made0  27845  madecut  27855  negsid  28010  negsex  28012  subadds  28039  divsmo  28153  muls0ord  28154  divsval  28158  norecdiv  28159  recsne0  28161  divsmulw  28162  divs1  28173  precsexlem8  28182  precsexlem9  28183  precsexlem11  28185  precsex  28186  recsex  28187  abssor  28214  elons  28221  noseqrdgfn  28267  bdayn0sf1o  28328  eucliddivs  28334  zsoring  28367  n0seo  28379  zseo  28380  nohalf  28382  expsne0  28394  pw2recs  28396  halfcut  28415  zs12negscl  28427  zs12zodd  28431  zs12ge0  28432  renegscl  28443  istrkg3ld  28482  axtgcgrid  28484  axtgsegcon  28485  axtg5seg  28486  axtgupdim2  28492  tgjustc1  28496  tgjustc2  28497  iscgrg  28533  isismt  28555  legov  28606  legov2  28607  hlcgreu  28639  mirreu3  28675  mircgr  28678  mirbtwn  28679  ismir  28680  mireq  28686  ismidb  28799  lmiopp  28823  dfcgra2  28851  inaghl  28866  f1otrg  28892  ttgval  28896  ttgelitv  28904  brbtwn  28921  brcgr  28922  colinearalglem2  28929  colinearalg  28932  axsegconlem1  28939  axsegcon  28949  ax5seglem4  28954  ax5seglem5  28955  axpaschlem  28962  axpasch  28963  axlowdimlem16  28979  axeuclidlem  28984  axeuclid  28985  axcontlem2  28987  axcontlem4  28989  axcontlem5  28990  edglnl  29165  usgredg2ALT  29215  usgredgprvALT  29217  usgrnloopvALT  29223  ushgredgedgloop  29253  edg0usgr  29275  nb3grpr  29404  cplgr1v  29452  cusgrsize  29477  vtxdgfval  29490  vtxdeqd  29500  vtxdun  29504  vtxd0nedgb  29511  vtxdusgr0edgnelALT  29519  1loopgrvd2  29526  usgruvtxvdb  29552  usgrvd0nedg  29556  vtxdginducedm1  29566  rusgrpropedg  29607  wksfval  29632  wlklenvclwlk  29676  iswlkon  29678  ispth  29743  dfpth2  29751  upgrwlkdvdelem  29758  crctcshwlkn0lem6  29837  wwlknon  29879  wwlksm1edg  29903  wwlksnextbi  29916  wwlksnextfun  29920  wwlksnextinj  29921  wwlksnextsurj  29922  wwlksnextbij  29924  wlksnwwlknvbij  29930  wwlksnextproplem3  29933  wwlksnextprop  29934  wspn0  29946  umgr2adedgwlkonALT  29969  umgr2adedgspth  29970  umgr2wlkon  29972  rusgrnumwwlkslem  29994  rusgrnumwwlkb0  29996  rusgrnumwwlks  29999  clwlkclwwlklem2a4  30021  clwlknf1oclwwlknlem2  30106  clwlknf1oclwwlkn  30108  isclwwlknon  30115  clwwlknon1loop  30122  s2elclwwlknon2  30128  clwwlknonwwlknonb  30130  clwwlkvbij  30137  uhgr3cyclex  30206  fusgreg2wsplem  30357  fusgr2wsp2nb  30358  fusgreghash2wsp  30362  frrusgrord0  30364  2clwwlkel  30373  extwwlkfab  30376  extwwlkfabel  30377  clwwlknonclwlknonf1o  30386  dlwwlknondlwlknonf1o  30389  wlkl0  30391  numclwwlk2lem1  30400  numclwlk2lem2f  30401  numclwlk2lem2f1o  30403  numclwwlk5  30412  ex-opab  30456  isgrpo  30521  isgrpoi  30522  grpoidinvlem3  30530  grpoideu  30533  gidval  30536  grpoidinv2  30539  grpoinveu  30543  grpoinvval  30547  grpoinv  30549  vciOLD  30585  isvclem  30601  cnidOLD  30606  isnvlem  30634  nvmul0or  30674  imsmetlem  30714  diporthcom  30740  ipz  30743  nmlno0  30819  ajfval  30833  hmoval  30834  isphg  30841  isph  30846  ip2eqi  30880  ajval  30885  hvmul0or  31049  hvsubeq0  31092  hvaddeq0  31093  hvaddcan  31094  hvmulcan  31096  hvmulcan2  31097  hvsubadd  31101  his6  31123  hial0  31126  hial02  31127  hi2eq  31129  orthcom  31132  normlem7tALT  31143  normsub0  31160  normpyth  31169  hilid  31185  hhssnv  31288  ocel  31305  ocsh  31307  ocorth  31315  ocin  31320  occllem  31327  choc0  31350  pjpreeq  31422  omlsi  31428  pjoc1  31458  pjoml  31460  pjoc2  31463  chm0  31515  chocin  31519  chlejb1  31536  chlejb2  31537  chjo  31539  h1deoi  31573  h1de2i  31577  pjoml6i  31613  pjoml2  31635  pjoml3  31636  pjch  31718  hodsi  31799  hodid  31816  eigorth  31862  elunop  31896  adjeu  31913  adjval  31914  eigvecval  31920  unopf1o  31940  adj1  31957  adjeq  31959  hmdmadj  31964  lnopeq0i  32031  lnopeqi  32032  lnopeq  32033  lnfn0  32071  riesz4i  32087  riesz4  32088  riesz1  32089  cnlnadjlem3  32093  cnlnadjlem5  32095  cnlnadjeu  32102  cnlnssadj  32104  nmopadjlei  32112  opsqrlem1  32164  hmopidmpji  32176  pjimai  32200  isst  32237  ishst  32238  hstel2  32243  stadd3i  32272  stri  32281  largei  32291  golem2  32296  superpos  32378  sumdmdii  32439  mddmdin0i  32455  opreu2reuALT  32500  difeq  32542  elim2if  32568  disji2f  32601  disjif2  32605  disjxpin  32612  iundisj2f  32614  disjunsn  32618  fmptco1f1o  32660  ofpreima  32692  fnpreimac  32698  ressupprn  32718  curry2ima  32737  preiman0  32738  receqid  32773  xrofsup  32796  iundisj2fi  32826  f1ocnt  32829  fzo0opth  32832  elq2  32841  fprodex01  32855  sgn0bi  32870  ind1a  32887  prodindf  32893  xdivval  32949  xrecex  32950  xreceu  32952  xdivmul  32955  rexdiv  32956  wrdt2ind  32984  mndlrinvb  33056  mndlactfo  33058  mndractfo  33060  mndlactf1o  33061  mndractf1o  33062  gsummpt2d  33081  gsumwun  33107  fzo0pmtrlast  33123  cyc3genpm  33183  cycpmconjslem2  33186  fxpval  33196  fxpgaeq  33200  cntrval2  33202  isslmd  33233  slmdlema  33234  urpropd  33262  elrgspnlem4  33276  elrgspnsubrunlem2  33279  erlcl1  33291  erlcl2  33292  erldi  33293  erlbrd  33294  erler  33296  rloccring  33301  domnprodeq0  33307  domnlcanOLD  33311  isdrng4  33326  fracerl  33337  fracfld  33339  resv1r  33369  islinds5  33397  linds2eq  33411  dvdsruassoi  33414  dvdsruasso  33415  dvdsruasso2  33416  quslsm  33435  rhmimaidl  33462  qsidomlem2  33483  ssdifidllem  33486  ssdifidl  33487  ssdifidlprm  33488  opprqus0g  33520  qsdrngilem  33524  unitmulrprm  33558  1arithidom  33567  1arithufdlem3  33576  1arithufdlem4  33577  ply1dg1rt  33610  r1pid2OLD  33639  extvfvv  33648  extvfvcl  33650  evlextv  33656  esplysply  33678  esplyind  33680  lbsdiflsp0  33732  fedgmullem1  33735  fedgmullem2  33736  irngss  33793  irngnzply1lem  33796  extdgfialglem2  33799  ply1annidllem  33807  ply1annnr  33809  minplymindeg  33814  minplyann  33815  minplyirredlem  33816  minplyirred  33817  irngnminplynz  33818  minplyelirng  33821  irredminply  33822  algextdeglem6  33828  algextdeglem7  33829  rtelextdg2lem  33832  fldext2chn  33834  constrsuc  33844  constrsslem  33847  constrconj  33851  constrextdg2lem  33854  constrextdg2  33855  constrlccllem  33859  constrcccllem  33860  constrcbvlem  33861  constrext2chn  33865  constrcon  33880  1smat1  33910  iscref  33950  metidval  33996  metidv  33998  metider  34000  pstmxmet  34003  xrmulc1cn  34036  esumfsup  34176  esumpcvgval  34184  esumcvg  34192  inelsros  34284  diffiunisros  34285  ismeas  34305  isrnmeas  34306  brae  34347  braew  34348  dya2iocuni  34389  elcarsg  34411  eulerpartleme  34469  eulerpartlemv  34470  eulerpartlemb  34474  eulerpartgbij  34478  eulerpartlemr  34480  eulerpartlemgvv  34482  eulerpartlemgh  34484  eulerpartlemn  34487  elprob  34515  ballotlemi  34607  ballotlemi1  34609  ballotlemii  34610  ballotlemsima  34622  ballotlemfrcn0  34636  signsw0g  34662  signswmnd  34663  signstfvc  34680  prodfzo03  34709  reprval  34716  reprsum  34719  reprsuc  34721  reprpmtf1o  34732  axtgupdim2ALTV  34774  brafs  34778  bnj125  34977  bnj154  34983  bnj526  34993  bnj609  35022  bnj893  35033  bnj1321  35132  bnj1491  35162  nummin  35198  fineqvnttrclselem2  35227  fineqvnttrclselem3  35228  fineqvnttrclse  35229  noinfepfnregs  35237  subgrwlk  35275  loop1cycl  35280  subfacp1lem3  35325  subfacp1lem5  35327  subfacp1lem6  35328  cnpconn  35373  txpconn  35375  ptpconn  35376  indispconn  35377  connpconn  35378  cvxpconn  35385  cvmscbv  35401  cvmsi  35408  cvmsval  35409  cvmsdisj  35413  cvmsss2  35417  cvmliftmo  35427  cvmliftlem14  35440  cvmliftiota  35444  cvmlift2lem12  35457  cvmlift2lem13  35458  cvmlift2  35459  cvmliftphtlem  35460  cvmlift3lem2  35463  cvmlift3lem4  35465  cvmlift3lem6  35467  cvmlift3lem7  35468  cvmlift3lem9  35470  cvmlift3  35471  snmlval  35474  satffunlem  35544  prv1n  35574  mrsub0  35659  mrsubcn  35662  ismfs  35692  sinccvglem  35815  br6  35900  brbigcup  36039  imageval  36071  funpartlem  36085  dfrdg4  36094  altopthsn  36104  brsegle  36251  rankeq1o  36314  cbviotadavw  36412  subtr  36457  opnbnd  36468  cldbnd  36469  isfne  36482  topfneec  36498  neibastop3  36505  cnndvlem2  36681  bj-imdirval2  37327  bj-imdirid  37330  bj-imdirco  37334  bj-inftyexpiinj  37353  bj-isrvecd  37442  bj-isrvec2  37444  bj-bary1lem1  37455  bj-bary1  37456  finxp00  37546  nlpfvineqsn  37553  pibp19  37558  pibt2  37561  unccur  37743  matunitlindflem2  37757  ptrecube  37760  poimirlem4  37764  poimirlem19  37779  poimirlem23  37783  poimirlem25  37785  poimirlem27  37787  poimirlem28  37788  poimirlem31  37791  poimirlem32  37792  broucube  37794  mblfinlem2  37798  ovoliunnfl  37802  voliunnfl  37804  volsupnfl  37805  mbfresfi  37806  itg2addnclem  37811  itg2addnclem3  37813  itg2addnc  37814  ftc2nc  37842  cover2  37855  sdclem2  37882  fdc  37885  metf1o  37895  istotbnd3  37911  0totbnd  37913  sstotbnd2  37914  equivtotbnd  37918  totbndbnd  37929  prdstotbnd  37934  heibor1  37950  rrnmet  37969  isexid  37987  ismgmOLD  37990  opidonOLD  37992  exidu1  37996  cmpidelt  37999  exidreslem  38017  exidres  38018  exidresid  38019  grpoeqdivid  38021  elghomlem1OLD  38025  grpokerinj  38033  isrngo  38037  isrngod  38038  rngoideu  38043  isgrpda  38095  isdrngo2  38098  isdrngo3  38099  isrngohom  38105  divrngidl  38168  dmnnzd  38215  dmncan1  38216  disjeccnvep  38422  disjressuc2  38535  mopre  38584  qsdisjALTV  38811  dmqseqeq1  38840  unidmqseq  38853  disjdmqseq  39003  eldisjlem19  39008  riotasvd  39155  toycom  39172  islshpsm  39179  lshpnel2N  39184  lsatfixedN  39208  islshpat  39216  lcvexchlem4  39236  l1cvpat  39253  lkr0f  39293  lkrsc  39296  lshpkrlem1  39309  lkreqN  39369  isopos  39379  oposlem  39381  opcon2b  39396  cmtbr3N  39453  cvlcvrp  39539  hlrelat5N  39600  cvrval5  39614  cvrat4  39642  3atlem5  39686  2at0mat0  39724  psubclsetN  40135  4atex2  40276  isldil  40309  ltrnu  40320  ltrnid  40334  isdilN  40353  trlnid  40378  cdleme21k  40537  cdleme29b  40574  cdlemefrs29pre00  40594  cdlemefrs29bpre0  40595  cdlemefrs29cpre1  40597  cdleme32fva  40636  cdleme42b  40677  cdleme50ex  40758  cdleme  40759  cdlemg1a  40769  ltrniotaval  40780  cdlemeiota  40784  tendoid0  41024  cdlemksv2  41046  cdlemkuv2  41066  cdlemk36  41112  cdlemk42  41140  cdlemk  41173  tendoex  41174  cdleml3N  41177  cdleml5N  41179  tendospcanN  41222  cdlemm10N  41317  dihffval  41429  dihfval  41430  dihlsscpre  41433  islpolN  41682  mapdhval  41923  mapdheq  41927  hdmap1fval  41995  hdmap1val  41997  hdmap1eq  42000  hdmap1cbv  42001  hdmapval2lem  42030  hdmap11  42047  hdmap14lem2a  42066  hdmap14lem6  42072  hgmapval  42086  hlhillcs  42157  hlhilphllem  42158  aks4d1  42282  isprimroot  42286  mndmolinv  42288  linvh  42289  primrootsunit1  42290  primrootsunit  42291  primrootscoprmpow  42292  primrootscoprbij  42295  primrootlekpowne0  42298  primrootspoweq0  42299  ringexp0nn  42327  aks6d1c5lem1  42329  sticksstones8  42346  sticksstones9  42347  sticksstones10  42348  sticksstones11  42349  sticksstones12a  42350  sticksstones12  42351  sticksstones16  42355  sticksstones17  42356  sticksstones18  42357  sticksstones19  42358  aks6d1c6lem4  42366  aks6d1c6isolem3  42369  rhmqusspan  42378  grpods  42387  unitscyglem1  42388  unitscyglem2  42389  unitscyglem3  42390  unitscyglem5  42392  expeq1d  42521  zdivgd  42534  ef11d  42536  resubval  42564  renegadd  42569  resubeu  42574  resubadd  42576  sn-remul0ord  42605  sn-negex12  42614  addinvcom  42629  redivvald  42639  rediveud  42640  redivmuld  42642  sn-mul02  42649  mulgt0con1d  42667  mulgt0con2d  42668  fimgmcyclem  42730  fidomncyc  42732  fsuppind  42775  mhphflem  42781  prjspnfv01  42809  prjspner01  42810  prjspner1  42811  prjcrvval  42817  dffltz  42819  flt4lem7  42844  nna4b4nsq  42845  negexpidd  42866  mzpcompact2lem  42935  eldioph  42942  eldioph2lem1  42944  eldioph2lem2  42945  eldioph2  42946  eldioph2b  42947  eldioph3  42950  diophin  42956  diophun  42957  eq0rabdioph  42960  dvdsrabdioph  42994  eldioph4i  42996  diophren  42997  rabren3dioph  42999  fphpd  43000  pellexlem5  43017  pellexlem6  43018  pellex  43019  pell1qrval  43030  pell14qrval  43032  pell1234qrval  43034  pell1234qrreccl  43038  pell1234qrmulcl  43039  pell1234qrdich  43045  pell14qrdich  43053  pell1qr1  43055  pellqrexplicit  43061  rmxycomplete  43101  jm2.27  43192  rmydioph  43198  rmxdiophlem  43199  rmxdioph  43200  pw2f1ocnv  43221  pwssplit4  43273  elmnc  43320  dgraalem  43329  dgraaub  43332  dgraa0p  43333  mpaaeu  43334  mpaaval  43335  mpaalem  43336  aaitgo  43346  rngunsnply  43353  proot1ex  43380  cantnfresb  43508  tfsconcatfv  43525  tfsconcatb0  43528  tfsconcat0i  43529  tfsconcat0b  43530  tfsconcat00  43531  tfsconcatrev  43532  naddwordnexlem4  43585  sqrtcval  43824  relexpnul  43861  relexpxpnnidm  43886  relexpiidm  43887  trclfvdecomr  43911  rfovcnvf1od  44187  ntrkbimka  44221  ntrk0kbimka  44222  clsk3nimkb  44223  clsk1independent  44229  ntrclsfveq1  44243  ntrclsfveq2  44244  ntrclskb  44252  k0004val  44333  k0004val0  44337  mnringmulrcld  44411  expgrowth  44518  bcc0  44523  relpfrlem  45136  permac8prim  45197  disjinfi  45378  fsumf1of  45762  limsupmnflem  45906  liminfpnfuz  46002  climxlim2lem  46031  coseq0  46050  icccncfext  46073  dvnmptconst  46127  dvnprodlem1  46132  dvnprodlem2  46133  dvnprodlem3  46134  dvnprod  46135  stoweidlem15  46201  stoweidlem31  46217  stoweidlem35  46221  stoweidlem36  46222  stoweidlem37  46223  stoweidlem43  46229  stoweidlem44  46230  stoweidlem46  46232  stoweidlem55  46241  stoweidlem59  46245  dirkerval2  46280  dirkertrigeqlem1  46284  dirkeritg  46288  dirkercncf  46293  fourierdlem2  46295  fourierdlem3  46296  fourierdlem42  46335  fourierdlem48  46340  fourierdlem49  46341  fourierdlem71  46363  fourierdlem112  46404  fourierdlem113  46405  elaa2lem  46419  etransclem11  46431  etransclem24  46444  etransclem26  46446  etransclem28  46448  etransclem35  46455  ioorrnopnxr  46493  salgenval  46507  intsaluni  46515  salgenn0  46517  salgencl  46518  sssalgen  46521  salgenss  46522  salgenuni  46523  issalgend  46524  dfsalgen2  46527  subsaliuncl  46544  sge0f1o  46568  sge0fodjrnlem  46602  ismea  46637  nnfoctbdjlem  46641  iundjiun  46646  isome  46680  caragenel  46681  ovn0lem  46751  ovnsubaddlem1  46756  smflimlem4  46960  smflim  46963  sigarcol  47050  chnsubseqwl  47065  nthrucw  47072  cfsetsnfsetf  47246  cfsetsnfsetfo  47248  fnbrafvb  47342  afv2fv0  47453  readdcnnred  47491  resubcnnred  47492  cndivrenred  47494  ceilbi  47521  minusmodnep2tmod  47541  modmkpkne  47549  fargshiftf1  47629  fargshiftfo  47630  ichexmpl2  47658  ichnreuop  47660  ichreuopeq  47661  elsprel  47663  prproropf1olem4  47694  reupr  47710  reuopreuprim  47714  goldbachthlem2  47734  fmtnoprmfac2lem1  47754  fmtnofac2lem  47756  prmdvdsfmtnof1lem2  47773  mod42tp1mod8  47790  lighneallem2  47794  lighneallem3  47795  lighneallem4  47798  proththd  47802  41prothprm  47807  requad01  47809  requad2  47811  dfeven2  47837  dfeven5  47854  dfodd7  47855  fpprel  47916  fppr2odd  47919  fpprwppr  47927  fpprwpprb  47928  nnsum3primesgbe  47980  isubgredg  48054  upgrimpths  48097  ushggricedg  48115  uhgrimisgrgric  48119  isubgr3stgrlem3  48156  isubgr3stgrlem4  48157  isubgr3stgrlem6  48159  grlimprclnbgr  48184  grlimgrtrilem2  48190  gpgedgvtx0  48249  gpgedgvtx1  48250  gpgvtxedg0  48251  gpgvtxedg1  48252  gpg3kgrtriexlem5  48275  gpgprismgr4cycllem3  48285  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgnbgreunbgrlem2lem3  48304  upwlksfval  48323  0nodd  48358  2nodd  48360  nnsgrpnmnd  48366  nn0mnd  48367  lidldomn1  48419  zlidlring  48422  uzlidlring  48423  2zrngamgm  48433  2zrngamnd  48435  2zrngagrp  48437  2zrngnmlid2  48445  ztprmneprm  48535  dmatALTbasel  48590  linindslinci  48636  lindslinindsimp1  48645  lindslinindimp2lem4  48649  lindslinindsimp2lem5  48650  linds0  48653  el0ldep  48654  lindsrng01  48656  snlindsntorlem  48658  snlindsntor  48659  ldepspr  48661  lincresunit3  48669  islindeps2  48671  isldepslvec2  48673  zlmodzxzldep  48692  blen1b  48776  dig2bits  48802  nn0sumshdiglem1  48809  0aryfvalelfv  48823  itcovalsuc  48855  prelrrx2b  48902  eenglngeehlnmlem1  48925  eenglngeehlnmlem2  48926  rrx2linest2  48932  elrrx2linest2  48933  spheres  48934  2sphere  48937  2sphere0  48938  line2ylem  48939  line2  48940  line2xlem  48941  line2x  48942  line2y  48943  itscnhlc0yqe  48947  itschlc0yqe  48948  itscnhlc0xyqsol  48953  itschlc0xyqsol1  48954  itsclc0xyqsolr  48957  itsclc0  48959  itsclc0b  48960  itsclinecirc0b  48962  itsclquadb  48964  itsclquadeu  48965  itscnhlinecirc02p  48973  resinsnALT  49060  sepnsepolem2  49110  sepnsepo  49111  sepfsepc  49115  iscnrm3rlem8  49134  iscnrm3r  49135  iscnrm3llem2  49137  iscnrm3l  49138  oppcendc  49205  isisod  49214  sectpropdlem  49223  ssccatid  49259  resccatlem  49260  imasubc  49338  uptrlem1  49397  oppcthinendcALT  49628  functhinclem2  49632  fullthinc2  49638  thincciso  49640  thinccisod  49641  termcpropd  49690  fulltermc2  49699  oduoppcciso  49753  discsnterm  49761  aacllem  49988