Theorem eqeq1d 2731

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 2722	. . . 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 2722	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
9		dfcleq 2722	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
10	7, 8, 9	3bitr4g 314	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eqeq1  2733  eqcomd  2735  eqeq2d  2740  eqeqan12d  2743  neeq1d  2984  rspcedeq1vd  3595  csbconstg  3881  csbhypf  3890  csbiebt  3891  csbiebg  3894  sbceq2g  4382  csbie2df  4406  disjeq0  4419  disjssun  4431  mosneq  4806  preq12b  4814  preq12bg  4817  elpreqprlem  4830  disji2  5091  invdisjrab  5094  disjprg  5103  disjxun  5105  iin0  5317  opthg  5437  opeqsng  5463  propeqop  5467  wefrc  5632  xpcan  6149  xpcan2  6150  dmsnopg  6186  rnmpt0f  6216  reuop  6266  dfpo2  6269  sspred  6283  onfr  6371  unisucg  6412  nsuceq0  6417  iotaeq  6476  iotabi  6477  fneq1  6609  fnun  6632  fnresdisj  6638  fnimadisj  6650  fnimaeq0  6651  foeq1  6768  fveqeq2d  6866  fvun1  6952  fvmptdv2  6986  fndmdifeq0  7016  fneqeql  7018  dffo3  7074  dffo3f  7078  fnnfpeq0  7152  foeqcnvco  7275  f1eqcocnv  7276  isofrlem  7315  eqfunresadj  7335  ovanraleqv  7411  f1opr  7445  eloprabga  7498  ovmpodv2  7547  ov3  7552  ovelimab  7567  caovcang  7590  caovcan  7593  caovmo  7626  caofinvl  7685  caofid1  7688  caofid2  7689  caofidlcan  7691  caonncan  7697  tfisi  7835  mptcnfimad  7965  oteqimp  7987  br1steqg  7990  br2ndeqg  7991  eqop  8010  reldm  8023  mposn  8082  fparlem1  8091  fparlem2  8092  fsplit  8096  frxp  8105  xporderlem  8106  fnwelem  8110  xpord2lem  8121  xpord3lem  8128  poseq  8137  soseq  8138  fnsuppeq0  8171  suppssov1  8176  suppssov2  8177  suppofss1d  8183  suppofss2d  8184  tposfo2  8228  mpocurryd  8248  iinon  8309  onnseq  8313  tz7.49  8413  seqomlem2  8419  oe0m1  8485  om0r  8503  oe1m  8509  oawordeulem  8518  oawordeu  8519  oarec  8526  omord  8532  oneo  8545  omeu  8549  oeeui  8566  nnm0r  8574  nnmord  8596  nnawordex  8601  nnaordex2  8603  nnneo  8619  nneob  8620  omopth  8626  nnasmo  8627  ereq1  8678  eqerlem  8706  qsdisj  8767  erov  8787  eceqoveq  8795  mapsnd  8859  endisj  9028  pw2f1olem  9045  enfixsn  9050  disjenex  9099  domssex2  9101  xpf1o  9103  mapxpen  9107  unxpdomlem2  9198  enp1ilem  9223  fodomfib  9280  fodomfibOLD  9282  fipreima  9309  opthreg  9571  cantnfp1lem3  9633  ssttrcl  9668  ttrcltr  9669  ttrclss  9673  ttrclselem2  9679  frmin  9702  updjud  9887  pm54.43  9954  dfac5  10082  dfacacn  10095  kmlem9  10112  cfeq0  10209  cfss  10218  cfslb  10219  fin23lem22  10280  fin23lem12  10284  fin23lem19  10289  fin23lem30  10295  fin23lem33  10298  fin1a2lem6  10358  axcc2lem  10389  axdc3lem2  10404  axdc3lem3  10405  axdc3lem4  10406  axdc3  10407  axdc4lem  10408  zorn2lem7  10455  ttukeylem3  10464  ttukeylem6  10467  ttukey2g  10469  fodomb  10479  axacndlem5  10564  fpwwe2cbv  10583  fpwwe2lem2  10585  fpwwe2lem3  10586  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe  10599  pwfseqlem2  10612  pwxpndom2  10618  addnidpi  10854  ltexpi  10855  recmulnq  10917  ltexnq  10928  halfnq  10929  archnq  10933  ltexpri  10996  recexpr  11004  addsrpr  11028  mulsrpr  11029  00sr  11052  negexsr  11055  recexsrlem  11056  recexsr  11060  axrnegex  11115  axrrecex  11116  00id  11349  mul02  11352  addrid  11354  cnegex  11355  cnegex2  11356  subval  11412  subadd  11424  subadd2  11425  subsub23  11426  addsubeq4  11436  subcan2  11447  negcon1  11474  subcan  11477  addrsub  11595  ltordlem  11703  ltord1  11704  recex  11810  mul0or  11818  muleqadd  11822  receu  11823  mulcan1g  11831  divval  11839  divmul  11840  rec11  11880  ldiv  12016  rdiv  12017  zdiv  12604  uzin  12833  xaddval  13183  xmulval  13185  xnn0xadd0  13207  xnegdi  13208  ioo0  13331  ico0  13352  ioc0  13353  icc0  13354  1fv  13608  fzon  13641  fvinim0ffz  13747  flbi  13778  mod0  13838  modmuladdnn0  13880  modirr  13907  addmodlteq  13911  uzrdgfni  13923  axdc4uzlem  13948  fsuppmapnn0fiubex  13957  mptnn0fsupp  13962  seqid  14012  seqz  14015  expval  14028  expeq0  14057  sqeqor  14181  nn0opth2  14237  hashdom  14344  elprchashprn2  14361  hashbc  14418  hashf1lem1  14420  hash2pwpr  14441  ccat0  14541  wrdl1s1  14579  ccatws1lenp1b  14586  pfxsuff1eqwrdeq  14664  swrdccatin2  14694  pfxccatin12lem2  14696  2cshwcshw  14791  scshwfzeqfzo  14792  cshimadifsn  14795  cshimadifsn0  14796  s2f1o  14882  wrdlen2i  14908  2swrd2eqwrdeq  14919  wwlktovf  14922  wwlktovf1  14923  wwlktovfo  14924  wrd2f1tovbij  14926  relexp0g  14988  relexpsucnnr  14991  dfrtrcl2  15028  mulre  15087  rennim  15205  cnpart  15206  01sqrex  15215  resqrex  15216  sqrmo  15217  resqrtcl  15219  resqrtthlem  15220  sqrtgt0  15224  sqrtneg  15233  sqrtsq2  15234  absmod0  15269  sqreulem  15326  sqreu  15327  sqrtthlem  15329  eqsqrtd  15334  reusq0  15431  fsum00  15764  telfsumo  15768  prodss  15913  fprodle  15962  tanaddlem  16134  absefib  16166  efieq1re  16167  divides  16224  dvdsval2  16225  nndivides  16232  dvds0lem  16236  dvds1lem  16237  dvds2lem  16238  negdvdsb  16242  muldvds1  16250  muldvds2  16251  dvdscmulr  16254  dvdsmulcr  16255  difmod0  16257  dvdstr  16264  dvdsabseq  16283  divconjdvds  16285  odd2np1lem  16310  odd2np1  16311  even2n  16312  oddm1even  16313  2tp1odd  16322  opeo  16335  omeo  16336  m1exp1  16346  divalglem4  16366  divalglem8  16370  divalgb  16374  bitsuz  16444  smupvallem  16453  gcdaddmlem  16494  gcdabs1  16499  bezoutlem3  16511  rplpwr  16528  rprpwr  16529  alginv  16545  algcvga  16549  algfx  16550  eucalgval2  16551  coprmdvds  16623  qredeq  16627  qredeu  16628  coprmprod  16631  coprmproddvdslem  16632  divgcdcoprm0  16635  divgcdcoprmex  16636  cncongr1  16637  rpexp  16692  rpexp12i  16694  cncongrprm  16699  qnumdenbi  16714  phival  16737  phicl2  16738  dfphi2  16744  phiprmpw  16746  phimullem  16749  eulerthlem1  16751  eulerthlem2  16752  eulerth  16753  fermltl  16754  hashgcdlem  16758  phisum  16761  odzval  16762  odzdvds  16766  reumodprminv  16775  modprm0  16776  nnnn0modprm0  16777  modprmn0modprm0  16778  coprimeprodsq  16779  coprimeprodsq2  16780  pythagtriplem2  16788  pythagtrip  16805  pcval  16815  pceulem  16816  pcqmul  16824  pcqcl  16827  pcabs  16846  pcgcd1  16848  pc2dvds  16850  pcaddlem  16859  pcadd  16860  pcmpt  16863  prmpwdvds  16875  pockthi  16878  unbenlem  16879  4sqlem12  16927  ramz  16996  ramcl  17000  cshwrepswhash1  17073  imasval  17474  fvprif  17524  iscat  17633  iscatd  17634  catidex  17635  catideu  17636  cidfval  17637  cidval  17638  catidd  17641  catlid  17644  catrid  17645  catpropd  17670  cidpropd  17671  issect  17715  dfiso2  17734  invcoisoid  17754  isocoinvid  17755  setcepi  18050  latleeqj2  18411  latleeqm2  18427  oduclatb  18466  mgmidmo  18587  grpidval  18588  grpidpropd  18589  ismgmid  18592  ismgmid2  18595  mgmidsssn0  18599  grpinvalem  18600  grprida  18602  gsumvalx  18603  gsumpropd  18605  gsumpropd2lem  18606  gsumress  18609  gsumval2  18613  ismnddef  18663  sgrpidmnd  18666  ismndd  18683  mndpropd  18686  mndinvmod  18691  mnd1  18706  ismhm  18712  gsumvallem2  18761  frmdgsum  18789  frmdup3  18794  efmndmnd  18816  smndex1mnd  18837  sgrp2rid2  18853  sgrp2rid2ex  18854  pwmnd  18864  grpinvex  18875  isgrpd2  18888  isgrpd  18890  dfgrp2  18894  grpinveu  18906  grpinvval  18912  grplinv  18921  isgrpinv  18925  grplrinv  18928  grpidinv2  18929  grpidinv  18930  grplmulf1o  18945  grpraddf1o  18946  grpsubeq0  18958  grpsubadd  18960  dfgrp3lem  18970  dfgrp3  18971  grp1  18979  imasgrp2  18987  qusgrp2  18990  mhmmnd  18996  ghmgrp  18998  mulgval  19003  mulgaddcom  19030  eqg0el  19115  cycsubmel  19132  ghmeqker  19175  ghmf1  19178  conjnmzb  19185  ghmqusker  19219  isga  19223  subgga  19232  gaorb  19239  gaorber  19240  gastacl  19241  gastacos  19242  orbsta  19245  symgfix2  19346  gsmsymgrfixlem1  19357  gsmsymgrfix  19358  gsmsymgreq  19362  symgfixelq  19363  f1omvdconj  19376  pmtrdifwrdel2  19416  psgnunilem1  19423  psgnunilem2  19425  psgnunilem3  19426  psgnunilem4  19427  odval  19464  odid  19468  odlem2  19469  oddvdsnn0  19474  odnncl  19475  oddvds  19477  odcong  19479  odeq  19480  odmulgid  19484  odmulgeq  19487  gexval  19508  gexid  19511  gexlem2  19512  gexdvdsi  19513  gexdvds  19514  subgpgp  19527  sylow1lem1  19528  sylow1lem4  19531  sylow2alem1  19547  sylow2alem2  19548  sylow2blem2  19551  sylow3lem6  19562  lsmdisj3a  19619  lsmdisj3b  19620  pj1val  19625  pj1eq  19630  efgredlemd  19674  efgredlem  19677  efgred  19678  efgrelexlema  19679  frgpup3  19708  ablsubadd  19739  ablsubsub23  19754  iscyggen  19810  cyggenod  19814  gsumval3lem2  19836  gsumval3  19837  gsummptnn0fz  19916  dmdprd  19930  dprddisj  19941  dprdfeq0  19954  dprdf11  19955  dmdprdpr  19981  dpjeq  19991  ablfacrp  19998  pgpfac1lem2  20007  pgpfac1lem3  20009  pgpfac1lem5  20011  pgpfac1  20012  pgpfaclem1  20013  pgpfaclem2  20014  pgpfaclem3  20015  ablfaclem2  20018  ablfaclem3  20019  ablfac2  20021  rngmneg1  20076  rngmneg2  20077  ringurd  20094  srgrz  20116  srglz  20117  srgisid  20118  srg1zr  20124  ringid  20183  qusring2  20243  opprring  20256  dvdsrval  20270  dvdsrmul  20273  dvdsr01  20280  dvdsr02  20281  crngunit  20287  ringunitnzdiv  20307  dvreq1  20320  dvdsrpropd  20325  irredn0  20332  irredrmul  20336  irredmul  20338  rngisomring  20376  rhmdvdsr  20417  lringuplu  20453  subrg1  20491  subrgdvds  20495  isrrg  20607  rrgeq0i  20608  rrgeq0  20609  domneq0  20617  isdomn4  20625  domnlcanb  20629  domnrcanb  20631  drngid2  20661  drngmul0orOLD  20670  isdrngd  20674  isdrngdOLD  20676  fidomndrnglem  20681  isabv  20720  issrngd  20764  islmod  20770  islmodd  20772  lmodprop2d  20830  mptscmfsupp0  20833  lss1d  20869  lspextmo  20963  lvecvs0or  21018  lvecvscan  21021  lvecvscan2  21022  lbsacsbs  21066  rngqiprngimf1lem  21204  rng2idl1cntr  21215  prmirredlem  21382  pzriprnglem7  21397  pzriprnglem13  21403  chrdvds  21436  chrnzr  21440  domnchr  21442  znval  21445  zncyg  21458  znfld  21470  znunit  21473  znrrg  21475  frgpcyg  21483  psgndiflemB  21509  psgndiflemA  21510  ipeq0  21547  ip2eq  21562  elocv  21577  ocvi  21578  obsne0  21634  dsmmacl  21650  dsmmlss  21653  frlmphl  21690  frlmup4  21710  islindf4  21747  islindf5  21748  mplsubrglem  21913  mplmon2  21968  evlslem1  21989  evlseu  21990  evlsval  21993  evlsval2  21994  ismhp3  22029  mhpsclcl  22034  mhpvarcl  22035  mhpmulcl  22036  psdmul  22053  psdmvr  22056  cply1coe0bi  22189  gsummoncoe1  22195  evl1vsd  22231  dmatel  22380  dmatelnd  22383  dmatmulcl  22387  scmateALT  22399  mdetdiaglem  22485  mdetunilem1  22499  mdetunilem3  22501  mdetunilem4  22502  mdetunilem9  22507  symgmatr01lem  22540  symgmatr01  22541  gsummatr01lem1  22542  gsummatr01lem4  22545  gsummatr01  22546  smadiadetlem3  22555  cramerlem3  22576  pmatcoe1fsupp  22588  cpmatel  22598  1elcpmat  22602  cpmatmcllem  22605  cpmatmcl  22606  d1mat2pmat  22626  m2cpminvid2lem  22641  m2cpminvid2  22642  decpmatmulsumfsupp  22660  pmatcollpw2lem  22664  pmatcollpwscmatlem1  22676  mp2pm2mplem4  22696  pm2mpmhmlem1  22705  chpscmat  22729  cpmidpmatlem3  22759  cayleyhamilton0  22776  cayleyhamiltonALT  22778  cayleyhamilton1  22779  0ntr  22958  ntreq0  22964  cldlp  23037  pnrmopn  23230  hausnei2  23240  cnhaus  23241  nrmsep  23244  isnrm2  23245  regsep2  23263  dishaus  23269  ordthauslem  23270  iscmp  23275  cmpsublem  23286  cmpsub  23287  tgcmp  23288  sscmp  23292  hauscmplem  23293  cmpfi  23295  bwth  23297  connsuba  23307  nconnsubb  23310  isref  23396  islocfin  23404  elpt  23459  elptr  23460  pthaus  23525  txcmp  23530  hausdiag  23532  txhaus  23534  txkgen  23539  xkohaus  23540  xkococnlem  23546  regr1lem  23626  fbasrn  23771  fmfnfmlem3  23843  flimtopon  23857  fclstopon  23899  alexsubb  23933  symgtgp  23993  qustgpopn  24007  qustgphaus  24010  ustuqtop  24134  isusp  24149  ispsmet  24192  psmet0  24196  ismet  24211  isxmet  24212  xmeteq0  24226  metn0  24248  xmetres2  24249  imasf1oxmet  24263  xblss2ps  24289  xblss2  24290  xmseq0  24352  comet  24401  stdbdxmet  24403  methaus  24408  dscmet  24460  nrmmetd  24462  nmeq0  24506  tngngp  24542  tngngp3  24544  nlmmul0or  24571  cnmet  24659  xrsxmet  24698  metnrmlem3  24750  icopnfcnv  24840  iccpnfcnv  24842  ishtpy  24871  isphtpy  24880  phtpyi  24883  om1elbas  24932  elpi1i  24946  pi1grplem  24949  isclmp  24997  cphsqrtcl2  25086  tcphcph  25137  bcth3  25231  rrxcph  25292  rrxmet  25308  ivth2  25356  iundisj2  25450  dyaddisj  25497  volivth  25508  mbfinf  25566  i1f1lem  25590  i1fmullem  25595  i1fmulclem  25603  i1fres  25606  itg1climres  25615  mbfi1fseqlem4  25619  dvnres  25833  dvcobr  25849  dvcobrOLD  25850  rolle  25894  cmvth  25895  cmvthOLD  25896  deg1leb  26000  ismon1p  26048  q1peqb  26061  dvdsr1p  26069  ply1remlem  26070  fta1glem2  26074  idomrootle  26078  elply2  26101  ne0p  26112  coeeu  26130  coelem  26131  coeeq  26132  dgrle  26148  coeaddlem  26154  plymul0or  26188  ofmulrt  26189  plydivlem3  26203  plydivlem4  26204  plydivex  26205  plydiveu  26206  plydivalg  26207  quotlem  26208  plyremlem  26212  quotcan  26217  plyexmo  26221  elqaalem3  26229  qaa  26231  iaa  26233  aareccl  26234  aacjcl  26235  aannenlem2  26237  reeff1o  26357  sineq0  26433  coseq1  26434  efeq1  26437  recosf1o  26444  logeftb  26492  cosarg0d  26518  logtayl  26569  cxpval  26573  cxpeq0  26587  root1eq1  26665  cxpeq  26667  logbgcd1irr  26704  angrtmuld  26718  affineequiv  26733  affineequiv3  26735  angpieqvdlem2  26739  quad2  26749  dcubic1lem  26753  dcubic2  26754  dcubic  26756  mcubic  26757  cubic2  26758  dquartlem1  26761  dquart  26763  quart  26771  atandm2  26787  atandm4  26789  atantan  26833  wilthlem2  26979  wilthlem3  26980  muval2  27044  isnsqf  27045  mumullem2  27090  sqff1o  27092  muinv  27103  mpodvdsmulf1o  27104  dvdsmulf1o  27106  dchrelbas2  27148  dchrmullid  27163  dchrfi  27166  lgsval  27212  lgsdir  27243  lgsne0  27246  lgsprme0  27250  lgsdirnn0  27255  lgsqrlem1  27257  lgsqr  27262  gausslemma2dlem0c  27269  gausslemma2dlem0i  27275  gausslemma2dlem7  27284  gausslemma2d  27285  lgseisenlem2  27287  lgsquadlem1  27291  lgsquadlem2  27292  lgsquad2lem2  27296  lgsquad3  27298  m1lgs  27299  2lgs  27318  2sqlem7  27335  2sqlem8  27337  2sqlem9  27338  2sqlem11  27340  2sq  27341  2sq2  27344  2sqmo  27348  addsq2reu  27351  addsqn2reu  27352  addsqrexnreu  27353  addsqnreup  27354  addsq2nreurex  27355  2sqreulem1  27357  2sqreultlem  27358  2sqreunnlem1  27360  2sqreunnltlem  27361  2sqreulem4  27365  2sqreuop  27373  2sqreuopnn  27374  2sqreuoplt  27375  2sqreuopltb  27376  2sqreuopnnlt  27377  2sqreuopnnltb  27378  2sqreuopb  27379  dchrisumlem1  27400  dchrvmaeq0  27415  dchrisum0re  27424  ostth3  27549  sltval  27559  nosepssdm  27598  nosupprefixmo  27612  noinfprefixmo  27613  nosupcbv  27614  nosupdm  27616  nosupfv  27618  nosupres  27619  nosupbnd1lem1  27620  nosupbnd1lem3  27622  nosupbnd1lem5  27624  noinfcbv  27629  noinfdm  27631  noinffv  27633  noinfres  27634  noinfbnd1lem3  27637  noinfbnd1lem5  27639  eqscut  27717  scutbdaylt  27730  made0  27785  madecut  27794  negsid  27947  negsex  27949  subadds  27974  divsmo  28087  muls0ord  28088  divsval  28092  norecdiv  28093  recsne0  28095  divsmulw  28096  divs1  28107  precsexlem8  28116  precsexlem9  28117  precsexlem11  28119  precsex  28120  recsex  28121  abssor  28148  elons  28154  noseqrdgfn  28200  bdayn0sf1o  28259  eucliddivs  28265  n0seo  28307  zseo  28308  nohalf  28310  expsne0  28321  pw2recs  28323  halfcut  28333  zs12negscl  28340  zs12ge0  28342  renegscl  28349  istrkg3ld  28388  axtgcgrid  28390  axtgsegcon  28391  axtg5seg  28392  axtgupdim2  28398  tgjustc1  28402  tgjustc2  28403  iscgrg  28439  isismt  28461  legov  28512  legov2  28513  hlcgreu  28545  mirreu3  28581  mircgr  28584  mirbtwn  28585  ismir  28586  mireq  28592  ismidb  28705  lmiopp  28729  dfcgra2  28757  inaghl  28772  f1otrg  28798  ttgval  28802  ttgelitv  28810  brbtwn  28826  brcgr  28827  colinearalglem2  28834  colinearalg  28837  axsegconlem1  28844  axsegcon  28854  ax5seglem4  28859  ax5seglem5  28860  axpaschlem  28867  axpasch  28868  axlowdimlem16  28884  axeuclidlem  28889  axeuclid  28890  axcontlem2  28892  axcontlem4  28894  axcontlem5  28895  edglnl  29070  usgredg2ALT  29120  usgredgprvALT  29122  usgrnloopvALT  29128  ushgredgedgloop  29158  edg0usgr  29180  nb3grpr  29309  cplgr1v  29357  cusgrsize  29382  vtxdgfval  29395  vtxdeqd  29405  vtxdun  29409  vtxd0nedgb  29416  vtxdusgr0edgnelALT  29424  1loopgrvd2  29431  usgruvtxvdb  29457  usgrvd0nedg  29461  vtxdginducedm1  29471  rusgrpropedg  29512  wksfval  29537  wlklenvclwlk  29583  iswlkon  29585  ispth  29651  dfpth2  29659  upgrwlkdvdelem  29666  crctcshwlkn0lem6  29745  wwlknon  29787  wwlksm1edg  29811  wwlksnextbi  29824  wwlksnextfun  29828  wwlksnextinj  29829  wwlksnextsurj  29830  wwlksnextbij  29832  wlksnwwlknvbij  29838  wwlksnextproplem3  29841  wwlksnextprop  29842  wspn0  29854  umgr2adedgwlkonALT  29877  umgr2adedgspth  29878  umgr2wlkon  29880  rusgrnumwwlkslem  29899  rusgrnumwwlkb0  29901  rusgrnumwwlks  29904  clwlkclwwlklem2a4  29926  clwlknf1oclwwlknlem2  30011  clwlknf1oclwwlkn  30013  isclwwlknon  30020  clwwlknon1loop  30027  s2elclwwlknon2  30033  clwwlknonwwlknonb  30035  clwwlkvbij  30042  uhgr3cyclex  30111  fusgreg2wsplem  30262  fusgr2wsp2nb  30263  fusgreghash2wsp  30267  frrusgrord0  30269  2clwwlkel  30278  extwwlkfab  30281  extwwlkfabel  30282  clwwlknonclwlknonf1o  30291  dlwwlknondlwlknonf1o  30294  wlkl0  30296  numclwwlk2lem1  30305  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  numclwwlk5  30317  ex-opab  30361  isgrpo  30426  isgrpoi  30427  grpoidinvlem3  30435  grpoideu  30438  gidval  30441  grpoidinv2  30444  grpoinveu  30448  grpoinvval  30452  grpoinv  30454  vciOLD  30490  isvclem  30506  cnidOLD  30511  isnvlem  30539  nvmul0or  30579  imsmetlem  30619  diporthcom  30645  ipz  30648  nmlno0  30724  ajfval  30738  hmoval  30739  isphg  30746  isph  30751  ip2eqi  30785  ajval  30790  hvmul0or  30954  hvsubeq0  30997  hvaddeq0  30998  hvaddcan  30999  hvmulcan  31001  hvmulcan2  31002  hvsubadd  31006  his6  31028  hial0  31031  hial02  31032  hi2eq  31034  orthcom  31037  normlem7tALT  31048  normsub0  31065  normpyth  31074  hilid  31090  hhssnv  31193  ocel  31210  ocsh  31212  ocorth  31220  ocin  31225  occllem  31232  choc0  31255  pjpreeq  31327  omlsi  31333  pjoc1  31363  pjoml  31365  pjoc2  31368  chm0  31420  chocin  31424  chlejb1  31441  chlejb2  31442  chjo  31444  h1deoi  31478  h1de2i  31482  pjoml6i  31518  pjoml2  31540  pjoml3  31541  pjch  31623  hodsi  31704  hodid  31721  eigorth  31767  elunop  31801  adjeu  31818  adjval  31819  eigvecval  31825  unopf1o  31845  adj1  31862  adjeq  31864  hmdmadj  31869  lnopeq0i  31936  lnopeqi  31937  lnopeq  31938  lnfn0  31976  riesz4i  31992  riesz4  31993  riesz1  31994  cnlnadjlem3  31998  cnlnadjlem5  32000  cnlnadjeu  32007  cnlnssadj  32009  nmopadjlei  32017  opsqrlem1  32069  hmopidmpji  32081  pjimai  32105  isst  32142  ishst  32143  hstel2  32148  stadd3i  32177  stri  32186  largei  32196  golem2  32201  superpos  32283  sumdmdii  32344  mddmdin0i  32360  opreu2reuALT  32406  difeq  32447  elim2if  32473  disji2f  32506  disjif2  32510  disjxpin  32517  iundisj2f  32519  disjunsn  32523  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  fxpval  33122  fxpgaeq  33126  cntrval2  33128  isslmd  33155  slmdlema  33156  urpropd  33183  elrgspnlem4  33196  elrgspnsubrunlem2  33199  erlcl1  33211  erlcl2  33212  erldi  33213  erlbrd  33214  erler  33216  rloccring  33221  domnlcanOLD  33230  isdrng4  33245  fracerl  33256  fracfld  33258  resv1r  33311  islinds5  33338  linds2eq  33352  dvdsruassoi  33355  dvdsruasso  33356  dvdsruasso2  33357  quslsm  33376  rhmimaidl  33403  qsidomlem2  33424  ssdifidllem  33427  ssdifidl  33428  ssdifidlprm  33429  opprqus0g  33461  qsdrngilem  33465  unitmulrprm  33499  1arithidom  33508  1arithufdlem3  33517  1arithufdlem4  33518  ply1dg1rt  33548  r1pid2OLD  33574  lbsdiflsp0  33622  fedgmullem1  33625  fedgmullem2  33626  irngss  33682  irngnzply1lem  33685  ply1annidllem  33691  ply1annnr  33693  minplymindeg  33698  minplyann  33699  minplyirredlem  33700  minplyirred  33701  irngnminplynz  33702  minplyelirng  33705  irredminply  33706  algextdeglem6  33712  algextdeglem7  33713  rtelextdg2lem  33716  fldext2chn  33718  constrsuc  33728  constrsslem  33731  constrconj  33735  constrextdg2lem  33738  constrextdg2  33739  constrlccllem  33743  constrcccllem  33744  constrcbvlem  33745  constrext2chn  33749  constrcon  33764  1smat1  33794  iscref  33834  metidval  33880  metidv  33882  metider  33884  pstmxmet  33887  xrmulc1cn  33920  esumfsup  34060  esumpcvgval  34068  esumcvg  34076  inelsros  34168  diffiunisros  34169  ismeas  34189  isrnmeas  34190  brae  34231  braew  34232  dya2iocuni  34274  elcarsg  34296  eulerpartleme  34354  eulerpartlemv  34355  eulerpartlemb  34359  eulerpartgbij  34363  eulerpartlemr  34365  eulerpartlemgvv  34367  eulerpartlemgh  34369  eulerpartlemn  34372  elprob  34400  ballotlemi  34492  ballotlemi1  34494  ballotlemii  34495  ballotlemsima  34507  ballotlemfrcn0  34521  signsw0g  34547  signswmnd  34548  signstfvc  34565  prodfzo03  34594  reprval  34601  reprsum  34604  reprsuc  34606  reprpmtf1o  34617  axtgupdim2ALTV  34659  brafs  34663  bnj125  34862  bnj154  34868  bnj526  34878  bnj609  34907  bnj893  34918  bnj1321  35017  bnj1491  35047  nummin  35081  subgrwlk  35119  loop1cycl  35124  subfacp1lem3  35169  subfacp1lem5  35171  subfacp1lem6  35172  cnpconn  35217  txpconn  35219  ptpconn  35220  indispconn  35221  connpconn  35222  cvxpconn  35229  cvmscbv  35245  cvmsi  35252  cvmsval  35253  cvmsdisj  35257  cvmsss2  35261  cvmliftmo  35271  cvmliftlem14  35284  cvmliftiota  35288  cvmlift2lem12  35301  cvmlift2lem13  35302  cvmlift2  35303  cvmliftphtlem  35304  cvmlift3lem2  35307  cvmlift3lem4  35309  cvmlift3lem6  35311  cvmlift3lem7  35312  cvmlift3lem9  35314  cvmlift3  35315  snmlval  35318  satffunlem  35388  prv1n  35418  mrsub0  35503  mrsubcn  35506  ismfs  35536  sinccvglem  35659  br6  35744  brbigcup  35886  imageval  35918  funpartlem  35930  dfrdg4  35939  altopthsn  35949  brsegle  36096  rankeq1o  36159  cbviotadavw  36257  subtr  36302  opnbnd  36313  cldbnd  36314  isfne  36327  topfneec  36343  neibastop3  36350  cnndvlem2  36526  bj-imdirval2  37171  bj-imdirid  37174  bj-imdirco  37178  bj-inftyexpiinj  37197  bj-isrvecd  37286  bj-isrvec2  37288  bj-bary1lem1  37299  bj-bary1  37300  finxp00  37390  nlpfvineqsn  37397  pibp19  37402  pibt2  37405  unccur  37597  matunitlindflem2  37611  ptrecube  37614  poimirlem4  37618  poimirlem19  37633  poimirlem23  37637  poimirlem25  37639  poimirlem27  37641  poimirlem28  37642  poimirlem31  37645  poimirlem32  37646  broucube  37648  mblfinlem2  37652  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  mbfresfi  37660  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  ftc2nc  37696  cover2  37709  sdclem2  37736  fdc  37739  metf1o  37749  istotbnd3  37765  0totbnd  37767  sstotbnd2  37768  equivtotbnd  37772  totbndbnd  37783  prdstotbnd  37788  heibor1  37804  rrnmet  37823  isexid  37841  ismgmOLD  37844  opidonOLD  37846  exidu1  37850  cmpidelt  37853  exidreslem  37871  exidres  37872  exidresid  37873  grpoeqdivid  37875  elghomlem1OLD  37879  grpokerinj  37887  isrngo  37891  isrngod  37892  rngoideu  37897  isgrpda  37949  isdrngo2  37952  isdrngo3  37953  isrngohom  37959  divrngidl  38022  dmnnzd  38069  dmncan1  38070  disjeccnvep  38272  disjressuc2  38374  qsdisjALTV  38606  dmqseqeq1  38634  unidmqseq  38647  disjdmqseq  38797  eldisjlem19  38802  riotasvd  38949  toycom  38966  islshpsm  38973  lshpnel2N  38978  lsatfixedN  39002  islshpat  39010  lcvexchlem4  39030  l1cvpat  39047  lkr0f  39087  lkrsc  39090  lshpkrlem1  39103  lkreqN  39163  isopos  39173  oposlem  39175  opcon2b  39190  cmtbr3N  39247  cvlcvrp  39333  hlrelat5N  39395  cvrval5  39409  cvrat4  39437  3atlem5  39481  2at0mat0  39519  psubclsetN  39930  4atex2  40071  isldil  40104  ltrnu  40115  ltrnid  40129  isdilN  40148  trlnid  40173  cdleme21k  40332  cdleme29b  40369  cdlemefrs29pre00  40389  cdlemefrs29bpre0  40390  cdlemefrs29cpre1  40392  cdleme32fva  40431  cdleme42b  40472  cdleme50ex  40553  cdleme  40554  cdlemg1a  40564  ltrniotaval  40575  cdlemeiota  40579  tendoid0  40819  cdlemksv2  40841  cdlemkuv2  40861  cdlemk36  40907  cdlemk42  40935  cdlemk  40968  tendoex  40969  cdleml3N  40972  cdleml5N  40974  tendospcanN  41017  cdlemm10N  41112  dihffval  41224  dihfval  41225  dihlsscpre  41228  islpolN  41477  mapdhval  41718  mapdheq  41722  hdmap1fval  41790  hdmap1val  41792  hdmap1eq  41795  hdmap1cbv  41796  hdmapval2lem  41825  hdmap11  41842  hdmap14lem2a  41861  hdmap14lem6  41867  hgmapval  41881  hlhillcs  41952  hlhilphllem  41953  aks4d1  42077  isprimroot  42081  mndmolinv  42083  linvh  42084  primrootsunit1  42085  primrootsunit  42086  primrootscoprmpow  42087  primrootscoprbij  42090  primrootlekpowne0  42093  primrootspoweq0  42094  ringexp0nn  42122  aks6d1c5lem1  42124  sticksstones8  42141  sticksstones9  42142  sticksstones10  42143  sticksstones11  42144  sticksstones12a  42145  sticksstones12  42146  sticksstones16  42150  sticksstones17  42151  sticksstones18  42152  sticksstones19  42153  aks6d1c6lem4  42161  aks6d1c6isolem3  42164  rhmqusspan  42173  grpods  42182  unitscyglem1  42183  unitscyglem2  42184  unitscyglem3  42185  unitscyglem5  42187  expeq1d  42312  zdivgd  42325  ef11d  42327  resubval  42355  renegadd  42360  resubeu  42365  resubadd  42367  sn-remul0ord  42396  sn-negex12  42405  addinvcom  42420  redivvald  42430  rediveud  42431  redivmuld  42433  sn-mul02  42440  mulgt0con1d  42458  mulgt0con2d  42459  fimgmcyclem  42521  fidomncyc  42523  evlsval3  42547  fsuppind  42578  mhphflem  42584  prjspnfv01  42612  prjspner01  42613  prjspner1  42614  prjcrvval  42620  dffltz  42622  flt4lem7  42647  nna4b4nsq  42648  negexpidd  42670  mzpcompact2lem  42739  eldioph  42746  eldioph2lem1  42748  eldioph2lem2  42749  eldioph2  42750  eldioph2b  42751  eldioph3  42754  diophin  42760  diophun  42761  eq0rabdioph  42764  dvdsrabdioph  42798  eldioph4i  42800  diophren  42801  rabren3dioph  42803  fphpd  42804  pellexlem5  42821  pellexlem6  42822  pellex  42823  pell1qrval  42834  pell14qrval  42836  pell1234qrval  42838  pell1234qrreccl  42842  pell1234qrmulcl  42843  pell1234qrdich  42849  pell14qrdich  42857  pell1qr1  42859  pellqrexplicit  42865  rmxycomplete  42906  jm2.27  42997  rmydioph  43003  rmxdiophlem  43004  rmxdioph  43005  pw2f1ocnv  43026  pwssplit4  43078  elmnc  43125  dgraalem  43134  dgraaub  43137  dgraa0p  43138  mpaaeu  43139  mpaaval  43140  mpaalem  43141  aaitgo  43151  rngunsnply  43158  proot1ex  43185  cantnfresb  43313  tfsconcatfv  43330  tfsconcatb0  43333  tfsconcat0i  43334  tfsconcat0b  43335  tfsconcat00  43336  tfsconcatrev  43337  naddwordnexlem4  43390  sqrtcval  43630  relexpnul  43667  relexpxpnnidm  43692  relexpiidm  43693  trclfvdecomr  43717  rfovcnvf1od  43993  ntrkbimka  44027  ntrk0kbimka  44028  clsk3nimkb  44029  clsk1independent  44035  ntrclsfveq1  44049  ntrclsfveq2  44050  ntrclskb  44058  k0004val  44139  k0004val0  44143  mnringmulrcld  44217  expgrowth  44324  bcc0  44329  relpfrlem  44943  permac8prim  45004  disjinfi  45186  fsumf1of  45572  limsupmnflem  45718  liminfpnfuz  45814  climxlim2lem  45843  coseq0  45862  icccncfext  45885  dvnmptconst  45939  dvnprodlem1  45944  dvnprodlem2  45945  dvnprodlem3  45946  dvnprod  45947  stoweidlem15  46013  stoweidlem31  46029  stoweidlem35  46033  stoweidlem36  46034  stoweidlem37  46035  stoweidlem43  46041  stoweidlem44  46042  stoweidlem46  46044  stoweidlem55  46053  stoweidlem59  46057  dirkerval2  46092  dirkertrigeqlem1  46096  dirkeritg  46100  dirkercncf  46105  fourierdlem2  46107  fourierdlem3  46108  fourierdlem42  46147  fourierdlem48  46152  fourierdlem49  46153  fourierdlem71  46175  fourierdlem112  46216  fourierdlem113  46217  elaa2lem  46231  etransclem11  46243  etransclem24  46256  etransclem26  46258  etransclem28  46260  etransclem35  46267  ioorrnopnxr  46305  salgenval  46319  intsaluni  46327  salgenn0  46329  salgencl  46330  sssalgen  46333  salgenss  46334  salgenuni  46335  issalgend  46336  dfsalgen2  46339  subsaliuncl  46356  sge0f1o  46380  sge0fodjrnlem  46414  ismea  46449  nnfoctbdjlem  46453  iundjiun  46458  isome  46492  caragenel  46493  ovn0lem  46563  ovnsubaddlem1  46568  smflimlem4  46772  smflim  46775  sigarcol  46862  cfsetsnfsetf  47059  cfsetsnfsetfo  47061  fnbrafvb  47155  afv2fv0  47266  readdcnnred  47304  resubcnnred  47305  cndivrenred  47307  ceilbi  47334  minusmodnep2tmod  47354  modmkpkne  47362  fargshiftf1  47442  fargshiftfo  47443  ichexmpl2  47471  ichnreuop  47473  ichreuopeq  47474  elsprel  47476  prproropf1olem4  47507  reupr  47523  reuopreuprim  47527  goldbachthlem2  47547  fmtnoprmfac2lem1  47567  fmtnofac2lem  47569  prmdvdsfmtnof1lem2  47586  mod42tp1mod8  47603  lighneallem2  47607  lighneallem3  47608  lighneallem4  47611  proththd  47615  41prothprm  47620  requad01  47622  requad2  47624  dfeven2  47650  dfeven5  47667  dfodd7  47668  fpprel  47729  fppr2odd  47732  fpprwppr  47740  fpprwpprb  47741  nnsum3primesgbe  47793  isubgredg  47866  upgrimpths  47909  ushggricedg  47927  uhgrimisgrgric  47931  isubgr3stgrlem3  47967  isubgr3stgrlem4  47968  isubgr3stgrlem6  47970  grlimgrtrilem2  47994  gpgedgvtx0  48052  gpgedgvtx1  48053  gpgvtxedg0  48054  gpgvtxedg1  48055  gpg3kgrtriexlem5  48078  gpgprismgr4cycllem3  48087  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  upwlksfval  48123  0nodd  48158  2nodd  48160  nnsgrpnmnd  48166  nn0mnd  48167  lidldomn1  48219  zlidlring  48222  uzlidlring  48223  2zrngamgm  48233  2zrngamnd  48235  2zrngagrp  48237  2zrngnmlid2  48245  ztprmneprm  48335  dmatALTbasel  48391  linindslinci  48437  lindslinindsimp1  48446  lindslinindimp2lem4  48450  lindslinindsimp2lem5  48451  linds0  48454  el0ldep  48455  lindsrng01  48457  snlindsntorlem  48459  snlindsntor  48460  ldepspr  48462  lincresunit3  48470  islindeps2  48472  isldepslvec2  48474  zlmodzxzldep  48493  blen1b  48577  dig2bits  48603  nn0sumshdiglem1  48610  0aryfvalelfv  48624  itcovalsuc  48656  prelrrx2b  48703  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  rrx2linest2  48733  elrrx2linest2  48734  spheres  48735  2sphere  48738  2sphere0  48739  line2ylem  48740  line2  48741  line2xlem  48742  line2x  48743  line2y  48744  itscnhlc0yqe  48748  itschlc0yqe  48749  itscnhlc0xyqsol  48754  itschlc0xyqsol1  48755  itsclc0xyqsolr  48758  itsclc0  48760  itsclc0b  48761  itsclinecirc0b  48763  itsclquadb  48765  itsclquadeu  48766  itscnhlinecirc02p  48774  resinsnALT  48861  sepnsepolem2  48911  sepnsepo  48912  sepfsepc  48916  iscnrm3rlem8  48935  iscnrm3r  48936  iscnrm3llem2  48938  iscnrm3l  48939  oppcendc  49007  isisod  49016  sectpropdlem  49025  ssccatid  49061  resccatlem  49062  imasubc  49140  uptrlem1  49199  oppcthinendcALT  49430  functhinclem2  49434  fullthinc2  49440  thincciso  49442  thinccisod  49443  termcpropd  49492  fulltermc2  49501  oduoppcciso  49555  discsnterm  49563  aacllem  49790