Theorem eqeq1d 2737

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 2728	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	biimpi 216	. . 3 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		bibi1 351	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	alimi 1811	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		albi 1818	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)) → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
7	1, 3, 5, 6	4syl 19	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
8		dfcleq 2728	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
9		dfcleq 2728	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
10	7, 8, 9	3bitr4g 314	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  eqeq1  2739  eqcomd  2741  eqeq2d  2746  eqeqan12d  2749  neeq1d  2991  rspcedeq1vd  3608  csbconstg  3893  csbhypf  3902  csbiebt  3903  csbiebg  3906  sbceq2g  4394  csbie2df  4418  disjeq0  4431  disjssun  4443  mosneq  4818  preq12b  4826  preq12bg  4829  elpreqprlem  4842  disji2  5103  invdisjrab  5106  disjprg  5115  disjxun  5117  iin0  5332  opthg  5452  opeqsng  5478  propeqop  5482  wefrc  5648  xpcan  6165  xpcan2  6166  dmsnopg  6202  rnmpt0f  6232  reuop  6282  dfpo2  6285  sspred  6299  onfr  6391  unisucg  6431  nsuceq0  6436  iotaeq  6495  iotabi  6496  fneq1  6628  fnun  6651  fnresdisj  6657  fnimadisj  6669  fnimaeq0  6670  foeq1  6785  fveqeq2d  6883  fvun1  6969  fvmptdv2  7003  fndmdifeq0  7033  fneqeql  7035  dffo3  7091  dffo3f  7095  fnnfpeq0  7169  foeqcnvco  7292  f1eqcocnv  7293  isofrlem  7332  eqfunresadj  7352  ovanraleqv  7427  f1opr  7461  eloprabga  7514  ovmpodv2  7563  ov3  7568  ovelimab  7583  caovcang  7606  caovcan  7609  caovmo  7642  caofinvl  7701  caofid1  7704  caofid2  7705  caofidlcan  7707  caonncan  7713  tfisi  7852  mptcnfimad  7983  oteqimp  8005  br1steqg  8008  br2ndeqg  8009  eqop  8028  reldm  8041  mposn  8100  fparlem1  8109  fparlem2  8110  fsplit  8114  frxp  8123  xporderlem  8124  fnwelem  8128  xpord2lem  8139  xpord3lem  8146  poseq  8155  soseq  8156  fnsuppeq0  8189  suppssov1  8194  suppssov2  8195  suppofss1d  8201  suppofss2d  8202  tposfo2  8246  mpocurryd  8266  iinon  8352  onnseq  8356  tz7.49  8457  seqomlem2  8463  oe0m1  8531  om0r  8549  oe1m  8555  oawordeulem  8564  oawordeu  8565  oarec  8572  omord  8578  oneo  8591  omeu  8595  oeeui  8612  nnm0r  8620  nnmord  8642  nnawordex  8647  nnaordex2  8649  nnneo  8665  nneob  8666  omopth  8672  nnasmo  8673  ereq1  8724  eqerlem  8752  qsdisj  8806  erov  8826  eceqoveq  8834  mapsnd  8898  endisj  9070  pw2f1olem  9088  enfixsn  9093  disjenex  9147  domssex2  9149  xpf1o  9151  mapxpen  9155  unxpdomlem2  9257  enp1ilem  9282  fodomfib  9339  fodomfibOLD  9341  fipreima  9368  opthreg  9630  cantnfp1lem3  9692  ssttrcl  9727  ttrcltr  9728  ttrclss  9732  ttrclselem2  9738  frmin  9761  updjud  9946  pm54.43  10013  dfac5  10141  dfacacn  10154  kmlem9  10171  cfeq0  10268  cfss  10277  cfslb  10278  fin23lem22  10339  fin23lem12  10343  fin23lem19  10348  fin23lem30  10354  fin23lem33  10357  fin1a2lem6  10417  axcc2lem  10448  axdc3lem2  10463  axdc3lem3  10464  axdc3lem4  10465  axdc3  10466  axdc4lem  10467  zorn2lem7  10514  ttukeylem3  10523  ttukeylem6  10526  ttukey2g  10528  fodomb  10538  axacndlem5  10623  fpwwe2cbv  10642  fpwwe2lem2  10644  fpwwe2lem3  10645  fpwwe2lem11  10653  fpwwe2lem12  10654  fpwwe  10658  pwfseqlem2  10671  pwxpndom2  10677  addnidpi  10913  ltexpi  10914  recmulnq  10976  ltexnq  10987  halfnq  10988  archnq  10992  ltexpri  11055  recexpr  11063  addsrpr  11087  mulsrpr  11088  00sr  11111  negexsr  11114  recexsrlem  11115  recexsr  11119  axrnegex  11174  axrrecex  11175  00id  11408  mul02  11411  addrid  11413  cnegex  11414  cnegex2  11415  subval  11471  subadd  11483  subadd2  11484  subsub23  11485  addsubeq4  11495  subcan2  11506  negcon1  11533  subcan  11536  addrsub  11652  ltordlem  11760  ltord1  11761  recex  11867  mul0or  11875  muleqadd  11879  receu  11880  mulcan1g  11888  divval  11896  divmul  11897  rec11  11937  ldiv  12073  rdiv  12074  zdiv  12661  uzin  12890  xaddval  13237  xmulval  13239  xnn0xadd0  13261  xnegdi  13262  ioo0  13385  ico0  13406  ioc0  13407  icc0  13408  1fv  13662  fzon  13695  fvinim0ffz  13800  flbi  13831  mod0  13891  modmuladdnn0  13931  modirr  13958  addmodlteq  13962  uzrdgfni  13974  axdc4uzlem  13999  fsuppmapnn0fiubex  14008  mptnn0fsupp  14013  seqid  14063  seqz  14066  expval  14079  expeq0  14108  sqeqor  14232  nn0opth2  14288  hashdom  14395  elprchashprn2  14412  hashbc  14469  hashf1lem1  14471  hash2pwpr  14492  ccat0  14592  wrdl1s1  14630  ccatws1lenp1b  14637  pfxsuff1eqwrdeq  14715  swrdccatin2  14745  pfxccatin12lem2  14747  2cshwcshw  14842  scshwfzeqfzo  14843  cshimadifsn  14846  cshimadifsn0  14847  s2f1o  14933  wrdlen2i  14959  2swrd2eqwrdeq  14970  wwlktovf  14973  wwlktovf1  14974  wwlktovfo  14975  wrd2f1tovbij  14977  relexp0g  15039  relexpsucnnr  15042  dfrtrcl2  15079  mulre  15138  rennim  15256  cnpart  15257  01sqrex  15266  resqrex  15267  sqrmo  15268  resqrtcl  15270  resqrtthlem  15271  sqrtgt0  15275  sqrtneg  15284  sqrtsq2  15285  absmod0  15320  sqreulem  15376  sqreu  15377  sqrtthlem  15379  eqsqrtd  15384  reusq0  15479  fsum00  15812  telfsumo  15816  prodss  15961  fprodle  16010  tanaddlem  16182  absefib  16214  efieq1re  16215  divides  16272  dvdsval2  16273  nndivides  16280  dvds0lem  16284  dvds1lem  16285  dvds2lem  16286  negdvdsb  16290  muldvds1  16298  muldvds2  16299  dvdscmulr  16302  dvdsmulcr  16303  dvdstr  16311  dvdsabseq  16330  divconjdvds  16332  odd2np1lem  16357  odd2np1  16358  even2n  16359  oddm1even  16360  2tp1odd  16369  opeo  16382  omeo  16383  m1exp1  16393  divalglem4  16413  divalglem8  16417  divalgb  16421  bitsuz  16491  smupvallem  16500  gcdaddmlem  16541  gcdabs1  16546  bezoutlem3  16558  rplpwr  16575  rprpwr  16576  alginv  16592  algcvga  16596  algfx  16597  eucalgval2  16598  coprmdvds  16670  qredeq  16674  qredeu  16675  coprmprod  16678  coprmproddvdslem  16679  divgcdcoprm0  16682  divgcdcoprmex  16683  cncongr1  16684  rpexp  16739  rpexp12i  16741  cncongrprm  16746  qnumdenbi  16761  phival  16784  phicl2  16785  dfphi2  16791  phiprmpw  16793  phimullem  16796  eulerthlem1  16798  eulerthlem2  16799  eulerth  16800  fermltl  16801  hashgcdlem  16805  phisum  16808  odzval  16809  odzdvds  16813  reumodprminv  16822  modprm0  16823  nnnn0modprm0  16824  modprmn0modprm0  16825  coprimeprodsq  16826  coprimeprodsq2  16827  pythagtriplem2  16835  pythagtrip  16852  pcval  16862  pceulem  16863  pcqmul  16871  pcqcl  16874  pcabs  16893  pcgcd1  16895  pc2dvds  16897  pcaddlem  16906  pcadd  16907  pcmpt  16910  prmpwdvds  16922  pockthi  16925  unbenlem  16926  4sqlem12  16974  ramz  17043  ramcl  17047  cshwrepswhash1  17120  imasval  17523  fvprif  17573  iscat  17682  iscatd  17683  catidex  17684  catideu  17685  cidfval  17686  cidval  17687  catidd  17690  catlid  17693  catrid  17694  catpropd  17719  cidpropd  17720  issect  17764  dfiso2  17783  invcoisoid  17803  isocoinvid  17804  setcepi  18099  latleeqj2  18460  latleeqm2  18476  oduclatb  18515  mgmidmo  18636  grpidval  18637  grpidpropd  18638  ismgmid  18641  ismgmid2  18644  mgmidsssn0  18648  grpinvalem  18649  grprida  18651  gsumvalx  18652  gsumpropd  18654  gsumpropd2lem  18655  gsumress  18658  gsumval2  18662  ismnddef  18712  sgrpidmnd  18715  ismndd  18732  mndpropd  18735  mndinvmod  18740  mnd1  18755  ismhm  18761  gsumvallem2  18810  frmdgsum  18838  frmdup3  18843  efmndmnd  18865  smndex1mnd  18886  sgrp2rid2  18902  sgrp2rid2ex  18903  pwmnd  18913  grpinvex  18924  isgrpd2  18937  isgrpd  18939  dfgrp2  18943  grpinveu  18955  grpinvval  18961  grplinv  18970  isgrpinv  18974  grplrinv  18977  grpidinv2  18978  grpidinv  18979  grplmulf1o  18994  grpraddf1o  18995  grpsubeq0  19007  grpsubadd  19009  dfgrp3lem  19019  dfgrp3  19020  grp1  19028  imasgrp2  19036  qusgrp2  19039  mhmmnd  19045  ghmgrp  19047  mulgval  19052  mulgaddcom  19079  eqg0el  19164  cycsubmel  19181  ghmeqker  19224  ghmf1  19227  conjnmzb  19234  ghmqusker  19268  isga  19272  subgga  19281  gaorb  19288  gaorber  19289  gastacl  19290  gastacos  19291  orbsta  19294  symgfix2  19395  gsmsymgrfixlem1  19406  gsmsymgrfix  19407  gsmsymgreq  19411  symgfixelq  19412  f1omvdconj  19425  pmtrdifwrdel2  19465  psgnunilem1  19472  psgnunilem2  19474  psgnunilem3  19475  psgnunilem4  19476  odval  19513  odid  19517  odlem2  19518  oddvdsnn0  19523  odnncl  19524  oddvds  19526  odcong  19528  odeq  19529  odmulgid  19533  odmulgeq  19536  gexval  19557  gexid  19560  gexlem2  19561  gexdvdsi  19562  gexdvds  19563  subgpgp  19576  sylow1lem1  19577  sylow1lem4  19580  sylow2alem1  19596  sylow2alem2  19597  sylow2blem2  19600  sylow3lem6  19611  lsmdisj3a  19668  lsmdisj3b  19669  pj1val  19674  pj1eq  19679  efgredlemd  19723  efgredlem  19726  efgred  19727  efgrelexlema  19728  frgpup3  19757  ablsubadd  19788  ablsubsub23  19803  iscyggen  19859  cyggenod  19863  gsumval3lem2  19885  gsumval3  19886  gsummptnn0fz  19965  dmdprd  19979  dprddisj  19990  dprdfeq0  20003  dprdf11  20004  dmdprdpr  20030  dpjeq  20040  ablfacrp  20047  pgpfac1lem2  20056  pgpfac1lem3  20058  pgpfac1lem5  20060  pgpfac1  20061  pgpfaclem1  20062  pgpfaclem2  20063  pgpfaclem3  20064  ablfaclem2  20067  ablfaclem3  20068  ablfac2  20070  rngmneg1  20125  rngmneg2  20126  ringurd  20143  srgrz  20165  srglz  20166  srgisid  20167  srg1zr  20173  ringid  20232  qusring2  20292  opprring  20305  dvdsrval  20319  dvdsrmul  20322  dvdsr01  20329  dvdsr02  20330  crngunit  20336  ringunitnzdiv  20356  dvreq1  20369  dvdsrpropd  20374  irredn0  20381  irredrmul  20385  irredmul  20387  rngisomring  20425  rhmdvdsr  20466  lringuplu  20502  subrg1  20540  subrgdvds  20544  isrrg  20656  rrgeq0i  20657  rrgeq0  20658  domneq0  20666  isdomn4  20674  domnlcanb  20678  domnrcanb  20680  drngid2  20710  drngmul0orOLD  20719  isdrngd  20723  isdrngdOLD  20725  fidomndrnglem  20730  isabv  20769  issrngd  20813  islmod  20819  islmodd  20821  lmodprop2d  20879  mptscmfsupp0  20882  lss1d  20918  lspextmo  21012  lvecvs0or  21067  lvecvscan  21070  lvecvscan2  21071  lbsacsbs  21115  rngqiprngimf1lem  21253  rng2idl1cntr  21264  prmirredlem  21431  pzriprnglem7  21446  pzriprnglem13  21452  chrdvds  21485  chrnzr  21489  domnchr  21491  znval  21494  zncyg  21507  znfld  21519  znunit  21522  znrrg  21524  frgpcyg  21532  psgndiflemB  21558  psgndiflemA  21559  ipeq0  21596  ip2eq  21611  elocv  21626  ocvi  21627  obsne0  21683  dsmmacl  21699  dsmmlss  21702  frlmphl  21739  frlmup4  21759  islindf4  21796  islindf5  21797  mplsubrglem  21962  mplmon2  22017  evlslem1  22038  evlseu  22039  evlsval  22042  evlsval2  22043  ismhp3  22078  mhpsclcl  22083  mhpvarcl  22084  mhpmulcl  22085  psdmul  22102  psdmvr  22105  cply1coe0bi  22238  gsummoncoe1  22244  evl1vsd  22280  dmatel  22429  dmatelnd  22432  dmatmulcl  22436  scmateALT  22448  mdetdiaglem  22534  mdetunilem1  22548  mdetunilem3  22550  mdetunilem4  22551  mdetunilem9  22556  symgmatr01lem  22589  symgmatr01  22590  gsummatr01lem1  22591  gsummatr01lem4  22594  gsummatr01  22595  smadiadetlem3  22604  cramerlem3  22625  pmatcoe1fsupp  22637  cpmatel  22647  1elcpmat  22651  cpmatmcllem  22654  cpmatmcl  22655  d1mat2pmat  22675  m2cpminvid2lem  22690  m2cpminvid2  22691  decpmatmulsumfsupp  22709  pmatcollpw2lem  22713  pmatcollpwscmatlem1  22725  mp2pm2mplem4  22745  pm2mpmhmlem1  22754  chpscmat  22778  cpmidpmatlem3  22808  cayleyhamilton0  22825  cayleyhamiltonALT  22827  cayleyhamilton1  22828  0ntr  23007  ntreq0  23013  cldlp  23086  pnrmopn  23279  hausnei2  23289  cnhaus  23290  nrmsep  23293  isnrm2  23294  regsep2  23312  dishaus  23318  ordthauslem  23319  iscmp  23324  cmpsublem  23335  cmpsub  23336  tgcmp  23337  sscmp  23341  hauscmplem  23342  cmpfi  23344  bwth  23346  connsuba  23356  nconnsubb  23359  isref  23445  islocfin  23453  elpt  23508  elptr  23509  pthaus  23574  txcmp  23579  hausdiag  23581  txhaus  23583  txkgen  23588  xkohaus  23589  xkococnlem  23595  regr1lem  23675  fbasrn  23820  fmfnfmlem3  23892  flimtopon  23906  fclstopon  23948  alexsubb  23982  symgtgp  24042  qustgpopn  24056  qustgphaus  24059  ustuqtop  24183  isusp  24198  ispsmet  24241  psmet0  24245  ismet  24260  isxmet  24261  xmeteq0  24275  metn0  24297  xmetres2  24298  imasf1oxmet  24312  xblss2ps  24338  xblss2  24339  xmseq0  24401  comet  24450  stdbdxmet  24452  methaus  24457  dscmet  24509  nrmmetd  24511  nmeq0  24555  tngngp  24591  tngngp3  24593  nlmmul0or  24620  cnmet  24708  xrsxmet  24747  metnrmlem3  24799  icopnfcnv  24889  iccpnfcnv  24891  ishtpy  24920  isphtpy  24929  phtpyi  24932  om1elbas  24981  elpi1i  24995  pi1grplem  24998  isclmp  25046  cphsqrtcl2  25136  tcphcph  25187  bcth3  25281  rrxcph  25342  rrxmet  25358  ivth2  25406  iundisj2  25500  dyaddisj  25547  volivth  25558  mbfinf  25616  i1f1lem  25640  i1fmullem  25645  i1fmulclem  25653  i1fres  25656  itg1climres  25665  mbfi1fseqlem4  25669  dvnres  25883  dvcobr  25899  dvcobrOLD  25900  rolle  25944  cmvth  25945  cmvthOLD  25946  deg1leb  26050  ismon1p  26098  q1peqb  26111  dvdsr1p  26119  ply1remlem  26120  fta1glem2  26124  idomrootle  26128  elply2  26151  ne0p  26162  coeeu  26180  coelem  26181  coeeq  26182  dgrle  26198  coeaddlem  26204  plymul0or  26238  ofmulrt  26239  plydivlem3  26253  plydivlem4  26254  plydivex  26255  plydiveu  26256  plydivalg  26257  quotlem  26258  plyremlem  26262  quotcan  26267  plyexmo  26271  elqaalem3  26279  qaa  26281  iaa  26283  aareccl  26284  aacjcl  26285  aannenlem2  26287  reeff1o  26407  sineq0  26483  coseq1  26484  efeq1  26487  recosf1o  26494  logeftb  26542  cosarg0d  26568  logtayl  26619  cxpval  26623  cxpeq0  26637  root1eq1  26715  cxpeq  26717  logbgcd1irr  26754  angrtmuld  26768  affineequiv  26783  affineequiv3  26785  angpieqvdlem2  26789  quad2  26799  dcubic1lem  26803  dcubic2  26804  dcubic  26806  mcubic  26807  cubic2  26808  dquartlem1  26811  dquart  26813  quart  26821  atandm2  26837  atandm4  26839  atantan  26883  wilthlem2  27029  wilthlem3  27030  muval2  27094  isnsqf  27095  mumullem2  27140  sqff1o  27142  muinv  27153  mpodvdsmulf1o  27154  dvdsmulf1o  27156  dchrelbas2  27198  dchrmullid  27213  dchrfi  27216  lgsval  27262  lgsdir  27293  lgsne0  27296  lgsprme0  27300  lgsdirnn0  27305  lgsqrlem1  27307  lgsqr  27312  gausslemma2dlem0c  27319  gausslemma2dlem0i  27325  gausslemma2dlem7  27334  gausslemma2d  27335  lgseisenlem2  27337  lgsquadlem1  27341  lgsquadlem2  27342  lgsquad2lem2  27346  lgsquad3  27348  m1lgs  27349  2lgs  27368  2sqlem7  27385  2sqlem8  27387  2sqlem9  27388  2sqlem11  27390  2sq  27391  2sq2  27394  2sqmo  27398  addsq2reu  27401  addsqn2reu  27402  addsqrexnreu  27403  addsqnreup  27404  addsq2nreurex  27405  2sqreulem1  27407  2sqreultlem  27408  2sqreunnlem1  27410  2sqreunnltlem  27411  2sqreulem4  27415  2sqreuop  27423  2sqreuopnn  27424  2sqreuoplt  27425  2sqreuopltb  27426  2sqreuopnnlt  27427  2sqreuopnnltb  27428  2sqreuopb  27429  dchrisumlem1  27450  dchrvmaeq0  27465  dchrisum0re  27474  ostth3  27599  sltval  27609  nosepssdm  27648  nosupprefixmo  27662  noinfprefixmo  27663  nosupcbv  27664  nosupdm  27666  nosupfv  27668  nosupres  27669  nosupbnd1lem1  27670  nosupbnd1lem3  27672  nosupbnd1lem5  27674  noinfcbv  27679  noinfdm  27681  noinffv  27683  noinfres  27684  noinfbnd1lem3  27687  noinfbnd1lem5  27689  eqscut  27767  scutbdaylt  27780  made0  27829  madecut  27838  negsid  27990  negsex  27992  subadds  28017  divsmo  28127  muls0ord  28128  divsval  28132  norecdiv  28133  divsmulw  28135  divs1  28146  precsexlem8  28155  precsexlem9  28156  precsexlem11  28158  precsex  28159  recsex  28160  abssor  28187  elons  28193  noseqrdgfn  28229  n0seo  28322  zseo  28323  nohalf  28324  expsne0  28331  renegscl  28347  istrkg3ld  28386  axtgcgrid  28388  axtgsegcon  28389  axtg5seg  28390  axtgupdim2  28396  tgjustc1  28400  tgjustc2  28401  iscgrg  28437  isismt  28459  legov  28510  legov2  28511  hlcgreu  28543  mirreu3  28579  mircgr  28582  mirbtwn  28583  ismir  28584  mireq  28590  ismidb  28703  lmiopp  28727  dfcgra2  28755  inaghl  28770  f1otrg  28796  ttgval  28800  ttgelitv  28808  brbtwn  28824  brcgr  28825  colinearalglem2  28832  colinearalg  28835  axsegconlem1  28842  axsegcon  28852  ax5seglem4  28857  ax5seglem5  28858  axpaschlem  28865  axpasch  28866  axlowdimlem16  28882  axeuclidlem  28887  axeuclid  28888  axcontlem2  28890  axcontlem4  28892  axcontlem5  28893  edglnl  29068  usgredg2ALT  29118  usgredgprvALT  29120  usgrnloopvALT  29126  ushgredgedgloop  29156  edg0usgr  29178  nb3grpr  29307  cplgr1v  29355  cusgrsize  29380  vtxdgfval  29393  vtxdeqd  29403  vtxdun  29407  vtxd0nedgb  29414  vtxdusgr0edgnelALT  29422  1loopgrvd2  29429  usgruvtxvdb  29455  usgrvd0nedg  29459  vtxdginducedm1  29469  rusgrpropedg  29510  wksfval  29535  wlklenvclwlk  29581  iswlkon  29583  ispth  29649  dfpth2  29657  upgrwlkdvdelem  29664  crctcshwlkn0lem6  29743  wwlknon  29785  wwlksm1edg  29809  wwlksnextbi  29822  wwlksnextfun  29826  wwlksnextinj  29827  wwlksnextsurj  29828  wwlksnextbij  29830  wlksnwwlknvbij  29836  wwlksnextproplem3  29839  wwlksnextprop  29840  wspn0  29852  umgr2adedgwlkonALT  29875  umgr2adedgspth  29876  umgr2wlkon  29878  rusgrnumwwlkslem  29897  rusgrnumwwlkb0  29899  rusgrnumwwlks  29902  clwlkclwwlklem2a4  29924  clwlknf1oclwwlknlem2  30009  clwlknf1oclwwlkn  30011  isclwwlknon  30018  clwwlknon1loop  30025  s2elclwwlknon2  30031  clwwlknonwwlknonb  30033  clwwlkvbij  30040  uhgr3cyclex  30109  fusgreg2wsplem  30260  fusgr2wsp2nb  30261  fusgreghash2wsp  30265  frrusgrord0  30267  2clwwlkel  30276  extwwlkfab  30279  extwwlkfabel  30280  clwwlknonclwlknonf1o  30289  dlwwlknondlwlknonf1o  30292  wlkl0  30294  numclwwlk2lem1  30303  numclwlk2lem2f  30304  numclwlk2lem2f1o  30306  numclwwlk5  30315  ex-opab  30359  isgrpo  30424  isgrpoi  30425  grpoidinvlem3  30433  grpoideu  30436  gidval  30439  grpoidinv2  30442  grpoinveu  30446  grpoinvval  30450  grpoinv  30452  vciOLD  30488  isvclem  30504  cnidOLD  30509  isnvlem  30537  nvmul0or  30577  imsmetlem  30617  diporthcom  30643  ipz  30646  nmlno0  30722  ajfval  30736  hmoval  30737  isphg  30744  isph  30749  ip2eqi  30783  ajval  30788  hvmul0or  30952  hvsubeq0  30995  hvaddeq0  30996  hvaddcan  30997  hvmulcan  30999  hvmulcan2  31000  hvsubadd  31004  his6  31026  hial0  31029  hial02  31030  hi2eq  31032  orthcom  31035  normlem7tALT  31046  normsub0  31063  normpyth  31072  hilid  31088  hhssnv  31191  ocel  31208  ocsh  31210  ocorth  31218  ocin  31223  occllem  31230  choc0  31253  pjpreeq  31325  omlsi  31331  pjoc1  31361  pjoml  31363  pjoc2  31366  chm0  31418  chocin  31422  chlejb1  31439  chlejb2  31440  chjo  31442  h1deoi  31476  h1de2i  31480  pjoml6i  31516  pjoml2  31538  pjoml3  31539  pjch  31621  hodsi  31702  hodid  31719  eigorth  31765  elunop  31799  adjeu  31816  adjval  31817  eigvecval  31823  unopf1o  31843  adj1  31860  adjeq  31862  hmdmadj  31867  lnopeq0i  31934  lnopeqi  31935  lnopeq  31936  lnfn0  31974  riesz4i  31990  riesz4  31991  riesz1  31992  cnlnadjlem3  31996  cnlnadjlem5  31998  cnlnadjeu  32005  cnlnssadj  32007  nmopadjlei  32015  opsqrlem1  32067  hmopidmpji  32079  pjimai  32103  isst  32140  ishst  32141  hstel2  32146  stadd3i  32175  stri  32184  largei  32194  golem2  32199  superpos  32281  sumdmdii  32342  mddmdin0i  32358  opreu2reuALT  32404  difeq  32445  elim2if  32471  disji2f  32504  disjif2  32508  disjxpin  32515  iundisj2f  32517  disjunsn  32521  fmptco1f1o  32557  ofpreima  32589  fnpreimac  32595  ressupprn  32613  curry2ima  32632  preiman0  32633  receqid  32668  xrofsup  32690  iundisj2fi  32720  f1ocnt  32725  fzo0opth  32728  elq2  32736  fprodex01  32750  sgn0bi  32765  ind1a  32782  prodindf  32786  xdivval  32839  xrecex  32840  xreceu  32842  xdivmul  32845  rexdiv  32846  wrdt2ind  32875  mndlrinvb  32966  mndlactfo  32968  mndractfo  32970  mndlactf1o  32971  mndractf1o  32972  gsummpt2d  32989  gsumwun  33005  fzo0pmtrlast  33049  cyc3genpm  33109  cycpmconjslem2  33112  isslmd  33145  slmdlema  33146  urpropd  33173  elrgspnlem4  33186  elrgspnsubrunlem2  33189  erlcl1  33201  erlcl2  33202  erldi  33203  erlbrd  33204  erler  33206  rloccring  33211  domnlcanOLD  33220  isdrng4  33235  fracerl  33246  fracfld  33248  resv1r  33301  islinds5  33328  linds2eq  33342  dvdsruassoi  33345  dvdsruasso  33346  dvdsruasso2  33347  quslsm  33366  rhmimaidl  33393  qsidomlem2  33414  ssdifidllem  33417  ssdifidl  33418  ssdifidlprm  33419  opprqus0g  33451  qsdrngilem  33455  unitmulrprm  33489  1arithidom  33498  1arithufdlem3  33507  1arithufdlem4  33508  ply1dg1rt  33538  r1pid2OLD  33564  lbsdiflsp0  33612  fedgmullem1  33615  fedgmullem2  33616  irngss  33674  irngnzply1lem  33677  ply1annidllem  33681  ply1annnr  33683  minplymindeg  33688  minplyann  33689  minplyirredlem  33690  minplyirred  33691  irngnminplynz  33692  minplyelirng  33695  irredminply  33696  algextdeglem6  33702  algextdeglem7  33703  rtelextdg2lem  33706  fldext2chn  33708  constrsuc  33718  constrsslem  33721  constrconj  33725  constrextdg2lem  33728  constrextdg2  33729  constrlccllem  33733  constrcccllem  33734  constrcbvlem  33735  constrext2chn  33739  constrcon  33754  1smat1  33781  iscref  33821  metidval  33867  metidv  33869  metider  33871  pstmxmet  33874  xrmulc1cn  33907  esumfsup  34047  esumpcvgval  34055  esumcvg  34063  inelsros  34155  diffiunisros  34156  ismeas  34176  isrnmeas  34177  brae  34218  braew  34219  dya2iocuni  34261  elcarsg  34283  eulerpartleme  34341  eulerpartlemv  34342  eulerpartlemb  34346  eulerpartgbij  34350  eulerpartlemr  34352  eulerpartlemgvv  34354  eulerpartlemgh  34356  eulerpartlemn  34359  elprob  34387  ballotlemi  34479  ballotlemi1  34481  ballotlemii  34482  ballotlemsima  34494  ballotlemfrcn0  34508  signsw0g  34534  signswmnd  34535  signstfvc  34552  prodfzo03  34581  reprval  34588  reprsum  34591  reprsuc  34593  reprpmtf1o  34604  axtgupdim2ALTV  34646  brafs  34650  bnj125  34849  bnj154  34855  bnj526  34865  bnj609  34894  bnj893  34905  bnj1321  35004  bnj1491  35034  nummin  35068  subgrwlk  35100  loop1cycl  35105  subfacp1lem3  35150  subfacp1lem5  35152  subfacp1lem6  35153  cnpconn  35198  txpconn  35200  ptpconn  35201  indispconn  35202  connpconn  35203  cvxpconn  35210  cvmscbv  35226  cvmsi  35233  cvmsval  35234  cvmsdisj  35238  cvmsss2  35242  cvmliftmo  35252  cvmliftlem14  35265  cvmliftiota  35269  cvmlift2lem12  35282  cvmlift2lem13  35283  cvmlift2  35284  cvmliftphtlem  35285  cvmlift3lem2  35288  cvmlift3lem4  35290  cvmlift3lem6  35292  cvmlift3lem7  35293  cvmlift3lem9  35295  cvmlift3  35296  snmlval  35299  satffunlem  35369  prv1n  35399  mrsub0  35484  mrsubcn  35487  ismfs  35517  sinccvglem  35640  br6  35720  brbigcup  35862  imageval  35894  funpartlem  35906  dfrdg4  35915  altopthsn  35925  brsegle  36072  rankeq1o  36135  cbviotadavw  36233  subtr  36278  opnbnd  36289  cldbnd  36290  isfne  36303  topfneec  36319  neibastop3  36326  cnndvlem2  36502  bj-imdirval2  37147  bj-imdirid  37150  bj-imdirco  37154  bj-inftyexpiinj  37173  bj-isrvecd  37262  bj-isrvec2  37264  bj-bary1lem1  37275  bj-bary1  37276  finxp00  37366  nlpfvineqsn  37373  pibp19  37378  pibt2  37381  unccur  37573  matunitlindflem2  37587  ptrecube  37590  poimirlem4  37594  poimirlem19  37609  poimirlem23  37613  poimirlem25  37615  poimirlem27  37617  poimirlem28  37618  poimirlem31  37621  poimirlem32  37622  broucube  37624  mblfinlem2  37628  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  mbfresfi  37636  itg2addnclem  37641  itg2addnclem3  37643  itg2addnc  37644  ftc2nc  37672  cover2  37685  sdclem2  37712  fdc  37715  metf1o  37725  istotbnd3  37741  0totbnd  37743  sstotbnd2  37744  equivtotbnd  37748  totbndbnd  37759  prdstotbnd  37764  heibor1  37780  rrnmet  37799  isexid  37817  ismgmOLD  37820  opidonOLD  37822  exidu1  37826  cmpidelt  37829  exidreslem  37847  exidres  37848  exidresid  37849  grpoeqdivid  37851  elghomlem1OLD  37855  grpokerinj  37863  isrngo  37867  isrngod  37868  rngoideu  37873  isgrpda  37925  isdrngo2  37928  isdrngo3  37929  isrngohom  37935  divrngidl  37998  dmnnzd  38045  dmncan1  38046  disjeccnvep  38248  disjressuc2  38352  qsdisjALTV  38579  dmqseqeq1  38607  unidmqseq  38619  disjdmqseq  38769  eldisjlem19  38774  riotasvd  38920  toycom  38937  islshpsm  38944  lshpnel2N  38949  lsatfixedN  38973  islshpat  38981  lcvexchlem4  39001  l1cvpat  39018  lkr0f  39058  lkrsc  39061  lshpkrlem1  39074  lkreqN  39134  isopos  39144  oposlem  39146  opcon2b  39161  cmtbr3N  39218  cvlcvrp  39304  hlrelat5N  39366  cvrval5  39380  cvrat4  39408  3atlem5  39452  2at0mat0  39490  psubclsetN  39901  4atex2  40042  isldil  40075  ltrnu  40086  ltrnid  40100  isdilN  40119  trlnid  40144  cdleme21k  40303  cdleme29b  40340  cdlemefrs29pre00  40360  cdlemefrs29bpre0  40361  cdlemefrs29cpre1  40363  cdleme32fva  40402  cdleme42b  40443  cdleme50ex  40524  cdleme  40525  cdlemg1a  40535  ltrniotaval  40546  cdlemeiota  40550  tendoid0  40790  cdlemksv2  40812  cdlemkuv2  40832  cdlemk36  40878  cdlemk42  40906  cdlemk  40939  tendoex  40940  cdleml3N  40943  cdleml5N  40945  tendospcanN  40988  cdlemm10N  41083  dihffval  41195  dihfval  41196  dihlsscpre  41199  islpolN  41448  mapdhval  41689  mapdheq  41693  hdmap1fval  41761  hdmap1val  41763  hdmap1eq  41766  hdmap1cbv  41767  hdmapval2lem  41796  hdmap11  41813  hdmap14lem2a  41832  hdmap14lem6  41838  hgmapval  41852  hlhillcs  41923  hlhilphllem  41924  aks4d1  42048  isprimroot  42052  mndmolinv  42054  linvh  42055  primrootsunit1  42056  primrootsunit  42057  primrootscoprmpow  42058  primrootscoprbij  42061  primrootlekpowne0  42064  primrootspoweq0  42065  ringexp0nn  42093  aks6d1c5lem1  42095  sticksstones8  42112  sticksstones9  42113  sticksstones10  42114  sticksstones11  42115  sticksstones12a  42116  sticksstones12  42117  sticksstones16  42121  sticksstones17  42122  sticksstones18  42123  sticksstones19  42124  aks6d1c6lem4  42132  aks6d1c6isolem3  42135  rhmqusspan  42144  grpods  42153  unitscyglem1  42154  unitscyglem2  42155  unitscyglem3  42156  unitscyglem5  42158  metakunt6  42169  metakunt15  42178  metakunt16  42179  metakunt27  42190  metakunt28  42191  metakunt32  42195  expeq1d  42320  zdivgd  42333  ef11d  42335  resubval  42357  renegadd  42362  resubeu  42367  resubadd  42369  sn-negex12  42406  addinvcom  42421  sn-mul02  42430  mulgt0con1d  42448  mulgt0con2d  42449  fimgmcyclem  42503  fidomncyc  42505  evlsval3  42529  fsuppind  42560  mhphflem  42566  prjspnfv01  42594  prjspner01  42595  prjspner1  42596  prjcrvval  42602  dffltz  42604  flt4lem7  42629  nna4b4nsq  42630  negexpidd  42652  mzpcompact2lem  42721  eldioph  42728  eldioph2lem1  42730  eldioph2lem2  42731  eldioph2  42732  eldioph2b  42733  eldioph3  42736  diophin  42742  diophun  42743  eq0rabdioph  42746  dvdsrabdioph  42780  eldioph4i  42782  diophren  42783  rabren3dioph  42785  fphpd  42786  pellexlem5  42803  pellexlem6  42804  pellex  42805  pell1qrval  42816  pell14qrval  42818  pell1234qrval  42820  pell1234qrreccl  42824  pell1234qrmulcl  42825  pell1234qrdich  42831  pell14qrdich  42839  pell1qr1  42841  pellqrexplicit  42847  rmxycomplete  42888  jm2.27  42979  rmydioph  42985  rmxdiophlem  42986  rmxdioph  42987  pw2f1ocnv  43008  pwssplit4  43060  elmnc  43107  dgraalem  43116  dgraaub  43119  dgraa0p  43120  mpaaeu  43121  mpaaval  43122  mpaalem  43123  aaitgo  43133  rngunsnply  43140  proot1ex  43167  cantnfresb  43295  tfsconcatfv  43312  tfsconcatb0  43315  tfsconcat0i  43316  tfsconcat0b  43317  tfsconcat00  43318  tfsconcatrev  43319  naddwordnexlem4  43372  sqrtcval  43612  relexpnul  43649  relexpxpnnidm  43674  relexpiidm  43675  trclfvdecomr  43699  rfovcnvf1od  43975  ntrkbimka  44009  ntrk0kbimka  44010  clsk3nimkb  44011  clsk1independent  44017  ntrclsfveq1  44031  ntrclsfveq2  44032  ntrclskb  44040  k0004val  44121  k0004val0  44125  mnringmulrcld  44200  expgrowth  44307  bcc0  44312  relpfrlem  44926  disjinfi  45164  fsumf1of  45551  limsupmnflem  45697  liminfpnfuz  45793  climxlim2lem  45822  coseq0  45841  icccncfext  45864  dvnmptconst  45918  dvnprodlem1  45923  dvnprodlem2  45924  dvnprodlem3  45925  dvnprod  45926  stoweidlem15  45992  stoweidlem31  46008  stoweidlem35  46012  stoweidlem36  46013  stoweidlem37  46014  stoweidlem43  46020  stoweidlem44  46021  stoweidlem46  46023  stoweidlem55  46032  stoweidlem59  46036  dirkerval2  46071  dirkertrigeqlem1  46075  dirkeritg  46079  dirkercncf  46084  fourierdlem2  46086  fourierdlem3  46087  fourierdlem42  46126  fourierdlem48  46131  fourierdlem49  46132  fourierdlem71  46154  fourierdlem112  46195  fourierdlem113  46196  elaa2lem  46210  etransclem11  46222  etransclem24  46235  etransclem26  46237  etransclem28  46239  etransclem35  46246  ioorrnopnxr  46284  salgenval  46298  intsaluni  46306  salgenn0  46308  salgencl  46309  sssalgen  46312  salgenss  46313  salgenuni  46314  issalgend  46315  dfsalgen2  46318  subsaliuncl  46335  sge0f1o  46359  sge0fodjrnlem  46393  ismea  46428  nnfoctbdjlem  46432  iundjiun  46437  isome  46471  caragenel  46472  ovn0lem  46542  ovnsubaddlem1  46547  smflimlem4  46751  smflim  46754  sigarcol  46841  cfsetsnfsetf  47035  cfsetsnfsetfo  47037  fnbrafvb  47131  afv2fv0  47242  readdcnnred  47280  resubcnnred  47281  cndivrenred  47283  ceilbi  47310  minusmodnep2tmod  47330  fargshiftf1  47403  fargshiftfo  47404  ichexmpl2  47432  ichnreuop  47434  ichreuopeq  47435  elsprel  47437  prproropf1olem4  47468  reupr  47484  reuopreuprim  47488  goldbachthlem2  47508  fmtnoprmfac2lem1  47528  fmtnofac2lem  47530  prmdvdsfmtnof1lem2  47547  mod42tp1mod8  47564  lighneallem2  47568  lighneallem3  47569  lighneallem4  47572  proththd  47576  41prothprm  47581  requad01  47583  requad2  47585  dfeven2  47611  dfeven5  47628  dfodd7  47629  fpprel  47690  fppr2odd  47693  fpprwppr  47701  fpprwpprb  47702  nnsum3primesgbe  47754  isubgredg  47827  upgrimpths  47870  ushggricedg  47888  uhgrimisgrgric  47892  isubgr3stgrlem3  47928  isubgr3stgrlem4  47929  isubgr3stgrlem6  47931  grlimgrtrilem2  47955  gpgedgvtx0  48013  gpgedgvtx1  48014  gpgvtxedg0  48015  gpgvtxedg1  48016  gpg3kgrtriexlem5  48037  gpgprismgr4cycllem3  48044  upwlksfval  48058  0nodd  48093  2nodd  48095  nnsgrpnmnd  48101  nn0mnd  48102  lidldomn1  48154  zlidlring  48157  uzlidlring  48158  2zrngamgm  48168  2zrngamnd  48170  2zrngagrp  48172  2zrngnmlid2  48180  ztprmneprm  48270  dmatALTbasel  48326  linindslinci  48372  lindslinindsimp1  48381  lindslinindimp2lem4  48385  lindslinindsimp2lem5  48386  linds0  48389  el0ldep  48390  lindsrng01  48392  snlindsntorlem  48394  snlindsntor  48395  ldepspr  48397  lincresunit3  48405  islindeps2  48407  isldepslvec2  48409  zlmodzxzldep  48428  blen1b  48516  dig2bits  48542  nn0sumshdiglem1  48549  0aryfvalelfv  48563  itcovalsuc  48595  prelrrx2b  48642  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  rrx2linest2  48672  elrrx2linest2  48673  spheres  48674  2sphere  48677  2sphere0  48678  line2ylem  48679  line2  48680  line2xlem  48681  line2x  48682  line2y  48683  itscnhlc0yqe  48687  itschlc0yqe  48688  itscnhlc0xyqsol  48693  itschlc0xyqsol1  48694  itsclc0xyqsolr  48697  itsclc0  48699  itsclc0b  48700  itsclinecirc0b  48702  itsclquadb  48704  itsclquadeu  48705  itscnhlinecirc02p  48713  resinsnALT  48796  sepnsepolem2  48845  sepnsepo  48846  sepfsepc  48850  iscnrm3rlem8  48869  iscnrm3r  48870  iscnrm3llem2  48872  iscnrm3l  48873  oppcendc  48941  isisod  48945  sectpropdlem  48951  ssccatid  48987  resccatlem  48988  imasubc  49039  oppcthinendcALT  49275  functhinclem2  49279  fullthinc2  49285  thincciso  49287  thinccisod  49288  termcpropd  49336  fulltermc2  49345  oduoppcciso  49391  discsnterm  49399  aacllem  49613