Theorem eqeq1d 2767

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 2758	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	biimpi 219	. . 3 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		bibi1 354	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	alimi 1844	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		albi 1851	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)) → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
7	1, 3, 5, 6	4syl 20	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
8		dfcleq 2758	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
9		dfcleq 2758	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
10	7, 8, 9	3bitr4g 317	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  eqeq1  2769  eqcomd  2771  eqeq2d  2776  eqeqan12d  2779  neeq1d  3019  csbconstg  3873  csbhypf  3882  csbiebt  3883  csbiebg  3886  sbceq2g  4384  csbie2df  4408  disjeq0  4416  disjssun  4428  mosneq  4809  preq12b  4817  preq12bg  4820  elpreqprlem  4833  disji2  5095  invdisjrab  5098  disjprg  5107  disjxun  5109  iin0  5335  opthg  5461  opeqsng  5488  propeqop  5492  wefrc  5657  xpcan  6176  xpcan2  6177  dmsnopg  6216  rnmpt0f  6246  reuop  6298  dfpo2  6301  sspred  6315  onfr  6404  unisucg  6445  nsuceq0  6450  iotaeq  6508  iotabi  6509  fneq1  6630  fnun  6653  fnresdisj  6659  fnimadisj  6671  fnimaeq0  6672  foeq1  6792  fveqeq2d  6893  fvun1  6976  fvmptdv2  7012  fndmdifeq0  7043  fneqeql  7045  dffo3  7101  dffo3f  7105  fnnfpeq0  7182  foeqcnvco  7307  f1eqcocnv  7308  isofrlem  7347  eqfunresadj  7369  ovanraleqv  7443  f1opr  7475  eloprabga  7528  ovmpodv2  7577  ov3  7582  ovelimab  7598  caovcang  7621  caovcan  7624  caovmo  7657  caofinvl  7716  caofid1  7719  caofid2  7720  caofidlcan  7722  caonncan  7728  tfisi  7861  mptcnfimad  7989  oteqimp  8011  br1steqg  8014  br2ndeqg  8015  eqop  8034  reldm  8047  mposn  8104  fparlem1  8113  fparlem2  8114  fsplit  8118  frxp  8128  xporderlem  8129  fnwelem  8133  xpord2lem  8144  xpord3lem  8151  poseq  8160  soseq  8161  fnsuppeq0  8194  suppssov1  8199  suppssov2  8200  suppofss1d  8206  suppofss2d  8207  tposfo2  8251  mpocurryd  8271  iinon  8333  onnseq  8337  tz7.49  8438  seqomlem2  8444  oe0m1  8512  om0r  8530  oe1m  8536  oawordeulem  8545  oawordeu  8546  oarec  8553  omord  8559  oneo  8572  omeu  8576  oeeui  8594  nnm0r  8602  nnmord  8624  nnawordex  8629  nnaordex2  8631  nnneo  8647  nneob  8648  omopth  8654  nnasmo  8655  ereq1  8708  eqerlem  8736  qsdisj  8798  erov  8818  eceqoveq  8826  mapsnd  8890  endisj  9059  pw2f1olem  9076  enfixsn  9081  disjenex  9130  domssex2  9132  xpf1o  9134  mapxpen  9138  unxpdomlem2  9224  enp1ilem  9245  fodomfib  9295  fipreima  9322  opthreg  9594  cantnfp1lem3  9656  ssttrcl  9691  ttrcltr  9692  ttrclss  9696  ttrclselem2  9702  frmin  9728  updjud  9936  pm54.43  10003  dfac5  10128  dfacacn  10141  kmlem9  10158  cfeq0  10255  cfss  10264  cfslb  10265  fin23lem22  10326  fin23lem12  10330  fin23lem19  10335  fin23lem30  10341  fin23lem33  10344  fin1a2lem6  10404  axcc2lem  10435  axdc3lem2  10450  axdc3lem3  10451  axdc3lem4  10452  axdc3  10453  axdc4lem  10454  zorn2lem7  10501  ttukeylem3  10510  ttukeylem6  10513  ttukey2g  10515  fodomb  10525  axacndlem5  10613  fpwwe2cbv  10632  fpwwe2lem2  10634  fpwwe2lem3  10635  fpwwe2lem11  10643  fpwwe2lem12  10644  fpwwe  10648  pwfseqlem2  10661  pwxpndom2  10667  addnidpi  10903  ltexpi  10904  recmulnq  10966  ltexnq  10977  halfnq  10978  archnq  10982  ltexpri  11045  recexpr  11053  addsrpr  11077  mulsrpr  11078  00sr  11101  negexsr  11104  recexsrlem  11105  recexsr  11109  axrnegex  11164  axrrecex  11165  00id  11402  mul02  11405  addrid  11407  cnegex  11408  cnegex2  11409  subval  11465  subadd  11477  subadd2  11478  subsub23  11479  addsubeq4  11489  subcan2  11500  negcon1  11527  subcan  11530  addrsub  11648  ltordlem  11756  ltord1  11757  recex  11863  mul0or  11871  muleqadd  11875  receu  11876  mulcan1g  11884  divval  11891  divmul  11892  rec11  11930  ldiv  12066  rdiv  12067  ind1a  12246  zdiv  12684  uzin  12916  xaddval  13267  xmulval  13269  xnn0xadd0  13291  xnegdi  13292  ioo0  13415  ico0  13436  ioc0  13437  icc0  13438  1fv  13694  fzon  13728  fvinim0ffz  13837  flbi  13869  mod0  13929  modmuladdnn0  13971  modirr  13998  addmodlteq  14002  uzrdgfni  14014  axdc4uzlem  14039  fsuppmapnn0fiubex  14048  mptnn0fsupp  14053  seqid  14103  seqz  14106  expval  14119  expeq0  14148  sqeqor  14272  nn0opth2  14328  hashdom  14435  elprchashprn2  14452  hashbc  14510  hashf1lem1  14512  hash2pwpr  14533  ccat0  14633  wrdl1s1  14674  ccatws1lenp1b  14681  pfxsuff1eqwrdeq  14760  swrdccatin2  14790  pfxccatin12lem2  14792  2cshwcshw  14888  scshwfzeqfzo  14889  cshimadifsn  14892  cshimadifsn0  14893  s2f1o  14979  wrdlen2i  15005  2swrd2eqwrdeq  15016  wwlktovf  15019  wwlktovf1  15020  wwlktovfo  15021  wrd2f1tovbij  15023  relexp0g  15085  relexpsucnnr  15088  dfrtrcl2  15125  sgn0bi  15166  mulre  15198  rennim  15316  cnpart  15317  01sqrex  15326  resqrex  15327  sqrmo  15328  resqrtcl  15330  resqrtthlem  15331  sqrtgt0  15335  sqrtneg  15344  sqrtsq2  15345  absmod0  15380  sqreulem  15437  sqreu  15438  sqrtthlem  15440  eqsqrtd  15445  reusq0  15542  fsum00  15875  telfsumo  15879  prodss  16026  fprodle  16075  tanaddlem  16246  absefib  16278  efieq1re  16279  divides  16336  dvdsval2  16337  nndivides  16344  dvds0lem  16348  dvds1lem  16349  dvds2lem  16350  negdvdsb  16354  muldvds1  16362  muldvds2  16363  dvdscmulr  16366  dvdsmulcr  16367  difmod0  16369  dvdstr  16376  dvdsabseq  16395  divconjdvds  16397  odd2np1lem  16422  odd2np1  16423  even2n  16424  oddm1even  16425  2tp1odd  16434  opeo  16447  omeo  16448  m1exp1  16458  divalglem4  16478  divalglem8  16482  divalgb  16486  bitsuz  16556  smupvallem  16565  gcdaddmlem  16606  gcdabs1  16611  bezoutlem3  16623  rplpwr  16640  rprpwr  16641  alginv  16657  algcvga  16661  algfx  16662  eucalgval2  16663  coprmdvds  16735  qredeq  16739  qredeu  16740  coprmprod  16743  coprmproddvdslem  16744  divgcdcoprm0  16747  divgcdcoprmex  16748  cncongr1  16749  rpexp  16805  rpexp12i  16807  cncongrprm  16812  qnumdenbi  16827  phival  16850  phicl2  16851  dfphi2  16857  phiprmpw  16859  phimullem  16862  eulerthlem1  16864  eulerthlem2  16865  eulerth  16866  fermltl  16867  hashgcdlem  16871  phisum  16874  odzval  16875  odzdvds  16879  reumodprminv  16888  modprm0  16889  nnnn0modprm0  16890  modprmn0modprm0  16891  coprimeprodsq  16892  coprimeprodsq2  16893  pythagtriplem2  16901  pythagtrip  16918  pcval  16928  pceulem  16929  pcqmul  16937  pcqcl  16940  pcabs  16959  pcgcd1  16961  pc2dvds  16963  pcaddlem  16972  pcadd  16973  pcmpt  16976  prmpwdvds  16988  pockthi  16991  unbenlem  16992  4sqlem12  17040  ramz  17109  ramcl  17113  cshwrepswhash1  17186  imasval  17589  fvprif  17639  iscat  17752  iscatd  17753  catidex  17754  catideu  17755  cidfval  17756  cidval  17757  catidd  17760  catlid  17763  catrid  17764  catpropd  17789  cidpropd  17790  issect  17834  dfiso2  17853  invcoisoid  17873  isocoinvid  17874  setcepi  18169  latleeqj2  18532  latleeqm2  18548  oduclatb  18587  mgmidmo  18744  grpidval  18746  grpidpropd  18747  ismgmid  18750  0gisid  18753  ismgmid2  18754  mgmidsssn0  18758  grpinvalem  18759  grprida  18761  mgmidpfod  18762  idressidex0  18765  idressid  18767  gsumvalx  18768  gsumpropd  18770  gsumpropd2lem  18771  gsumress  18774  gsumval2  18778  ismnddef  18828  sgrpidmnd  18831  ismndd  18849  mndpropd  18854  mndinvmod  18861  mnd1  18876  ismhm  18882  gsumvallem2  18932  frmdgsum  18960  frmdup3  18965  efmndmnd  18987  smndex1mnd  19011  sgrp2rid2  19027  sgrp2rid2ex  19028  pwmnd  19045  grpinvex  19056  isgrpd2  19069  isgrpd  19071  dfgrp2  19075  grpinveu  19087  grpinvval  19093  grplinv  19102  isgrpinv  19106  grplrinv  19109  grpidinv2  19110  grpidinv  19111  grplmulf1o  19125  grpraddf1o  19126  grpsubeq0  19138  grpsubadd  19140  dfgrp3lem  19150  dfgrp3  19151  grp1  19159  imasgrp2  19167  qusgrp2  19170  mhmmnd  19176  ghmgrp  19178  mulgval  19183  mulgaddcom  19210  eqg0el  19300  cycsubmel  19317  ghmeqker  19359  ghmf1  19362  conjnmzb  19369  ghmqusker  19403  isga  19407  subgga  19416  gaorb  19423  gaorber  19424  gastacl  19425  gastacos  19426  orbsta  19429  symgfix2  19532  gsmsymgrfixlem1  19543  gsmsymgrfix  19544  gsmsymgreq  19548  symgfixelq  19549  f1omvdconj  19562  pmtrdifwrdel2  19602  psgnunilem1  19609  psgnunilem2  19611  psgnunilem3  19612  psgnunilem4  19613  odval  19650  odid  19654  odlem2  19655  oddvdsnn0  19660  odnncl  19661  oddvds  19663  odcong  19665  odeq  19666  odmulgid  19670  odmulgeq  19673  gexval  19694  gexid  19697  gexlem2  19698  gexdvdsi  19699  gexdvds  19700  subgpgp  19713  sylow1lem1  19714  sylow1lem4  19717  sylow2alem1  19733  sylow2alem2  19734  sylow2blem2  19737  sylow3lem6  19748  lsmdisj3a  19805  lsmdisj3b  19806  pj1val  19811  pj1eq  19816  efgredlemd  19860  efgredlem  19863  efgred  19864  efgrelexlema  19865  frgpup3  19894  ablsubadd  19925  ablsubsub23  19940  iscyggen  19996  cyggenod  20000  gsumval3lem2  20022  gsumval3  20023  gsummptnn0fz  20102  dmdprd  20116  dprddisj  20127  dprdfeq0  20140  dprdf11  20141  dmdprdpr  20167  dpjeq  20177  ablfacrp  20184  pgpfac1lem2  20193  pgpfac1lem3  20195  pgpfac1lem5  20197  pgpfac1  20198  pgpfaclem1  20199  pgpfaclem2  20200  pgpfaclem3  20201  ablfaclem2  20204  ablfaclem3  20205  ablfac2  20207  rngmneg1  20291  rngmneg2  20292  rng1zrlem  20305  ringurd  20313  srgrz  20335  srglz  20336  srgisid  20337  ringid  20404  qusring2  20464  opprring  20477  dvdsrval  20491  dvdsrmul  20494  dvdsr01  20501  dvdsr02  20502  crngunit  20508  ringunitnzdiv  20528  dvreq1  20541  dvdsrpropd  20546  irredn0  20553  irredrmul  20557  irredmul  20559  rngisomring  20597  isrhm0  20606  rhmdvdsr  20657  lringuplu  20695  subrg1  20733  subrgdvds  20737  isrrg  20849  rrgeq0i  20850  rrgeq0  20851  domneq0  20859  isdomn4  20866  domnlcanb  20870  domnrcanb  20872  isdrng4  20891  isdrng3lem1  20903  isdrng3lem2  20904  isdrng5  20906  drngid2  20908  isdrngd  20920  isdrngdOLD  20922  fidomndrnglem  20928  isabv  20966  issrngd  21010  islmod  21037  islmodd  21039  lmodprop2d  21097  mptscmfsupp0  21100  lss1d  21136  lspextmo  21229  lvecvs0or  21284  lvecvscan  21287  lvecvscan2  21288  lbsacsbs  21332  rngqiprngimf1lem  21486  rng2idl1cntr  21497  qsidomlem2  21533  ssdifidllem  21536  ssdifidl  21537  ssdifidlprm  21538  prmirredlem  21674  pzriprnglem7  21689  pzriprnglem13  21695  chrdvds  21728  chrnzr  21732  domnchr  21734  znval  21737  zncyg  21750  znfld  21762  znunit  21765  znrrg  21767  frgpcyg  21775  psgndiflemB  21802  psgndiflemA  21803  ipeq0  21840  ip2eq  21855  elocv  21870  ocvi  21871  obsne0  21927  dsmmacl  21943  dsmmlss  21946  frlmphl  21983  frlmup4  22003  islindf4  22040  islindf5  22041  mplsubrglem  22205  mplmon2  22264  evlslem1  22285  evlseu  22286  evlsval  22289  evlsval2  22290  evlsval3  22292  ismhp3  22357  mhpsclcl  22362  mhpvarcl  22363  mhpmulcl  22364  psdmul  22381  psdmvr  22384  cply1coe0bi  22514  gsummoncoe1  22520  evl1vsd  22556  dmatel  22702  dmatelnd  22705  dmatmulcl  22709  scmateALT  22721  mdetdiaglem  22807  mdetunilem1  22821  mdetunilem3  22823  mdetunilem4  22824  mdetunilem9  22829  symgmatr01lem  22862  symgmatr01  22863  gsummatr01lem1  22864  gsummatr01lem4  22867  gsummatr01  22868  smadiadetlem3  22877  cramerlem3  22898  pmatcoe1fsupp  22910  cpmatel  22920  1elcpmat  22924  cpmatmcllem  22927  cpmatmcl  22928  d1mat2pmat  22948  m2cpminvid2lem  22963  m2cpminvid2  22964  decpmatmulsumfsupp  22982  pmatcollpw2lem  22986  pmatcollpwscmatlem1  22998  mp2pm2mplem4  23018  pm2mpmhmlem1  23027  chpscmat  23051  cpmidpmatlem3  23081  cayleyhamilton0  23098  cayleyhamiltonALT  23100  cayleyhamilton1  23101  0ntr  23280  ntreq0  23286  cldlp  23359  pnrmopn  23552  hausnei2  23562  cnhaus  23563  nrmsep  23566  isnrm2  23567  regsep2  23585  dishaus  23591  ordthauslem  23592  iscmp  23597  cmpsublem  23608  cmpsub  23609  tgcmp  23610  sscmp  23614  hauscmplem  23615  cmpfi  23617  bwth  23619  connsuba  23629  nconnsubb  23632  isref  23719  islocfin  23727  elpt  23782  elptr  23783  pthaus  23848  txcmp  23853  hausdiag  23855  txhaus  23857  txkgen  23862  xkohaus  23863  xkococnlem  23869  regr1lem  23949  fbasrn  24094  fmfnfmlem3  24166  flimtopon  24180  fclstopon  24222  alexsubb  24256  symgtgp  24316  qustgpopn  24330  qustgphaus  24333  ustuqtop  24456  isusp  24471  ispsmet  24514  psmet0  24518  ismet  24533  isxmet  24534  xmeteq0  24548  metn0  24570  xmetres2  24571  imasf1oxmet  24585  xblss2ps  24611  xblss2  24612  xmseq0  24674  comet  24723  stdbdxmet  24725  methaus  24730  dscmet  24782  nrmmetd  24784  nmeq0  24828  tngngp  24864  tngngp3  24866  nlmmul0or  24893  cnmet  24981  xrsxmet  25020  metnrmlem3  25072  icopnfcnv  25154  iccpnfcnv  25156  ishtpy  25184  isphtpy  25193  phtpyi  25196  om1elbas  25244  elpi1i  25258  pi1grplem  25261  isclmp  25309  cphsqrtcl2  25398  tcphcph  25449  bcth3  25543  rrxcph  25604  rrxmet  25620  ivth2  25667  iundisj2  25761  dyaddisj  25808  volivth  25819  mbfinf  25877  i1f1lem  25901  i1fmullem  25906  i1fmulclem  25914  i1fres  25917  itg1climres  25926  mbfi1fseqlem4  25930  dvnres  26143  dvcobr  26158  rolle  26202  cmvth  26203  deg1leb  26305  ismon1p  26353  q1peqb  26366  dvdsr1p  26374  ply1remlem  26375  fta1glem2  26379  idomrootle  26383  elply2  26406  ne0p  26417  coeeu  26435  coelem  26436  coeeq  26437  dgrle  26453  coeaddlem  26459  plymul0or  26492  ofmulrt  26493  plydivlem3  26509  plydivlem4  26510  plydivex  26511  plydiveu  26512  plydivalg  26513  quotlem  26514  plyremlem  26518  quotcan  26523  plyexmo  26527  elqaalem3  26535  qaa  26537  iaa  26541  aareccl  26542  aacjcl  26543  aannenlem2  26545  reeff1o  26663  sineq0  26742  coseq1  26743  efeq1  26746  recosf1o  26753  logeftb  26801  cosarg0d  26827  logtayl  26878  cxpval  26882  cxpeq0  26896  root1eq1  26973  cxpeq  26975  logbgcd1irr  27012  angrtmuld  27026  affineequiv  27041  affineequiv3  27043  angpieqvdlem2  27047  quad2  27057  dcubic1lem  27061  dcubic2  27062  dcubic  27064  mcubic  27065  cubic2  27066  dquartlem1  27069  dquart  27071  quart  27079  atandm2  27095  atandm4  27097  atantan  27141  wilthlem2  27286  wilthlem3  27287  muval2  27351  isnsqf  27352  mumullem2  27397  sqff1o  27399  muinv  27410  mpodvdsmulf1o  27411  dvdsmulf1o  27413  dchrelbas2  27454  dchrmullid  27469  dchrfi  27472  lgsval  27518  lgsdir  27549  lgsne0  27552  lgsprme0  27556  lgsdirnn0  27561  lgsqrlem1  27563  lgsqr  27568  gausslemma2dlem0c  27575  gausslemma2dlem0i  27581  gausslemma2dlem7  27590  gausslemma2d  27591  lgseisenlem2  27593  lgsquadlem1  27597  lgsquadlem2  27598  lgsquad2lem2  27602  lgsquad3  27604  m1lgs  27605  2lgs  27624  2sqlem7  27641  2sqlem8  27643  2sqlem9  27644  2sqlem11  27646  2sq  27647  2sq2  27650  2sqmo  27654  addsq2reu  27657  addsqn2reu  27658  addsqrexnreu  27659  addsqnreup  27660  addsq2nreurex  27661  2sqreulem1  27663  2sqreultlem  27664  2sqreunnlem1  27666  2sqreunnltlem  27667  2sqreulem4  27671  2sqreuop  27679  2sqreuopnn  27680  2sqreuoplt  27681  2sqreuopltb  27682  2sqreuopnnlt  27683  2sqreuopnnltb  27684  2sqreuopb  27685  dchrisumlem1  27706  dchrvmaeq0  27721  dchrisum0re  27730  ostth3  27855  ltsval  27864  nosepssdm  27903  nosupprefixmo  27917  noinfprefixmo  27918  nosupcbv  27919  nosupdm  27921  nosupfv  27923  nosupres  27924  nosupbnd1lem1  27925  nosupbnd1lem3  27927  nosupbnd1lem5  27929  noinfcbv  27934  noinfdm  27936  noinffv  27938  noinfres  27939  noinfbnd1lem3  27942  noinfbnd1lem5  27944  eqcuts  28031  cutbdaylt  28044  made0  28109  madecut  28129  negsid  28287  negsex  28289  subadds  28316  divsmo  28430  muls0ord  28431  divsval  28435  norecdiv  28436  recsne0  28438  divmulsw  28439  divs1  28450  precsexlem8  28460  precsexlem9  28461  precsexlem11  28463  precsex  28464  recsex  28465  abssor  28492  elons  28499  noseqrdgfn  28552  bdayn0sf1o  28616  eucliddivs  28622  zsoring  28655  n0seo  28667  zseo  28668  nohalf  28670  expsne0  28682  pw2recs  28684  halfcut  28704  z12negscl  28724  z12zsodd  28728  z12sge0  28729  renegscl  28744  istrkg3ld  28783  axtgcgrid  28785  axtgsegcon  28786  axtg5seg  28787  axtgupdim2  28793  tgjustc1  28797  tgjustc2  28798  iscgrg  28834  isismt  28856  legov  28907  legov2  28908  hlcgreu  28943  mirreu3  28984  mircgr  28987  mirbtwn  28988  ismir  28989  mireq  28995  lnssplng  29127  ismidb  29140  lmiopp  29165  dfcgra2  29194  inaghl  29219  brprlng  29245  prlngsym  29248  dfprlng3  29255  f1otrg  29277  ttgval  29281  ttgelitv  29289  brbtwn  29306  brcgr  29307  colinearalglem2  29314  colinearalg  29317  axsegconlem1  29324  axsegcon  29334  ax5seglem4  29339  ax5seglem5  29340  axpaschlem  29347  axpasch  29348  axlowdimlem16  29364  axeuclidlem  29369  axeuclid  29370  axcontlem2  29372  axcontlem4  29374  axcontlem5  29375  edglnl  29550  usgredg2ALT  29603  usgredgprvALT  29605  usgrnloopvALT  29611  ushgredgedgloop  29641  edg0usgr  29663  nb3grpr  29792  cplgr1v  29840  cusgrsize  29864  vtxdgfval  29877  vtxdeqd  29887  vtxdun  29891  vtxd0nedgb  29898  vtxdusgr0edgnelALT  29906  1loopgrvd2  29913  usgruvtxvdb  29939  usgrvd0nedg  29943  vtxdginducedm1  29953  rusgrpropedg  29994  wksfval  30019  wlklenvclwlk  30063  iswlkon  30065  subgrwlk  30098  ispth  30135  dfpth2  30143  upgrwlkdvdelem  30151  crctcshwlkn0lem6  30233  wwlknon  30275  wwlksm1edg  30299  wwlksnextbi  30312  wwlksnextfun  30316  wwlksnextinj  30317  wwlksnextsurj  30318  wwlksnextbij  30320  wlksnwwlknvbij  30326  wwlksnextproplem3  30329  wwlksnextprop  30330  wspn0  30342  umgr2adedgwlkonALT  30365  umgr2adedgspth  30366  umgr2wlkon  30368  rusgrnumwwlkslem  30390  rusgrnumwwlkb0  30392  rusgrnumwwlks  30395  clwlkclwwlklem2a4  30417  clwlknf1oclwwlknlem2  30502  clwlknf1oclwwlkn  30504  isclwwlknon  30511  clwwlknon1loop  30518  s2elclwwlknon2  30524  clwwlknonwwlknonb  30526  clwwlkvbij  30533  loop1cycl  30573  uhgr3cyclex  30606  fusgreg2wsplem  30757  fusgr2wsp2nb  30758  fusgreghash2wsp  30762  frrusgrord0  30764  2clwwlkel  30773  extwwlkfab  30776  extwwlkfabel  30777  clwwlknonclwlknonf1o  30786  dlwwlknondlwlknonf1o  30789  wlkl0  30791  numclwwlk2lem1  30800  numclwlk2lem2f  30801  numclwlk2lem2f1o  30803  numclwwlk5  30812  ex-opab  30856  isgrpo  30922  isgrpoi  30923  grpoidinvlem3  30931  grpoideu  30934  gidval  30937  grpoidinv2  30940  grpoinveu  30944  grpoinvval  30948  grpoinv  30950  vciOLD  30986  isvclem  31002  cnidOLD  31007  isnvlem  31035  nvmul0or  31075  imsmetlem  31115  diporthcom  31141  ipz  31144  nmlno0  31220  ajfval  31234  hmoval  31235  isphg  31242  isph  31247  ip2eqi  31281  ajval  31286  hvmul0or  31450  hvsubeq0  31493  hvaddeq0  31494  hvaddcan  31495  hvmulcan  31497  hvmulcan2  31498  hvsubadd  31502  his6  31524  hial0  31527  hial02  31528  hi2eq  31530  orthcom  31533  normlem7tALT  31544  normsub0  31561  normpyth  31570  hilid  31586  hhssnv  31689  ocel  31706  ocsh  31708  ocorth  31716  ocin  31721  occllem  31728  choc0  31751  pjpreeq  31823  omlsi  31829  pjoc1  31859  pjoml  31861  pjoc2  31864  chm0  31916  chocin  31920  chlejb1  31937  chlejb2  31938  chjo  31940  h1deoi  31974  h1de2i  31978  pjoml6i  32014  pjoml2  32036  pjoml3  32037  pjch  32119  hodsi  32200  hodid  32217  eigorth  32263  elunop  32297  adjeu  32314  adjval  32315  eigvecval  32321  unopf1o  32341  adj1  32358  adjeq  32360  hmdmadj  32365  lnopeq0i  32432  lnopeqi  32433  lnopeq  32434  lnfn0  32472  riesz4i  32488  riesz4  32489  riesz1  32490  cnlnadjlem3  32494  cnlnadjlem5  32496  cnlnadjeu  32503  cnlnssadj  32505  nmopadjlei  32513  opsqrlem1  32565  hmopidmpji  32577  pjimai  32601  isst  32638  ishst  32639  hstel2  32644  stadd3i  32673  stri  32682  largei  32692  golem2  32697  superpos  32779  sumdmdii  32840  mddmdin0i  32856  opreu2reuALT  32896  difeq  32937  elim2if  32963  disji2f  32995  disjif2  32999  disjxpin  33006  iundisj2f  33008  disjunsn  33012  fmptco1f1o  33051  ofpreima  33083  fnpreimac  33088  ressupprn  33108  curry2ima  33127  preiman0  33128  receqid  33161  xrofsup  33184  iundisj2fi  33214  f1ocnt  33217  fzo0opth  33220  elq2  33228  fprodex01  33241  prodindf  33254  xdivval  33310  xrecex  33311  xreceu  33313  xdivmul  33316  rexdiv  33317  wrdt2ind  33341  mndlrinvb  33411  mndlactfo  33413  mndractfo  33415  mndlactf1o  33416  mndractf1o  33417  gsummpt2d  33435  gsumwun  33462  fzo0pmtrlast  33478  cyc3genpm  33538  cycpmconjslem2  33541  fxpval  33551  fxpgaeq  33555  cntrval2  33557  isslmd  33588  slmdlema  33589  urpropd  33616  isunitc  33627  elrgspnlem4  33631  elrgspnsubrunlem2  33634  erlcl1  33646  erlcl2  33647  erldi  33648  erlbrd  33649  erler  33651  erld2  33652  rloccring  33657  rlocinvunit  33661  rlocisunit  33662  domnprodeq0  33665  fracerl  33693  fracfld  33695  resv1r  33725  islinds5  33748  linds2eq  33760  dvdsruassoi  33763  dvdsruasso  33764  dvdsruasso2  33765  quslsm  33780  rhmimaidl  33806  opprqus0g  33838  qsdrngilem  33842  unitmulrprm  33884  1arithidom  33893  1arithufdlem3  33902  1arithufdlem4  33903  ply1dg1rt  33936  extvfvv  33990  extvfvcl  33992  evlextv  33998  esplysply  34027  esplyind  34031  lbsdiflsp0  34082  fedgmullem1  34085  fedgmullem2  34086  irngss  34143  irngnzply1lem  34146  extdgfialglem2  34149  ply1annidllem  34157  ply1annnr  34159  minplymindeg  34164  minplyann  34165  minplyirredlem  34166  minplyirred  34167  irngnminplynz  34168  minplyelirng  34171  irredminply  34172  algextdeglem6  34178  algextdeglem7  34179  rtelextdg2lem  34182  fldext2chn  34184  constrsuc  34194  constrsslem  34197  constrconj  34201  constrextdg2lem  34204  constrextdg2  34205  constrlccllem  34209  constrcccllem  34210  constrcbvlem  34211  constrext2chn  34215  constrcon  34230  1smat1  34260  iscref  34300  metidval  34346  metidv  34348  metider  34350  pstmxmet  34353  xrmulc1cn  34386  esumfsup  34526  esumpcvgval  34534  esumcvg  34542  inelsros  34635  diffiunisros  34636  ismeas  34656  isrnmeas  34657  brae  34698  braew  34699  dya2iocuni  34740  elcarsg  34762  eulerpartleme  34820  eulerpartlemv  34821  eulerpartlemb  34825  eulerpartgbij  34829  eulerpartlemr  34831  eulerpartlemgvv  34833  eulerpartlemgh  34835  eulerpartlemn  34838  elprob  34866  ballotlemi  34958  ballotlemi1  34960  ballotlemii  34961  ballotlemsima  34973  ballotlemfrcn0  34987  signsw0g  35010  signswmnd  35011  signstfvc  35028  prodfzo03  35057  reprval  35064  reprsum  35067  reprsuc  35069  reprpmtf1o  35080  axtgupdim2ALTV  35122  brafs  35129  bnj125  35327  bnj154  35333  bnj526  35343  bnj609  35372  bnj893  35383  bnj1321  35482  bnj1491  35512  nummin  35544  fineqvnttrclselem2  35594  fineqvnttrclselem3  35595  fineqvnttrclse  35596  noinfepfnregs  35604  kardcard2b  35637  subfacp1lem3  35713  subfacp1lem5  35715  subfacp1lem6  35716  cnpconn  35761  txpconn  35763  ptpconn  35764  indispconn  35765  connpconn  35766  cvxpconn  35773  cvmscbv  35789  cvmsi  35796  cvmsval  35797  cvmsdisj  35801  cvmsss2  35805  cvmliftmo  35815  cvmliftlem14  35828  cvmliftiota  35832  cvmlift2lem12  35845  cvmlift2lem13  35846  cvmlift2  35847  cvmliftphtlem  35848  cvmlift3lem2  35851  cvmlift3lem4  35853  cvmlift3lem6  35855  cvmlift3lem7  35856  cvmlift3lem9  35858  cvmlift3  35859  snmlval  35862  satffunlem  35932  prv1n  35962  mrsub0  36047  mrsubcn  36050  ismfs  36080  sinccvglem  36203  br6  36288  brbigcup  36427  imageval  36459  funpartlem  36473  dfrdg4  36482  altopthsn  36492  brsegle  36639  rankeq1o  36702  cbviotadavw  36840  subtr  36884  opnbnd  36895  cldbnd  36896  isfne  36909  topfneec  36925  neibastop3  36932  dfttc4lem1  37098  dfttc4lem2  37099  dfttc4  37100  elttcirr  37101  cnndvlem2  37186  bj-imdirval2  37886  bj-imdirid  37889  bj-imdirco  37893  bj-inftyexpiinj  37912  bj-isrvecd  38001  bj-isrvec2  38003  bj-bary1lem1  38014  bj-bary1  38015  qdiff  38030  finxp00  38107  nlpfvineqsn  38114  pibp19  38119  pibt2  38122  unccur  38313  matunitlindflem2  38327  ptrecube  38330  poimirlem4  38334  poimirlem19  38349  poimirlem23  38353  poimirlem25  38355  poimirlem27  38357  poimirlem28  38358  poimirlem31  38361  poimirlem32  38362  broucube  38364  mblfinlem2  38368  ovoliunnfl  38372  voliunnfl  38374  volsupnfl  38375  mbfresfi  38376  itg2addnclem  38381  itg2addnclem3  38383  itg2addnc  38384  ftc2nc  38412  cover2  38426  sdclem2  38453  fdc  38456  metf1o  38466  istotbnd3  38482  0totbnd  38484  sstotbnd2  38485  equivtotbnd  38489  totbndbnd  38500  prdstotbnd  38505  heibor1  38521  rrnmet  38540  isexid  38558  ismgmOLD  38561  opidonOLD  38563  exidu1  38567  cmpidelt  38570  exidreslem  38588  exidres  38589  exidresid  38590  grpoeqdivid  38592  elghomlem1OLD  38596  grpokerinj  38604  isrngo  38608  isrngod  38609  rngoideu  38614  isgrpda  38666  isdrngo2  38669  isdrngo3  38670  isrngohom  38676  divrngidl  38739  dmnnzd  38786  dmncan1  38787  disjeccnvep  38999  disjressuc2  39120  mopre  39180  qsdisjALTV  39408  dmqseqeq1  39436  unidmqseq  39449  disjdmqseq  39617  eldisjlem19  39622  riotasvd  39790  toycom  39807  islshpsm  39814  lshpnel2N  39819  lsatfixedN  39843  islshpat  39851  lcvexchlem4  39871  l1cvpat  39888  lkr0f  39928  lkrsc  39931  lshpkrlem1  39944  lkreqN  40004  isopos  40014  oposlem  40016  opcon2b  40031  cmtbr3N  40088  cvlcvrp  40174  hlrelat5N  40235  cvrval5  40249  cvrat4  40277  3atlem5  40321  2at0mat0  40359  psubclsetN  40770  4atex2  40911  isldil  40944  ltrnu  40955  ltrnid  40969  isdilN  40988  trlnid  41013  cdleme21k  41172  cdleme29b  41209  cdlemefrs29pre00  41229  cdlemefrs29bpre0  41230  cdlemefrs29cpre1  41232  cdleme32fva  41271  cdleme42b  41312  cdleme50ex  41393  cdleme  41394  cdlemg1a  41404  ltrniotaval  41415  cdlemeiota  41419  tendoid0  41659  cdlemksv2  41681  cdlemkuv2  41701  cdlemk36  41747  cdlemk42  41775  cdlemk  41808  tendoex  41809  cdleml3N  41812  cdleml5N  41814  tendospcanN  41857  cdlemm10N  41952  dihffval  42064  dihfval  42065  dihlsscpre  42068  islpolN  42317  mapdhval  42558  mapdheq  42562  hdmap1fval  42630  hdmap1val  42632  hdmap1eq  42635  hdmap1cbv  42636  hdmapval2lem  42665  hdmap11  42682  hdmap14lem2a  42701  hdmap14lem6  42707  hgmapval  42721  hlhillcs  42792  hlhilphllem  42793  aks4d1  42916  isprimroot  42920  mndmolinv  42922  linvh  42923  primrootsunit1  42924  primrootsunit  42925  primrootscoprmpow  42926  primrootscoprbij  42929  primrootlekpowne0  42932  primrootspoweq0  42933  ringexp0nn  42961  aks6d1c5lem1  42963  sticksstones8  42980  sticksstones9  42981  sticksstones10  42982  sticksstones11  42983  sticksstones12a  42984  sticksstones12  42985  sticksstones16  42989  sticksstones17  42990  sticksstones18  42991  sticksstones19  42992  aks6d1c6lem4  43000  aks6d1c6isolem3  43003  rhmqusspan  43012  grpods  43021  unitscyglem1  43022  unitscyglem2  43023  unitscyglem3  43024  unitscyglem5  43026  quadfac  43032  expeq1d  43145  zdivgd  43158  ef11d  43160  resubval  43188  renegadd  43193  resubeu  43198  resubadd  43200  sn-remul0ord  43229  sn-negex12  43238  addinvcom  43253  redivvald  43263  rediveud  43264  redivmuld  43266  sn-mul02  43286  mulgt0con1d  43304  mulgt0con2d  43305  fimgmcyclem  43361  fidomncyc  43363  fsuppind  43382  mhphflem  43388  prjspnfv01  43416  prjspner01  43417  prjspner1  43418  prjcrvval  43424  dffltz  43426  flt4lem7  43451  nna4b4nsq  43452  negexpidd  43473  mzpcompact2lem  43542  eldioph  43549  eldioph2lem1  43551  eldioph2lem2  43552  eldioph2  43553  eldioph2b  43554  eldioph3  43557  diophin  43563  diophun  43564  eq0rabdioph  43567  dvdsrabdioph  43597  eldioph4i  43599  diophren  43600  rabren3dioph  43602  fphpd  43603  pellexlem5  43620  pellexlem6  43621  pellex  43622  pell1qrval  43633  pell14qrval  43635  pell1234qrval  43637  pell1234qrreccl  43641  pell1234qrmulcl  43642  pell1234qrdich  43648  pell14qrdich  43656  pell1qr1  43658  pellqrexplicit  43664  rmxycomplete  43704  jm2.27  43795  rmydioph  43801  rmxdiophlem  43802  rmxdioph  43803  pw2f1ocnv  43824  pwssplit4  43876  elmnc  43923  dgraalem  43932  dgraaub  43935  dgraa0p  43936  mpaaeu  43937  mpaaval  43938  mpaalem  43939  aaitgo  43949  rngunsnply  43956  proot1ex  43983  cantnfresb  44111  tfsconcatfv  44128  tfsconcatb0  44131  tfsconcat0i  44132  tfsconcat0b  44133  tfsconcat00  44134  tfsconcatrev  44135  naddwordnexlem4  44188  sqrtcval  44427  relexpnul  44464  relexpxpnnidm  44489  relexpiidm  44490  trclfvdecomr  44514  rfovcnvf1od  44790  ntrkbimka  44824  ntrk0kbimka  44825  clsk3nimkb  44826  clsk1independent  44832  ntrclsfveq1  44846  ntrclsfveq2  44847  ntrclskb  44855  k0004val  44936  k0004val0  44940  mnringmulrcld  45012  expgrowth  45105  bcc0  45110  relpfrlem  45722  permac8prim  45783  disjinfi  45970  fsumf1of  46350  limsupmnflem  46494  liminfpnfuz  46590  climxlim2lem  46619  coseq0  46638  icccncfext  46661  dvnmptconst  46715  dvnprodlem1  46720  dvnprodlem2  46721  dvnprodlem3  46722  dvnprod  46723  stoweidlem15  46789  stoweidlem31  46805  stoweidlem35  46809  stoweidlem36  46810  stoweidlem37  46811  stoweidlem43  46817  stoweidlem44  46818  stoweidlem46  46820  stoweidlem55  46829  stoweidlem59  46833  dirkerval2  46868  dirkertrigeqlem1  46872  dirkeritg  46876  dirkercncf  46881  fourierdlem2  46883  fourierdlem3  46884  fourierdlem42  46923  fourierdlem71  46951  fourierdlem112  46992  fourierdlem113  46993  elaa2lem  47007  etransclem11  47019  etransclem24  47032  etransclem26  47034  etransclem28  47036  etransclem35  47043  ioorrnopnxr  47081  salgenval  47095  intsaluni  47103  salgenn0  47105  salgencl  47106  sssalgen  47109  salgenss  47110  salgenuni  47111  issalgend  47112  dfsalgen2  47115  subsaliuncl  47132  sge0f1o  47156  sge0fodjrnlem  47190  ismea  47225  nnfoctbdjlem  47229  iundjiun  47234  isome  47268  caragenel  47269  ovn0lem  47339  ovnsubaddlem1  47344  smflimlem4  47548  smflim  47551  sigarcol  47638  chnsubseqwl  47655  sqrtnnaa  47664  sqrtnzqaa  47665  cfsetsnfsetf  47855  cfsetsnfsetfo  47857  fnbrafvb  47951  afv2fv0  48062  readdcnnred  48100  resubcnnred  48101  cndivrenred  48103  nnmul2  48127  ceilbi  48134  minusmodnep2tmod  48156  modmkpkne  48164  nndivides2  48181  fargshiftf1  48250  fargshiftfo  48251  ichexmpl2  48279  ichnreuop  48281  ichreuopeq  48282  elsprel  48284  prproropf1olem4  48315  reupr  48331  reuopreuprim  48335  goldbachthlem2  48358  fmtnoprmfac2lem1  48378  fmtnofac2lem  48380  prmdvdsfmtnof1lem2  48397  mod42tp1mod8  48414  lighneallem2  48418  lighneallem3  48419  lighneallem4  48422  proththd  48426  41prothprm  48431  requad01  48446  requad2  48448  dfeven2  48474  dfeven5  48491  dfodd7  48492  fpprel  48553  fppr2odd  48556  fpprwppr  48564  fpprwpprb  48565  nnsum3primesgbe  48617  isubgredg  48691  upgrimpths  48734  ushggricedg  48752  uhgrimisgrgric  48756  isubgr3stgrlem3  48793  isubgr3stgrlem4  48794  isubgr3stgrlem6  48796  grlimprclnbgr  48821  grlimgrtrilem2  48827  gpgedgvtx0  48886  gpgedgvtx1  48887  gpgvtxedg0  48888  gpgvtxedg1  48889  gpg3kgrtriexlem5  48912  gpgprismgr4cycllem3  48922  pgnbgreunbgrlem2lem1  48939  pgnbgreunbgrlem2lem2  48940  pgnbgreunbgrlem2lem3  48941  upwlksfval  48960  0nodd  48994  2nodd  48996  nnsgrpnmnd  49002  nn0mnd  49003  lidldomn1  49055  zlidlring  49058  uzlidlring  49059  2zrngamgm  49069  2zrngamnd  49071  2zrngagrp  49073  2zrngnmlid2  49081  smprngprmrng  49163  idomnzd  49170  idomcanl  49171  ztprmneprm  49186  dmatALTbasel  49241  linindslinci  49287  lindslinindsimp1  49296  lindslinindimp2lem4  49300  lindslinindsimp2lem5  49301  linds0  49304  el0ldep  49305  lindsrng01  49307  snlindsntorlem  49309  snlindsntor  49310  ldepspr  49312  lincresunit3  49320  islindeps2  49322  isldepslvec2  49324  zlmodzxzldep  49343  blen1b  49427  dig2bits  49453  nn0sumshdiglem1  49460  0aryfvalelfv  49474  itcovalsuc  49506  prelrrx2b  49553  eenglngeehlnmlem1  49576  eenglngeehlnmlem2  49577  rrx2linest2  49583  elrrx2linest2  49584  spheres  49585  2sphere  49588  2sphere0  49589  line2ylem  49590  line2  49591  line2xlem  49592  line2x  49593  line2y  49594  itscnhlc0yqe  49598  itschlc0yqe  49599  itscnhlc0xyqsol  49604  itschlc0xyqsol1  49605  itsclc0xyqsolr  49608  itsclc0  49610  itsclc0b  49611  itsclinecirc0b  49613  itsclquadb  49615  itsclquadeu  49616  itscnhlinecirc02p  49624  resinsnALT  49710  sepnsepolem2  49760  sepnsepo  49761  sepfsepc  49765  iscnrm3rlem8  49784  iscnrm3r  49785  iscnrm3llem2  49787  iscnrm3l  49788  oppcendc  49855  isisod  49864  sectpropdlem  49873  ssccatid  49909  resccatlem  49910  imasubc  49988  uptrlem1  50047  oppcthinendcALT  50278  functhinclem2  50282  fullthinc2  50288  thincciso  50290  thinccisod  50291  termcpropd  50340  fulltermc2  50349  oduoppcciso  50403  discsnterm  50411  aacllem  50680