Theorem eqeq1d 2754

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 2745	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	biimpi 218	. . 3 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		bibi1 353	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	alimi 1821	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		albi 1828	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)) → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
7	1, 3, 5, 6	4syl 19	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
8		dfcleq 2745	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
9		dfcleq 2745	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
10	7, 8, 9	3bitr4g 316	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1548   = wceq 1550   ∈ wcel 2132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-cleq 2744

This theorem is referenced by:  eqeq1  2756  eqcomd  2758  eqeq2d  2763  eqeqan12d  2766  neeq1d  3006  csbconstg  3862  csbhypf  3871  csbiebt  3872  csbiebg  3875  sbceq2g  4363  csbie2df  4387  disjeq0  4400  disjssun  4412  mosneq  4790  preq12b  4798  preq12bg  4801  elpreqprlem  4814  disji2  5074  invdisjrab  5077  disjprg  5086  disjxun  5088  iin0  5309  opthg  5435  opeqsng  5462  propeqop  5466  wefrc  5630  xpcan  6147  xpcan2  6148  dmsnopg  6185  rnmpt0f  6215  reuop  6265  dfpo2  6268  sspred  6282  onfr  6370  unisucg  6411  nsuceq0  6416  iotaeq  6474  iotabi  6475  fneq1  6597  fnun  6620  fnresdisj  6626  fnimadisj  6638  fnimaeq0  6639  foeq1  6759  fveqeq2d  6860  fvun1  6943  fvmptdv2  6979  fndmdifeq0  7010  fneqeql  7012  dffo3  7068  dffo3f  7072  fnnfpeq0  7147  foeqcnvco  7269  f1eqcocnv  7270  isofrlem  7309  eqfunresadj  7329  ovanraleqv  7405  f1opr  7437  eloprabga  7490  ovmpodv2  7539  ov3  7544  ovelimab  7559  caovcang  7582  caovcan  7585  caovmo  7618  caofinvl  7677  caofid1  7680  caofid2  7681  caofidlcan  7683  caonncan  7689  tfisi  7824  mptcnfimad  7952  oteqimp  7974  br1steqg  7977  br2ndeqg  7978  eqop  7997  reldm  8010  mposn  8066  fparlem1  8075  fparlem2  8076  fsplit  8080  frxp  8090  xporderlem  8091  fnwelem  8095  xpord2lem  8106  xpord3lem  8113  poseq  8122  soseq  8123  fnsuppeq0  8156  suppssov1  8161  suppssov2  8162  suppofss1d  8168  suppofss2d  8169  tposfo2  8213  mpocurryd  8233  iinon  8295  onnseq  8299  tz7.49  8400  seqomlem2  8406  oe0m1  8474  om0r  8492  oe1m  8498  oawordeulem  8507  oawordeu  8508  oarec  8515  omord  8521  oneo  8534  omeu  8538  oeeui  8556  nnm0r  8564  nnmord  8586  nnawordex  8591  nnaordex2  8593  nnneo  8609  nneob  8610  omopth  8616  nnasmo  8617  ereq1  8670  eqerlem  8698  qsdisj  8760  erov  8780  eceqoveq  8788  mapsnd  8853  endisj  9021  pw2f1olem  9038  enfixsn  9043  disjenex  9092  domssex2  9094  xpf1o  9096  mapxpen  9100  unxpdomlem2  9186  enp1ilem  9207  fodomfib  9258  fodomfibOLD  9260  fipreima  9287  opthreg  9559  cantnfp1lem3  9621  ssttrcl  9656  ttrcltr  9657  ttrclss  9661  ttrclselem2  9667  frmin  9693  updjud  9878  pm54.43  9945  dfac5  10071  dfacacn  10084  kmlem9  10101  cfeq0  10199  cfss  10208  cfslb  10209  fin23lem22  10270  fin23lem12  10274  fin23lem19  10279  fin23lem30  10285  fin23lem33  10288  fin1a2lem6  10348  axcc2lem  10379  axdc3lem2  10394  axdc3lem3  10395  axdc3lem4  10396  axdc3  10397  axdc4lem  10398  zorn2lem7  10445  ttukeylem3  10454  ttukeylem6  10457  ttukey2g  10459  fodomb  10469  axacndlem5  10555  fpwwe2cbv  10574  fpwwe2lem2  10576  fpwwe2lem3  10577  fpwwe2lem11  10585  fpwwe2lem12  10586  fpwwe  10590  pwfseqlem2  10603  pwxpndom2  10609  addnidpi  10845  ltexpi  10846  recmulnq  10908  ltexnq  10919  halfnq  10920  archnq  10924  ltexpri  10987  recexpr  10995  addsrpr  11019  mulsrpr  11020  00sr  11043  negexsr  11046  recexsrlem  11047  recexsr  11051  axrnegex  11106  axrrecex  11107  00id  11344  mul02  11347  addrid  11349  cnegex  11350  cnegex2  11351  subval  11407  subadd  11419  subadd2  11420  subsub23  11421  addsubeq4  11431  subcan2  11442  negcon1  11469  subcan  11472  addrsub  11590  ltordlem  11698  ltord1  11699  recex  11805  mul0or  11813  muleqadd  11817  receu  11818  mulcan1g  11826  divval  11833  divmul  11834  rec11  11875  ldiv  12011  rdiv  12012  ind1a  12192  zdiv  12629  uzin  12861  xaddval  13212  xmulval  13214  xnn0xadd0  13236  xnegdi  13237  ioo0  13360  ico0  13381  ioc0  13382  icc0  13383  1fv  13638  fzon  13672  fvinim0ffz  13781  flbi  13812  mod0  13872  modmuladdnn0  13914  modirr  13941  addmodlteq  13945  uzrdgfni  13957  axdc4uzlem  13982  fsuppmapnn0fiubex  13991  mptnn0fsupp  13996  seqid  14046  seqz  14049  expval  14062  expeq0  14091  sqeqor  14215  nn0opth2  14271  hashdom  14378  elprchashprn2  14395  hashbc  14452  hashf1lem1  14454  hash2pwpr  14475  ccat0  14575  wrdl1s1  14614  ccatws1lenp1b  14621  pfxsuff1eqwrdeq  14698  swrdccatin2  14728  pfxccatin12lem2  14730  2cshwcshw  14824  scshwfzeqfzo  14825  cshimadifsn  14828  cshimadifsn0  14829  s2f1o  14915  wrdlen2i  14941  2swrd2eqwrdeq  14952  wwlktovf  14955  wwlktovf1  14956  wwlktovfo  14957  wrd2f1tovbij  14959  relexp0g  15021  relexpsucnnr  15024  dfrtrcl2  15061  mulre  15120  rennim  15238  cnpart  15239  01sqrex  15248  resqrex  15249  sqrmo  15250  resqrtcl  15252  resqrtthlem  15253  sqrtgt0  15257  sqrtneg  15266  sqrtsq2  15267  absmod0  15302  sqreulem  15359  sqreu  15360  sqrtthlem  15362  eqsqrtd  15367  reusq0  15464  fsum00  15798  telfsumo  15802  prodss  15949  fprodle  15998  tanaddlem  16170  absefib  16202  efieq1re  16203  divides  16260  dvdsval2  16261  nndivides  16268  dvds0lem  16272  dvds1lem  16273  dvds2lem  16274  negdvdsb  16278  muldvds1  16286  muldvds2  16287  dvdscmulr  16290  dvdsmulcr  16291  difmod0  16293  dvdstr  16300  dvdsabseq  16319  divconjdvds  16321  odd2np1lem  16346  odd2np1  16347  even2n  16348  oddm1even  16349  2tp1odd  16358  opeo  16371  omeo  16372  m1exp1  16382  divalglem4  16402  divalglem8  16406  divalgb  16410  bitsuz  16480  smupvallem  16489  gcdaddmlem  16530  gcdabs1  16535  bezoutlem3  16547  rplpwr  16564  rprpwr  16565  alginv  16581  algcvga  16585  algfx  16586  eucalgval2  16587  coprmdvds  16659  qredeq  16663  qredeu  16664  coprmprod  16667  coprmproddvdslem  16668  divgcdcoprm0  16671  divgcdcoprmex  16672  cncongr1  16673  rpexp  16729  rpexp12i  16731  cncongrprm  16736  qnumdenbi  16751  phival  16774  phicl2  16775  dfphi2  16781  phiprmpw  16783  phimullem  16786  eulerthlem1  16788  eulerthlem2  16789  eulerth  16790  fermltl  16791  hashgcdlem  16795  phisum  16798  odzval  16799  odzdvds  16803  reumodprminv  16812  modprm0  16813  nnnn0modprm0  16814  modprmn0modprm0  16815  coprimeprodsq  16816  coprimeprodsq2  16817  pythagtriplem2  16825  pythagtrip  16842  pcval  16852  pceulem  16853  pcqmul  16861  pcqcl  16864  pcabs  16883  pcgcd1  16885  pc2dvds  16887  pcaddlem  16896  pcadd  16897  pcmpt  16900  prmpwdvds  16912  pockthi  16915  unbenlem  16916  4sqlem12  16964  ramz  17033  ramcl  17037  cshwrepswhash1  17110  imasval  17513  fvprif  17563  iscat  17676  iscatd  17677  catidex  17678  catideu  17679  cidfval  17680  cidval  17681  catidd  17684  catlid  17687  catrid  17688  catpropd  17713  cidpropd  17714  issect  17758  dfiso2  17777  invcoisoid  17797  isocoinvid  17798  setcepi  18093  latleeqj2  18456  latleeqm2  18472  oduclatb  18511  mgmidmo  18666  grpidval  18667  grpidpropd  18668  ismgmid  18671  ismgmid2  18674  mgmidsssn0  18678  grpinvalem  18679  grprida  18681  gsumvalx  18682  gsumpropd  18684  gsumpropd2lem  18685  gsumress  18688  gsumval2  18692  ismnddef  18742  sgrpidmnd  18745  ismndd  18762  mndpropd  18765  mndinvmod  18770  mnd1  18785  ismhm  18791  gsumvallem2  18840  frmdgsum  18868  frmdup3  18873  efmndmnd  18895  smndex1mnd  18919  sgrp2rid2  18935  sgrp2rid2ex  18936  pwmnd  18946  grpinvex  18957  isgrpd2  18970  isgrpd  18972  dfgrp2  18976  grpinveu  18988  grpinvval  18994  grplinv  19003  isgrpinv  19007  grplrinv  19010  grpidinv2  19011  grpidinv  19012  grplmulf1o  19027  grpraddf1o  19028  grpsubeq0  19040  grpsubadd  19042  dfgrp3lem  19052  dfgrp3  19053  grp1  19061  imasgrp2  19069  qusgrp2  19072  mhmmnd  19078  ghmgrp  19080  mulgval  19085  mulgaddcom  19112  eqg0el  19196  cycsubmel  19213  ghmeqker  19255  ghmf1  19258  conjnmzb  19265  ghmqusker  19299  isga  19303  subgga  19312  gaorb  19319  gaorber  19320  gastacl  19321  gastacos  19322  orbsta  19325  symgfix2  19428  gsmsymgrfixlem1  19439  gsmsymgrfix  19440  gsmsymgreq  19444  symgfixelq  19445  f1omvdconj  19458  pmtrdifwrdel2  19498  psgnunilem1  19505  psgnunilem2  19507  psgnunilem3  19508  psgnunilem4  19509  odval  19546  odid  19550  odlem2  19551  oddvdsnn0  19556  odnncl  19557  oddvds  19559  odcong  19561  odeq  19562  odmulgid  19566  odmulgeq  19569  gexval  19590  gexid  19593  gexlem2  19594  gexdvdsi  19595  gexdvds  19596  subgpgp  19609  sylow1lem1  19610  sylow1lem4  19613  sylow2alem1  19629  sylow2alem2  19630  sylow2blem2  19633  sylow3lem6  19644  lsmdisj3a  19701  lsmdisj3b  19702  pj1val  19707  pj1eq  19712  efgredlemd  19756  efgredlem  19759  efgred  19760  efgrelexlema  19761  frgpup3  19790  ablsubadd  19821  ablsubsub23  19836  iscyggen  19892  cyggenod  19896  gsumval3lem2  19918  gsumval3  19919  gsummptnn0fz  19998  dmdprd  20012  dprddisj  20023  dprdfeq0  20036  dprdf11  20037  dmdprdpr  20063  dpjeq  20073  ablfacrp  20080  pgpfac1lem2  20089  pgpfac1lem3  20091  pgpfac1lem5  20093  pgpfac1  20094  pgpfaclem1  20095  pgpfaclem2  20096  pgpfaclem3  20097  ablfaclem2  20100  ablfaclem3  20101  ablfac2  20103  rngmneg1  20185  rngmneg2  20186  ringurd  20203  srgrz  20225  srglz  20226  srgisid  20227  srg1zr  20233  ringid  20292  qusring2  20351  opprring  20364  dvdsrval  20378  dvdsrmul  20381  dvdsr01  20388  dvdsr02  20389  crngunit  20395  ringunitnzdiv  20415  dvreq1  20428  dvdsrpropd  20433  irredn0  20440  irredrmul  20444  irredmul  20446  rngisomring  20484  rhmdvdsr  20526  lringuplu  20562  subrg1  20600  subrgdvds  20604  isrrg  20716  rrgeq0i  20717  rrgeq0  20718  domneq0  20726  isdomn4  20734  domnlcanb  20738  domnrcanb  20740  drngid2  20770  drngmul0orOLD  20779  isdrngd  20783  isdrngdOLD  20785  fidomndrnglem  20790  isabv  20829  issrngd  20873  islmod  20900  islmodd  20902  lmodprop2d  20960  mptscmfsupp0  20963  lss1d  20999  lspextmo  21092  lvecvs0or  21147  lvecvscan  21150  lvecvscan2  21151  lbsacsbs  21195  rngqiprngimf1lem  21333  rng2idl1cntr  21344  prmirredlem  21493  pzriprnglem7  21508  pzriprnglem13  21514  chrdvds  21547  chrnzr  21551  domnchr  21553  znval  21556  zncyg  21569  znfld  21581  znunit  21584  znrrg  21586  frgpcyg  21594  psgndiflemB  21621  psgndiflemA  21622  ipeq0  21659  ip2eq  21674  elocv  21689  ocvi  21690  obsne0  21746  dsmmacl  21762  dsmmlss  21765  frlmphl  21802  frlmup4  21822  islindf4  21859  islindf5  21860  mplsubrglem  22024  mplmon2  22083  evlslem1  22104  evlseu  22105  evlsval  22108  evlsval2  22109  evlsval3  22111  ismhp3  22176  mhpsclcl  22181  mhpvarcl  22182  mhpmulcl  22183  psdmul  22200  psdmvr  22203  cply1coe0bi  22334  gsummoncoe1  22340  evl1vsd  22376  dmatel  22522  dmatelnd  22525  dmatmulcl  22529  scmateALT  22541  mdetdiaglem  22627  mdetunilem1  22641  mdetunilem3  22643  mdetunilem4  22644  mdetunilem9  22649  symgmatr01lem  22682  symgmatr01  22683  gsummatr01lem1  22684  gsummatr01lem4  22687  gsummatr01  22688  smadiadetlem3  22697  cramerlem3  22718  pmatcoe1fsupp  22730  cpmatel  22740  1elcpmat  22744  cpmatmcllem  22747  cpmatmcl  22748  d1mat2pmat  22768  m2cpminvid2lem  22783  m2cpminvid2  22784  decpmatmulsumfsupp  22802  pmatcollpw2lem  22806  pmatcollpwscmatlem1  22818  mp2pm2mplem4  22838  pm2mpmhmlem1  22847  chpscmat  22871  cpmidpmatlem3  22901  cayleyhamilton0  22918  cayleyhamiltonALT  22920  cayleyhamilton1  22921  0ntr  23100  ntreq0  23106  cldlp  23179  pnrmopn  23372  hausnei2  23382  cnhaus  23383  nrmsep  23386  isnrm2  23387  regsep2  23405  dishaus  23411  ordthauslem  23412  iscmp  23417  cmpsublem  23428  cmpsub  23429  tgcmp  23430  sscmp  23434  hauscmplem  23435  cmpfi  23437  bwth  23439  connsuba  23449  nconnsubb  23452  isref  23538  islocfin  23546  elpt  23601  elptr  23602  pthaus  23667  txcmp  23672  hausdiag  23674  txhaus  23676  txkgen  23681  xkohaus  23682  xkococnlem  23688  regr1lem  23768  fbasrn  23913  fmfnfmlem3  23985  flimtopon  23999  fclstopon  24041  alexsubb  24075  symgtgp  24135  qustgpopn  24149  qustgphaus  24152  ustuqtop  24275  isusp  24290  ispsmet  24333  psmet0  24337  ismet  24352  isxmet  24353  xmeteq0  24367  metn0  24389  xmetres2  24390  imasf1oxmet  24404  xblss2ps  24430  xblss2  24431  xmseq0  24493  comet  24542  stdbdxmet  24544  methaus  24549  dscmet  24601  nrmmetd  24603  nmeq0  24647  tngngp  24683  tngngp3  24685  nlmmul0or  24712  cnmet  24800  xrsxmet  24839  metnrmlem3  24891  icopnfcnv  24973  iccpnfcnv  24975  ishtpy  25003  isphtpy  25012  phtpyi  25015  om1elbas  25063  elpi1i  25077  pi1grplem  25080  isclmp  25128  cphsqrtcl2  25217  tcphcph  25268  bcth3  25362  rrxcph  25423  rrxmet  25439  ivth2  25486  iundisj2  25580  dyaddisj  25627  volivth  25638  mbfinf  25696  i1f1lem  25720  i1fmullem  25725  i1fmulclem  25733  i1fres  25736  itg1climres  25745  mbfi1fseqlem4  25749  dvnres  25962  dvcobr  25977  rolle  26021  cmvth  26022  deg1leb  26124  ismon1p  26172  q1peqb  26185  dvdsr1p  26193  ply1remlem  26194  fta1glem2  26198  idomrootle  26202  elply2  26225  ne0p  26236  coeeu  26254  coelem  26255  coeeq  26256  dgrle  26272  coeaddlem  26278  plymul0or  26311  ofmulrt  26312  plydivlem3  26325  plydivlem4  26326  plydivex  26327  plydiveu  26328  plydivalg  26329  quotlem  26330  plyremlem  26334  quotcan  26339  plyexmo  26343  elqaalem3  26351  qaa  26353  iaa  26355  aareccl  26356  aacjcl  26357  aannenlem2  26359  reeff1o  26476  sineq0  26555  coseq1  26556  efeq1  26559  recosf1o  26566  logeftb  26614  cosarg0d  26640  logtayl  26691  cxpval  26695  cxpeq0  26709  root1eq1  26786  cxpeq  26788  logbgcd1irr  26825  angrtmuld  26839  affineequiv  26854  affineequiv3  26856  angpieqvdlem2  26860  quad2  26870  dcubic1lem  26874  dcubic2  26875  dcubic  26877  mcubic  26878  cubic2  26879  dquartlem1  26882  dquart  26884  quart  26892  atandm2  26908  atandm4  26910  atantan  26954  wilthlem2  27099  wilthlem3  27100  muval2  27164  isnsqf  27165  mumullem2  27210  sqff1o  27212  muinv  27223  mpodvdsmulf1o  27224  dvdsmulf1o  27226  dchrelbas2  27267  dchrmullid  27282  dchrfi  27285  lgsval  27331  lgsdir  27362  lgsne0  27365  lgsprme0  27369  lgsdirnn0  27374  lgsqrlem1  27376  lgsqr  27381  gausslemma2dlem0c  27388  gausslemma2dlem0i  27394  gausslemma2dlem7  27403  gausslemma2d  27404  lgseisenlem2  27406  lgsquadlem1  27410  lgsquadlem2  27411  lgsquad2lem2  27415  lgsquad3  27417  m1lgs  27418  2lgs  27437  2sqlem7  27454  2sqlem8  27456  2sqlem9  27457  2sqlem11  27459  2sq  27460  2sq2  27463  2sqmo  27467  addsq2reu  27470  addsqn2reu  27471  addsqrexnreu  27472  addsqnreup  27473  addsq2nreurex  27474  2sqreulem1  27476  2sqreultlem  27477  2sqreunnlem1  27479  2sqreunnltlem  27480  2sqreulem4  27484  2sqreuop  27492  2sqreuopnn  27493  2sqreuoplt  27494  2sqreuopltb  27495  2sqreuopnnlt  27496  2sqreuopnnltb  27497  2sqreuopb  27498  dchrisumlem1  27519  dchrvmaeq0  27534  dchrisum0re  27543  ostth3  27668  ltsval  27677  nosepssdm  27716  nosupprefixmo  27730  noinfprefixmo  27731  nosupcbv  27732  nosupdm  27734  nosupfv  27736  nosupres  27737  nosupbnd1lem1  27738  nosupbnd1lem3  27740  nosupbnd1lem5  27742  noinfcbv  27747  noinfdm  27749  noinffv  27751  noinfres  27752  noinfbnd1lem3  27755  noinfbnd1lem5  27757  eqcuts  27844  cutbdaylt  27857  made0  27922  madecut  27942  negsid  28100  negsex  28102  subadds  28129  divsmo  28243  muls0ord  28244  divsval  28248  norecdiv  28249  recsne0  28251  divmulsw  28252  divs1  28263  precsexlem8  28273  precsexlem9  28274  precsexlem11  28276  precsex  28277  recsex  28278  abssor  28305  elons  28312  noseqrdgfn  28365  bdayn0sf1o  28429  eucliddivs  28435  zsoring  28468  n0seo  28480  zseo  28481  nohalf  28483  expsne0  28495  pw2recs  28497  halfcut  28517  z12negscl  28537  z12zsodd  28541  z12sge0  28542  renegscl  28557  istrkg3ld  28596  axtgcgrid  28598  axtgsegcon  28599  axtg5seg  28600  axtgupdim2  28606  tgjustc1  28610  tgjustc2  28611  iscgrg  28647  isismt  28669  legov  28720  legov2  28721  hlcgreu  28753  mirreu3  28789  mircgr  28792  mirbtwn  28793  ismir  28794  mireq  28800  ismidb  28913  lmiopp  28937  dfcgra2  28965  inaghl  28980  f1otrg  29006  ttgval  29010  ttgelitv  29018  brbtwn  29035  brcgr  29036  colinearalglem2  29043  colinearalg  29046  axsegconlem1  29053  axsegcon  29063  ax5seglem4  29068  ax5seglem5  29069  axpaschlem  29076  axpasch  29077  axlowdimlem16  29093  axeuclidlem  29098  axeuclid  29099  axcontlem2  29101  axcontlem4  29103  axcontlem5  29104  edglnl  29279  usgredg2ALT  29329  usgredgprvALT  29331  usgrnloopvALT  29337  ushgredgedgloop  29367  edg0usgr  29389  nb3grpr  29518  cplgr1v  29566  cusgrsize  29590  vtxdgfval  29603  vtxdeqd  29613  vtxdun  29617  vtxd0nedgb  29624  vtxdusgr0edgnelALT  29632  1loopgrvd2  29639  usgruvtxvdb  29665  usgrvd0nedg  29669  vtxdginducedm1  29679  rusgrpropedg  29720  wksfval  29745  wlklenvclwlk  29789  iswlkon  29791  ispth  29856  dfpth2  29864  upgrwlkdvdelem  29871  crctcshwlkn0lem6  29950  wwlknon  29992  wwlksm1edg  30016  wwlksnextbi  30029  wwlksnextfun  30033  wwlksnextinj  30034  wwlksnextsurj  30035  wwlksnextbij  30037  wlksnwwlknvbij  30043  wwlksnextproplem3  30046  wwlksnextprop  30047  wspn0  30059  umgr2adedgwlkonALT  30082  umgr2adedgspth  30083  umgr2wlkon  30085  rusgrnumwwlkslem  30107  rusgrnumwwlkb0  30109  rusgrnumwwlks  30112  clwlkclwwlklem2a4  30134  clwlknf1oclwwlknlem2  30219  clwlknf1oclwwlkn  30221  isclwwlknon  30228  clwwlknon1loop  30235  s2elclwwlknon2  30241  clwwlknonwwlknonb  30243  clwwlkvbij  30250  uhgr3cyclex  30319  fusgreg2wsplem  30470  fusgr2wsp2nb  30471  fusgreghash2wsp  30475  frrusgrord0  30477  2clwwlkel  30486  extwwlkfab  30489  extwwlkfabel  30490  clwwlknonclwlknonf1o  30499  dlwwlknondlwlknonf1o  30502  wlkl0  30504  numclwwlk2lem1  30513  numclwlk2lem2f  30514  numclwlk2lem2f1o  30516  numclwwlk5  30525  ex-opab  30569  isgrpo  30635  isgrpoi  30636  grpoidinvlem3  30644  grpoideu  30647  gidval  30650  grpoidinv2  30653  grpoinveu  30657  grpoinvval  30661  grpoinv  30663  vciOLD  30699  isvclem  30715  cnidOLD  30720  isnvlem  30748  nvmul0or  30788  imsmetlem  30828  diporthcom  30854  ipz  30857  nmlno0  30933  ajfval  30947  hmoval  30948  isphg  30955  isph  30960  ip2eqi  30994  ajval  30999  hvmul0or  31163  hvsubeq0  31206  hvaddeq0  31207  hvaddcan  31208  hvmulcan  31210  hvmulcan2  31211  hvsubadd  31215  his6  31237  hial0  31240  hial02  31241  hi2eq  31243  orthcom  31246  normlem7tALT  31257  normsub0  31274  normpyth  31283  hilid  31299  hhssnv  31402  ocel  31419  ocsh  31421  ocorth  31429  ocin  31434  occllem  31441  choc0  31464  pjpreeq  31536  omlsi  31542  pjoc1  31572  pjoml  31574  pjoc2  31577  chm0  31629  chocin  31633  chlejb1  31650  chlejb2  31651  chjo  31653  h1deoi  31687  h1de2i  31691  pjoml6i  31727  pjoml2  31749  pjoml3  31750  pjch  31832  hodsi  31913  hodid  31930  eigorth  31976  elunop  32010  adjeu  32027  adjval  32028  eigvecval  32034  unopf1o  32054  adj1  32071  adjeq  32073  hmdmadj  32078  lnopeq0i  32145  lnopeqi  32146  lnopeq  32147  lnfn0  32185  riesz4i  32201  riesz4  32202  riesz1  32203  cnlnadjlem3  32207  cnlnadjlem5  32209  cnlnadjeu  32216  cnlnssadj  32218  nmopadjlei  32226  opsqrlem1  32278  hmopidmpji  32290  pjimai  32314  isst  32351  ishst  32352  hstel2  32357  stadd3i  32386  stri  32395  largei  32405  golem2  32410  superpos  32492  sumdmdii  32553  mddmdin0i  32569  opreu2reuALT  32613  difeq  32655  elim2if  32681  disji2f  32715  disjif2  32719  disjxpin  32726  iundisj2f  32728  disjunsn  32732  fmptco1f1o  32774  ofpreima  32806  fnpreimac  32811  ressupprn  32831  curry2ima  32850  preiman0  32851  receqid  32885  xrofsup  32908  iundisj2fi  32938  f1ocnt  32941  fzo0opth  32944  elq2  32953  fprodex01  32966  sgn0bi  32981  prodindf  32990  xdivval  33046  xrecex  33047  xreceu  33049  xdivmul  33052  rexdiv  33053  wrdt2ind  33081  mndlrinvb  33153  mndlactfo  33155  mndractfo  33157  mndlactf1o  33158  mndractf1o  33159  gsummpt2d  33179  gsumwun  33206  fzo0pmtrlast  33222  cyc3genpm  33282  cycpmconjslem2  33285  fxpval  33295  fxpgaeq  33299  cntrval2  33301  isslmd  33332  slmdlema  33333  urpropd  33361  elrgspnlem4  33375  elrgspnsubrunlem2  33378  erlcl1  33390  erlcl2  33391  erldi  33392  erlbrd  33393  erler  33395  rloccring  33400  domnprodeq0  33406  domnlcanOLD  33410  isdrng4  33428  fracerl  33439  fracfld  33441  resv1r  33471  islinds5  33499  linds2eq  33513  dvdsruassoi  33516  dvdsruasso  33517  dvdsruasso2  33518  quslsm  33537  rhmimaidl  33564  qsidomlem2  33585  ssdifidllem  33588  ssdifidl  33589  ssdifidlprm  33590  opprqus0g  33622  qsdrngilem  33626  unitmulrprm  33668  1arithidom  33677  1arithufdlem3  33686  1arithufdlem4  33687  ply1dg1rt  33720  r1pid2OLD  33749  extvfvv  33775  extvfvcl  33777  evlextv  33783  esplysply  33812  esplyind  33816  lbsdiflsp0  33867  fedgmullem1  33870  fedgmullem2  33871  irngss  33928  irngnzply1lem  33931  extdgfialglem2  33934  ply1annidllem  33942  ply1annnr  33944  minplymindeg  33949  minplyann  33950  minplyirredlem  33951  minplyirred  33952  irngnminplynz  33953  minplyelirng  33956  irredminply  33957  algextdeglem6  33963  algextdeglem7  33964  rtelextdg2lem  33967  fldext2chn  33969  constrsuc  33979  constrsslem  33982  constrconj  33986  constrextdg2lem  33989  constrextdg2  33990  constrlccllem  33994  constrcccllem  33995  constrcbvlem  33996  constrext2chn  34000  constrcon  34015  1smat1  34045  iscref  34085  metidval  34131  metidv  34133  metider  34135  pstmxmet  34138  xrmulc1cn  34171  esumfsup  34311  esumpcvgval  34319  esumcvg  34327  inelsros  34419  diffiunisros  34420  ismeas  34440  isrnmeas  34441  brae  34482  braew  34483  dya2iocuni  34524  elcarsg  34546  eulerpartleme  34604  eulerpartlemv  34605  eulerpartlemb  34609  eulerpartgbij  34613  eulerpartlemr  34615  eulerpartlemgvv  34617  eulerpartlemgh  34619  eulerpartlemn  34622  elprob  34650  ballotlemi  34742  ballotlemi1  34744  ballotlemii  34745  ballotlemsima  34757  ballotlemfrcn0  34771  signsw0g  34797  signswmnd  34798  signstfvc  34815  prodfzo03  34844  reprval  34851  reprsum  34854  reprsuc  34856  reprpmtf1o  34867  axtgupdim2ALTV  34909  brafs  34916  bnj125  35114  bnj154  35120  bnj526  35130  bnj609  35159  bnj893  35170  bnj1321  35269  bnj1491  35299  nummin  35334  fineqvnttrclselem2  35363  fineqvnttrclselem3  35364  fineqvnttrclse  35365  noinfepfnregs  35373  subgrwlk  35420  loop1cycl  35425  subfacp1lem3  35470  subfacp1lem5  35472  subfacp1lem6  35473  cnpconn  35518  txpconn  35520  ptpconn  35521  indispconn  35522  connpconn  35523  cvxpconn  35530  cvmscbv  35546  cvmsi  35553  cvmsval  35554  cvmsdisj  35558  cvmsss2  35562  cvmliftmo  35572  cvmliftlem14  35585  cvmliftiota  35589  cvmlift2lem12  35602  cvmlift2lem13  35603  cvmlift2  35604  cvmliftphtlem  35605  cvmlift3lem2  35608  cvmlift3lem4  35610  cvmlift3lem6  35612  cvmlift3lem7  35613  cvmlift3lem9  35615  cvmlift3  35616  snmlval  35619  satffunlem  35689  prv1n  35719  mrsub0  35804  mrsubcn  35807  ismfs  35837  sinccvglem  35960  br6  36045  brbigcup  36184  imageval  36216  funpartlem  36230  dfrdg4  36239  altopthsn  36249  brsegle  36396  rankeq1o  36459  cbviotadavw  36567  subtr  36612  opnbnd  36623  cldbnd  36624  isfne  36637  topfneec  36653  neibastop3  36660  dfttc4lem1  36826  dfttc4lem2  36827  dfttc4  36828  elttcirr  36829  cnndvlem2  36914  bj-imdirval2  37613  bj-imdirid  37616  bj-imdirco  37620  bj-inftyexpiinj  37639  bj-isrvecd  37728  bj-isrvec2  37730  bj-bary1lem1  37741  bj-bary1  37742  qdiff  37757  finxp00  37834  nlpfvineqsn  37841  pibp19  37846  pibt2  37849  unccur  38040  matunitlindflem2  38054  ptrecube  38057  poimirlem4  38061  poimirlem19  38076  poimirlem23  38080  poimirlem25  38082  poimirlem27  38084  poimirlem28  38085  poimirlem31  38088  poimirlem32  38089  broucube  38091  mblfinlem2  38095  ovoliunnfl  38099  voliunnfl  38101  volsupnfl  38102  mbfresfi  38103  itg2addnclem  38108  itg2addnclem3  38110  itg2addnc  38111  ftc2nc  38139  cover2  38152  sdclem2  38179  fdc  38182  metf1o  38192  istotbnd3  38208  0totbnd  38210  sstotbnd2  38211  equivtotbnd  38215  totbndbnd  38226  prdstotbnd  38231  heibor1  38247  rrnmet  38266  isexid  38284  ismgmOLD  38287  opidonOLD  38289  exidu1  38293  cmpidelt  38296  exidreslem  38314  exidres  38315  exidresid  38316  grpoeqdivid  38318  elghomlem1OLD  38322  grpokerinj  38330  isrngo  38334  isrngod  38335  rngoideu  38340  isgrpda  38392  isdrngo2  38395  isdrngo3  38396  isrngohom  38402  divrngidl  38465  dmnnzd  38512  dmncan1  38513  disjeccnvep  38727  disjressuc2  38848  mopre  38908  qsdisjALTV  39136  dmqseqeq1  39164  unidmqseq  39177  disjdmqseq  39345  eldisjlem19  39350  riotasvd  39518  toycom  39535  islshpsm  39542  lshpnel2N  39547  lsatfixedN  39571  islshpat  39579  lcvexchlem4  39599  l1cvpat  39616  lkr0f  39656  lkrsc  39659  lshpkrlem1  39672  lkreqN  39732  isopos  39742  oposlem  39744  opcon2b  39759  cmtbr3N  39816  cvlcvrp  39902  hlrelat5N  39963  cvrval5  39977  cvrat4  40005  3atlem5  40049  2at0mat0  40087  psubclsetN  40498  4atex2  40639  isldil  40672  ltrnu  40683  ltrnid  40697  isdilN  40716  trlnid  40741  cdleme21k  40900  cdleme29b  40937  cdlemefrs29pre00  40957  cdlemefrs29bpre0  40958  cdlemefrs29cpre1  40960  cdleme32fva  40999  cdleme42b  41040  cdleme50ex  41121  cdleme  41122  cdlemg1a  41132  ltrniotaval  41143  cdlemeiota  41147  tendoid0  41387  cdlemksv2  41409  cdlemkuv2  41429  cdlemk36  41475  cdlemk42  41503  cdlemk  41536  tendoex  41537  cdleml3N  41540  cdleml5N  41542  tendospcanN  41585  cdlemm10N  41680  dihffval  41792  dihfval  41793  dihlsscpre  41796  islpolN  42045  mapdhval  42286  mapdheq  42290  hdmap1fval  42358  hdmap1val  42360  hdmap1eq  42363  hdmap1cbv  42364  hdmapval2lem  42393  hdmap11  42410  hdmap14lem2a  42429  hdmap14lem6  42435  hgmapval  42449  hlhillcs  42520  hlhilphllem  42521  aks4d1  42644  isprimroot  42648  mndmolinv  42650  linvh  42651  primrootsunit1  42652  primrootsunit  42653  primrootscoprmpow  42654  primrootscoprbij  42657  primrootlekpowne0  42660  primrootspoweq0  42661  ringexp0nn  42689  aks6d1c5lem1  42691  sticksstones8  42708  sticksstones9  42709  sticksstones10  42710  sticksstones11  42711  sticksstones12a  42712  sticksstones12  42713  sticksstones16  42717  sticksstones17  42718  sticksstones18  42719  sticksstones19  42720  aks6d1c6lem4  42728  aks6d1c6isolem3  42731  rhmqusspan  42740  grpods  42749  unitscyglem1  42750  unitscyglem2  42751  unitscyglem3  42752  unitscyglem5  42754  expeq1d  42871  zdivgd  42884  ef11d  42886  resubval  42914  renegadd  42919  resubeu  42924  resubadd  42926  sn-remul0ord  42955  sn-negex12  42964  addinvcom  42979  redivvald  42989  rediveud  42990  redivmuld  42992  sn-mul02  43012  mulgt0con1d  43030  mulgt0con2d  43031  fimgmcyclem  43089  fidomncyc  43091  fsuppind  43110  mhphflem  43116  prjspnfv01  43144  prjspner01  43145  prjspner1  43146  prjcrvval  43152  dffltz  43154  flt4lem7  43179  nna4b4nsq  43180  negexpidd  43201  mzpcompact2lem  43270  eldioph  43277  eldioph2lem1  43279  eldioph2lem2  43280  eldioph2  43281  eldioph2b  43282  eldioph3  43285  diophin  43291  diophun  43292  eq0rabdioph  43295  dvdsrabdioph  43325  eldioph4i  43327  diophren  43328  rabren3dioph  43330  fphpd  43331  pellexlem5  43348  pellexlem6  43349  pellex  43350  pell1qrval  43361  pell14qrval  43363  pell1234qrval  43365  pell1234qrreccl  43369  pell1234qrmulcl  43370  pell1234qrdich  43376  pell14qrdich  43384  pell1qr1  43386  pellqrexplicit  43392  rmxycomplete  43432  jm2.27  43523  rmydioph  43529  rmxdiophlem  43530  rmxdioph  43531  pw2f1ocnv  43552  pwssplit4  43604  elmnc  43651  dgraalem  43660  dgraaub  43663  dgraa0p  43664  mpaaeu  43665  mpaaval  43666  mpaalem  43667  aaitgo  43677  rngunsnply  43684  proot1ex  43711  cantnfresb  43839  tfsconcatfv  43856  tfsconcatb0  43859  tfsconcat0i  43860  tfsconcat0b  43861  tfsconcat00  43862  tfsconcatrev  43863  naddwordnexlem4  43916  sqrtcval  44155  relexpnul  44192  relexpxpnnidm  44217  relexpiidm  44218  trclfvdecomr  44242  rfovcnvf1od  44518  ntrkbimka  44552  ntrk0kbimka  44553  clsk3nimkb  44554  clsk1independent  44560  ntrclsfveq1  44574  ntrclsfveq2  44575  ntrclskb  44583  k0004val  44664  k0004val0  44668  mnringmulrcld  44742  expgrowth  44849  bcc0  44854  relpfrlem  45467  permac8prim  45528  disjinfi  45708  fsumf1of  46088  limsupmnflem  46232  liminfpnfuz  46328  climxlim2lem  46357  coseq0  46376  icccncfext  46399  dvnmptconst  46453  dvnprodlem1  46458  dvnprodlem2  46459  dvnprodlem3  46460  dvnprod  46461  stoweidlem15  46527  stoweidlem31  46543  stoweidlem35  46547  stoweidlem36  46548  stoweidlem37  46549  stoweidlem43  46555  stoweidlem44  46556  stoweidlem46  46558  stoweidlem55  46567  stoweidlem59  46571  dirkerval2  46606  dirkertrigeqlem1  46610  dirkeritg  46614  dirkercncf  46619  fourierdlem2  46621  fourierdlem3  46622  fourierdlem42  46661  fourierdlem48  46666  fourierdlem49  46667  fourierdlem71  46689  fourierdlem112  46730  fourierdlem113  46731  elaa2lem  46745  etransclem11  46757  etransclem24  46770  etransclem26  46772  etransclem28  46774  etransclem35  46781  ioorrnopnxr  46819  salgenval  46833  intsaluni  46841  salgenn0  46843  salgencl  46844  sssalgen  46847  salgenss  46848  salgenuni  46849  issalgend  46850  dfsalgen2  46853  subsaliuncl  46870  sge0f1o  46894  sge0fodjrnlem  46928  ismea  46963  nnfoctbdjlem  46967  iundjiun  46972  isome  47006  caragenel  47007  ovn0lem  47077  ovnsubaddlem1  47082  smflimlem4  47286  smflim  47289  sigarcol  47376  chnsubseqwl  47393  nthrucw  47400  cfsetsnfsetf  47590  cfsetsnfsetfo  47592  fnbrafvb  47686  afv2fv0  47797  readdcnnred  47835  resubcnnred  47836  cndivrenred  47838  nnmul2  47862  ceilbi  47869  minusmodnep2tmod  47891  modmkpkne  47899  nndivides2  47916  fargshiftf1  47985  fargshiftfo  47986  ichexmpl2  48014  ichnreuop  48016  ichreuopeq  48017  elsprel  48019  prproropf1olem4  48050  reupr  48066  reuopreuprim  48070  goldbachthlem2  48093  fmtnoprmfac2lem1  48113  fmtnofac2lem  48115  prmdvdsfmtnof1lem2  48132  mod42tp1mod8  48149  lighneallem2  48153  lighneallem3  48154  lighneallem4  48157  proththd  48161  41prothprm  48166  requad01  48181  requad2  48183  dfeven2  48209  dfeven5  48226  dfodd7  48227  fpprel  48288  fppr2odd  48291  fpprwppr  48299  fpprwpprb  48300  nnsum3primesgbe  48352  isubgredg  48426  upgrimpths  48469  ushggricedg  48487  uhgrimisgrgric  48491  isubgr3stgrlem3  48528  isubgr3stgrlem4  48529  isubgr3stgrlem6  48531  grlimprclnbgr  48556  grlimgrtrilem2  48562  gpgedgvtx0  48621  gpgedgvtx1  48622  gpgvtxedg0  48623  gpgvtxedg1  48624  gpg3kgrtriexlem5  48647  gpgprismgr4cycllem3  48657  pgnbgreunbgrlem2lem1  48674  pgnbgreunbgrlem2lem2  48675  pgnbgreunbgrlem2lem3  48676  upwlksfval  48695  0nodd  48730  2nodd  48732  nnsgrpnmnd  48738  nn0mnd  48739  lidldomn1  48791  zlidlring  48794  uzlidlring  48795  2zrngamgm  48805  2zrngamnd  48807  2zrngagrp  48809  2zrngnmlid2  48817  ztprmneprm  48907  dmatALTbasel  48962  linindslinci  49008  lindslinindsimp1  49017  lindslinindimp2lem4  49021  lindslinindsimp2lem5  49022  linds0  49025  el0ldep  49026  lindsrng01  49028  snlindsntorlem  49030  snlindsntor  49031  ldepspr  49033  lincresunit3  49041  islindeps2  49043  isldepslvec2  49045  zlmodzxzldep  49064  blen1b  49148  dig2bits  49174  nn0sumshdiglem1  49181  0aryfvalelfv  49195  itcovalsuc  49227  prelrrx2b  49274  eenglngeehlnmlem1  49297  eenglngeehlnmlem2  49298  rrx2linest2  49304  elrrx2linest2  49305  spheres  49306  2sphere  49309  2sphere0  49310  line2ylem  49311  line2  49312  line2xlem  49313  line2x  49314  line2y  49315  itscnhlc0yqe  49319  itschlc0yqe  49320  itscnhlc0xyqsol  49325  itschlc0xyqsol1  49326  itsclc0xyqsolr  49329  itsclc0  49331  itsclc0b  49332  itsclinecirc0b  49334  itsclquadb  49336  itsclquadeu  49337  itscnhlinecirc02p  49345  resinsnALT  49432  sepnsepolem2  49482  sepnsepo  49483  sepfsepc  49487  iscnrm3rlem8  49506  iscnrm3r  49507  iscnrm3llem2  49509  iscnrm3l  49510  oppcendc  49577  isisod  49586  sectpropdlem  49595  ssccatid  49631  resccatlem  49632  imasubc  49710  uptrlem1  49769  oppcthinendcALT  50000  functhinclem2  50004  fullthinc2  50010  thincciso  50012  thinccisod  50013  termcpropd  50062  fulltermc2  50071  oduoppcciso  50125  discsnterm  50133  aacllem  50360