Theorem eqeq1d 2728

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 2719	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	biimpi 215	. . 3 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		bibi1 350	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	alimi 1806	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		albi 1813	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)) → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
7	1, 3, 5, 6	4syl 19	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
8		dfcleq 2719	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
9		dfcleq 2719	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
10	7, 8, 9	3bitr4g 313	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1532   = wceq 1534   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718

This theorem is referenced by:  eqeq1  2730  eqcomd  2732  eqeq2d  2737  eqeqan12d  2740  neeq1d  2990  rspcedeq1vd  3615  csbconstg  3911  csbhypf  3921  csbiebt  3922  csbiebg  3925  sbceq2g  4414  csbie2df  4438  disjeq0  4451  disjssun  4463  mosneq  4842  preq12b  4850  preq12bg  4853  elpreqprlem  4865  disji2  5128  invdisjrab  5131  disjprg  5140  disjxun  5142  iin0  5357  opthg  5474  opeqsng  5500  propeqop  5504  wefrc  5667  xpcan  6178  xpcan2  6179  dmsnopg  6215  rnmpt0f  6245  reuop  6295  dfpo2  6298  sspred  6312  onfr  6405  unisucg  6444  nsuceq0  6449  iotaeq  6509  iotabi  6510  fneq1  6641  fnun  6664  fnresdisj  6671  fnimadisj  6683  fnimaeq0  6684  foeq1  6801  fveqeq2d  6899  fvun1  6983  fvmptdv2  7017  fndmdifeq0  7047  fneqeql  7049  dffo3  7106  dffo3f  7110  fnnfpeq0  7182  foeqcnvco  7304  f1eqcocnv  7305  isofrlem  7342  eqfunresadj  7362  ovanraleqv  7438  f1opr  7471  eloprabga  7523  eloprabgaOLD  7524  ovmpodv2  7574  ov3  7579  ovelimab  7594  caovcang  7617  caovcan  7620  caovmo  7653  caofinvl  7711  caofid1  7714  caofid2  7715  caonncan  7722  tfisi  7859  mptcnfimad  7990  oteqimp  8012  br1steqg  8015  br2ndeqg  8016  eqop  8035  reldm  8048  mposn  8107  fparlem1  8116  fparlem2  8117  fsplit  8121  frxp  8130  xporderlem  8131  fnwelem  8135  xpord2lem  8146  xpord3lem  8153  poseq  8162  soseq  8163  fnsuppeq0  8196  suppssov1  8202  suppssov2  8203  suppofss1d  8209  suppofss2d  8210  tposfo2  8254  mpocurryd  8274  iinon  8360  onnseq  8364  tz7.49  8465  seqomlem2  8471  oe0m1  8541  om0r  8559  oe1m  8565  oawordeulem  8574  oawordeu  8575  oarec  8582  omord  8588  oneo  8601  omeu  8605  oeeui  8622  nnm0r  8630  nnmord  8652  nnawordex  8657  nnaordex2  8659  nnneo  8675  nneob  8676  omopth  8682  nnasmo  8683  ereq1  8731  eqerlem  8759  qsdisj  8813  erov  8833  eceqoveq  8841  mapsnd  8905  endisj  9086  pw2f1olem  9104  enfixsn  9109  disjenex  9163  domssex2  9165  xpf1o  9167  mapxpen  9171  unxpdomlem2  9276  enp1ilem  9303  fodomfib  9362  fodomfibOLD  9364  fipreima  9393  opthreg  9652  cantnfp1lem3  9714  ssttrcl  9749  ttrcltr  9750  ttrclss  9754  ttrclselem2  9760  frmin  9783  updjud  9968  pm54.43  10035  dfac5  10162  dfacacn  10175  kmlem9  10192  cfeq0  10288  cfss  10297  cfslb  10298  fin23lem22  10359  fin23lem12  10363  fin23lem19  10368  fin23lem30  10374  fin23lem33  10377  fin1a2lem6  10437  axcc2lem  10468  axdc3lem2  10483  axdc3lem3  10484  axdc3lem4  10485  axdc3  10486  axdc4lem  10487  zorn2lem7  10534  ttukeylem3  10543  ttukeylem6  10546  ttukey2g  10548  fodomb  10558  axacndlem5  10643  fpwwe2cbv  10662  fpwwe2lem2  10664  fpwwe2lem3  10665  fpwwe2lem11  10673  fpwwe2lem12  10674  fpwwe  10678  pwfseqlem2  10691  pwxpndom2  10697  addnidpi  10933  ltexpi  10934  recmulnq  10996  ltexnq  11007  halfnq  11008  archnq  11012  ltexpri  11075  recexpr  11083  addsrpr  11107  mulsrpr  11108  00sr  11131  negexsr  11134  recexsrlem  11135  recexsr  11139  axrnegex  11194  axrrecex  11195  00id  11428  mul02  11431  addrid  11433  cnegex  11434  cnegex2  11435  subval  11490  subadd  11502  subadd2  11503  subsub23  11504  addsubeq4  11514  subcan2  11524  negcon1  11551  subcan  11554  addrsub  11670  ltordlem  11778  ltord1  11779  recex  11885  mul0or  11893  muleqadd  11897  receu  11898  mulcan1g  11906  divval  11914  divmul  11915  rec11  11955  ldiv  12091  rdiv  12092  zdiv  12676  uzin  12906  xaddval  13248  xmulval  13250  xnn0xadd0  13272  xnegdi  13273  ioo0  13395  ico0  13416  ioc0  13417  icc0  13418  1fv  13666  fzon  13699  fvinim0ffz  13798  flbi  13828  mod0  13888  modmuladdnn0  13927  modirr  13954  addmodlteq  13958  uzrdgfni  13970  axdc4uzlem  13995  fsuppmapnn0fiubex  14004  mptnn0fsupp  14009  seqid  14059  seqz  14062  expval  14075  expeq0  14104  sqeqor  14226  nn0opth2  14282  hashdom  14389  elprchashprn2  14406  hashbc  14463  hashf1lem1  14466  hashf1lem1OLD  14467  hash2pwpr  14488  ccat0  14577  wrdl1s1  14615  ccatws1lenp1b  14622  pfxsuff1eqwrdeq  14700  swrdccatin2  14730  pfxccatin12lem2  14732  2cshwcshw  14827  scshwfzeqfzo  14828  cshimadifsn  14831  cshimadifsn0  14832  s2f1o  14918  wrdlen2i  14944  2swrd2eqwrdeq  14955  wwlktovf  14958  wwlktovf1  14959  wwlktovfo  14960  wrd2f1tovbij  14962  relexp0g  15020  relexpsucnnr  15023  dfrtrcl2  15060  mulre  15119  rennim  15237  cnpart  15238  01sqrex  15247  resqrex  15248  sqrmo  15249  resqrtcl  15251  resqrtthlem  15252  sqrtgt0  15256  sqrtneg  15265  sqrtsq2  15266  absmod0  15301  sqreulem  15357  sqreu  15358  sqrtthlem  15360  eqsqrtd  15365  reusq0  15460  fsum00  15795  telfsumo  15799  prodss  15942  fprodle  15991  tanaddlem  16161  absefib  16193  efieq1re  16194  divides  16251  dvdsval2  16252  nndivides  16259  dvds0lem  16262  dvds1lem  16263  dvds2lem  16264  negdvdsb  16268  muldvds1  16276  muldvds2  16277  dvdscmulr  16280  dvdsmulcr  16281  dvdstr  16289  dvdsabseq  16308  divconjdvds  16310  odd2np1lem  16335  odd2np1  16336  even2n  16337  oddm1even  16338  2tp1odd  16347  opeo  16360  omeo  16361  m1exp1  16371  divalglem4  16391  divalglem8  16395  divalgb  16399  bitsuz  16467  smupvallem  16476  gcdaddmlem  16517  gcdabs1  16522  bezoutlem3  16535  rplpwr  16552  rprpwr  16553  alginv  16569  algcvga  16573  algfx  16574  eucalgval2  16575  coprmdvds  16647  qredeq  16651  qredeu  16652  coprmprod  16655  coprmproddvdslem  16656  divgcdcoprm0  16659  divgcdcoprmex  16660  cncongr1  16661  rpexp  16717  rpexp12i  16719  cncongrprm  16724  qnumdenbi  16739  phival  16762  phicl2  16763  dfphi2  16769  phiprmpw  16771  phimullem  16774  eulerthlem1  16776  eulerthlem2  16777  eulerth  16778  fermltl  16779  hashgcdlem  16783  phisum  16785  odzval  16786  odzdvds  16790  reumodprminv  16799  modprm0  16800  nnnn0modprm0  16801  modprmn0modprm0  16802  coprimeprodsq  16803  coprimeprodsq2  16804  pythagtriplem2  16812  pythagtrip  16829  pcval  16839  pceulem  16840  pcqmul  16848  pcqcl  16851  pcabs  16870  pcgcd1  16872  pc2dvds  16874  pcaddlem  16883  pcadd  16884  pcmpt  16887  prmpwdvds  16899  pockthi  16902  unbenlem  16903  4sqlem12  16951  ramz  17020  ramcl  17024  cshwrepswhash1  17098  imasval  17519  fvprif  17569  iscat  17678  iscatd  17679  catidex  17680  catideu  17681  cidfval  17682  cidval  17683  catidd  17686  catlid  17689  catrid  17690  catpropd  17715  cidpropd  17716  issect  17762  dfiso2  17781  invcoisoid  17801  isocoinvid  17802  setcepi  18103  latleeqj2  18470  latleeqm2  18486  oduclatb  18525  mgmidmo  18646  grpidval  18647  grpidpropd  18648  ismgmid  18651  ismgmid2  18654  mgmidsssn0  18658  grpinvalem  18659  grprida  18661  gsumvalx  18662  gsumpropd  18664  gsumpropd2lem  18665  gsumress  18668  gsumval2  18672  ismnddef  18722  sgrpidmnd  18725  ismndd  18742  mndpropd  18745  mndinvmod  18750  mnd1  18762  ismhm  18768  gsumvallem2  18817  frmdgsum  18845  frmdup3  18850  efmndmnd  18872  smndex1mnd  18893  sgrp2rid2  18909  sgrp2rid2ex  18910  pwmnd  18920  grpinvex  18931  isgrpd2  18944  isgrpd  18946  dfgrp2  18950  grpinveu  18962  grpinvval  18968  grplinv  18977  isgrpinv  18981  grplrinv  18984  grpidinv2  18985  grpidinv  18986  grplmulf1o  19001  grpraddf1o  19002  grpsubeq0  19014  grpsubadd  19016  dfgrp3lem  19026  dfgrp3  19027  grp1  19035  imasgrp2  19043  qusgrp2  19046  mhmmnd  19052  ghmgrp  19054  mulgval  19059  mulgaddcom  19086  eqg0el  19171  cycsubmel  19188  ghmeqker  19231  ghmf1  19234  conjnmzb  19241  ghmqusker  19275  isga  19279  subgga  19288  gaorb  19295  gaorber  19296  gastacl  19297  gastacos  19298  orbsta  19301  symgfix2  19408  gsmsymgrfixlem1  19419  gsmsymgrfix  19420  gsmsymgreq  19424  symgfixelq  19425  f1omvdconj  19438  pmtrdifwrdel2  19478  psgnunilem1  19485  psgnunilem2  19487  psgnunilem3  19488  psgnunilem4  19489  odval  19526  odid  19530  odlem2  19531  oddvdsnn0  19536  odnncl  19537  oddvds  19539  odcong  19541  odeq  19542  odmulgid  19546  odmulgeq  19549  gexval  19570  gexid  19573  gexlem2  19574  gexdvdsi  19575  gexdvds  19576  subgpgp  19589  sylow1lem1  19590  sylow1lem4  19593  sylow2alem1  19609  sylow2alem2  19610  sylow2blem2  19613  sylow3lem6  19624  lsmdisj3a  19681  lsmdisj3b  19682  pj1val  19687  pj1eq  19692  efgredlemd  19736  efgredlem  19739  efgred  19740  efgrelexlema  19741  frgpup3  19770  ablsubadd  19801  ablsubsub23  19816  iscyggen  19872  cyggenod  19876  gsumval3lem2  19898  gsumval3  19899  gsummptnn0fz  19978  dmdprd  19992  dprddisj  20003  dprdfeq0  20016  dprdf11  20017  dmdprdpr  20043  dpjeq  20053  ablfacrp  20060  pgpfac1lem2  20069  pgpfac1lem3  20071  pgpfac1lem5  20073  pgpfac1  20074  pgpfaclem1  20075  pgpfaclem2  20076  pgpfaclem3  20077  ablfaclem2  20080  ablfaclem3  20081  ablfac2  20083  rngmneg1  20144  rngmneg2  20145  ringurd  20162  srgrz  20184  srglz  20185  srgisid  20186  srg1zr  20192  ringid  20247  qusring2  20307  opprring  20323  dvdsrval  20337  dvdsrmul  20340  dvdsr01  20347  dvdsr02  20348  crngunit  20354  ringunitnzdiv  20374  dvreq1  20387  dvdsrpropd  20392  irredn0  20399  irredrmul  20403  irredmul  20405  rngisomring  20443  rhmdvdsr  20484  lringuplu  20520  subrg1  20560  subrgdvds  20564  isrrg  20670  rrgeq0i  20671  rrgeq0  20672  domneq0  20680  isdomn4  20688  domnlcanb  20692  domnrcanb  20694  drngid2  20724  drngmul0orOLD  20733  isdrngd  20737  isdrngdOLD  20739  fidomndrnglem  20745  isabv  20784  issrngd  20828  islmod  20834  islmodd  20836  lmodprop2d  20894  mptscmfsupp0  20897  lss1d  20934  lspextmo  21028  lvecvs0or  21083  lvecvscan  21086  lvecvscan2  21087  lbsacsbs  21131  rngqiprngimf1lem  21277  rng2idl1cntr  21288  prmirredlem  21456  pzriprnglem7  21471  pzriprnglem13  21477  chrdvds  21514  chrnzr  21518  domnchr  21520  znval  21523  zncyg  21540  znfld  21552  znunit  21555  znrrg  21557  frgpcyg  21565  psgndiflemB  21590  psgndiflemA  21591  ipeq0  21628  ip2eq  21643  elocv  21658  ocvi  21659  obsne0  21717  dsmmacl  21733  dsmmlss  21736  frlmphl  21773  frlmup4  21793  islindf4  21830  islindf5  21831  mplsubrglem  22007  mplmon2  22068  evlslem1  22091  evlseu  22092  evlsval  22095  evlsval2  22096  ismhp3  22131  mhpsclcl  22135  mhpvarcl  22136  mhpmulcl  22137  psdmul  22154  cply1coe0bi  22288  gsummoncoe1  22294  evl1vsd  22330  dmatel  22481  dmatelnd  22484  dmatmulcl  22488  scmateALT  22500  mdetdiaglem  22586  mdetunilem1  22600  mdetunilem3  22602  mdetunilem4  22603  mdetunilem9  22608  symgmatr01lem  22641  symgmatr01  22642  gsummatr01lem1  22643  gsummatr01lem4  22646  gsummatr01  22647  smadiadetlem3  22656  cramerlem3  22677  pmatcoe1fsupp  22689  cpmatel  22699  1elcpmat  22703  cpmatmcllem  22706  cpmatmcl  22707  d1mat2pmat  22727  m2cpminvid2lem  22742  m2cpminvid2  22743  decpmatmulsumfsupp  22761  pmatcollpw2lem  22765  pmatcollpwscmatlem1  22777  mp2pm2mplem4  22797  pm2mpmhmlem1  22806  chpscmat  22830  cpmidpmatlem3  22860  cayleyhamilton0  22877  cayleyhamiltonALT  22879  cayleyhamilton1  22880  0ntr  23061  ntreq0  23067  cldlp  23140  pnrmopn  23333  hausnei2  23343  cnhaus  23344  nrmsep  23347  isnrm2  23348  regsep2  23366  dishaus  23372  ordthauslem  23373  iscmp  23378  cmpsublem  23389  cmpsub  23390  tgcmp  23391  sscmp  23395  hauscmplem  23396  cmpfi  23398  bwth  23400  connsuba  23410  nconnsubb  23413  isref  23499  islocfin  23507  elpt  23562  elptr  23563  pthaus  23628  txcmp  23633  hausdiag  23635  txhaus  23637  txkgen  23642  xkohaus  23643  xkococnlem  23649  regr1lem  23729  fbasrn  23874  fmfnfmlem3  23946  flimtopon  23960  fclstopon  24002  alexsubb  24036  symgtgp  24096  qustgpopn  24110  qustgphaus  24113  ustuqtop  24237  isusp  24252  ispsmet  24296  psmet0  24300  ismet  24315  isxmet  24316  xmeteq0  24330  metn0  24352  xmetres2  24353  imasf1oxmet  24367  xblss2ps  24393  xblss2  24394  xmseq0  24456  comet  24508  stdbdxmet  24510  methaus  24515  dscmet  24567  nrmmetd  24569  nmeq0  24613  tngngp  24657  tngngp3  24659  nlmmul0or  24686  cnmet  24774  xrsxmet  24811  metnrmlem3  24863  icopnfcnv  24953  iccpnfcnv  24955  ishtpy  24984  isphtpy  24993  phtpyi  24996  om1elbas  25045  elpi1i  25059  pi1grplem  25062  isclmp  25110  cphsqrtcl2  25200  tcphcph  25251  bcth3  25345  rrxcph  25406  rrxmet  25422  ivth2  25470  iundisj2  25564  dyaddisj  25611  volivth  25622  mbfinf  25680  i1f1lem  25704  i1fmullem  25709  i1fmulclem  25718  i1fres  25721  itg1climres  25730  mbfi1fseqlem4  25734  dvnres  25947  dvcobr  25963  dvcobrOLD  25964  rolle  26008  cmvth  26009  cmvthOLD  26010  deg1leb  26117  ismon1p  26165  q1peqb  26178  dvdsr1p  26186  ply1remlem  26187  fta1glem2  26191  idomrootle  26195  elply2  26218  ne0p  26229  coeeu  26247  coelem  26248  coeeq  26249  dgrle  26265  coeaddlem  26271  plymul0or  26303  ofmulrt  26304  plydivlem3  26318  plydivlem4  26319  plydivex  26320  plydiveu  26321  plydivalg  26322  quotlem  26323  plyremlem  26327  quotcan  26332  plyexmo  26336  elqaalem3  26344  qaa  26346  iaa  26348  aareccl  26349  aacjcl  26350  aannenlem2  26352  reeff1o  26472  sineq0  26546  coseq1  26547  efeq1  26550  recosf1o  26557  logeftb  26605  cosarg0d  26631  logtayl  26682  cxpval  26686  cxpeq0  26700  root1eq1  26778  cxpeq  26780  logbgcd1irr  26817  angrtmuld  26831  affineequiv  26846  affineequiv3  26848  angpieqvdlem2  26852  quad2  26862  dcubic1lem  26866  dcubic2  26867  dcubic  26869  mcubic  26870  cubic2  26871  dquartlem1  26874  dquart  26876  quart  26884  atandm2  26900  atandm4  26902  atantan  26946  wilthlem2  27092  wilthlem3  27093  muval2  27157  isnsqf  27158  mumullem2  27203  sqff1o  27205  muinv  27216  mpodvdsmulf1o  27217  dvdsmulf1o  27219  dchrelbas2  27261  dchrmullid  27276  dchrfi  27279  lgsval  27325  lgsdir  27356  lgsne0  27359  lgsprme0  27363  lgsdirnn0  27368  lgsqrlem1  27370  lgsqr  27375  gausslemma2dlem0c  27382  gausslemma2dlem0i  27388  gausslemma2dlem7  27397  gausslemma2d  27398  lgseisenlem2  27400  lgsquadlem1  27404  lgsquadlem2  27405  lgsquad2lem2  27409  lgsquad3  27411  m1lgs  27412  2lgs  27431  2sqlem7  27448  2sqlem8  27450  2sqlem9  27451  2sqlem11  27453  2sq  27454  2sq2  27457  2sqmo  27461  addsq2reu  27464  addsqn2reu  27465  addsqrexnreu  27466  addsqnreup  27467  addsq2nreurex  27468  2sqreulem1  27470  2sqreultlem  27471  2sqreunnlem1  27473  2sqreunnltlem  27474  2sqreulem4  27478  2sqreuop  27486  2sqreuopnn  27487  2sqreuoplt  27488  2sqreuopltb  27489  2sqreuopnnlt  27490  2sqreuopnnltb  27491  2sqreuopb  27492  dchrisumlem1  27513  dchrvmaeq0  27528  dchrisum0re  27537  ostth3  27662  sltval  27672  nosepssdm  27711  nosupprefixmo  27725  noinfprefixmo  27726  nosupcbv  27727  nosupdm  27729  nosupfv  27731  nosupres  27732  nosupbnd1lem1  27733  nosupbnd1lem3  27735  nosupbnd1lem5  27737  noinfcbv  27742  noinfdm  27744  noinffv  27746  noinfres  27747  noinfbnd1lem3  27750  noinfbnd1lem5  27752  eqscut  27830  scutbdaylt  27843  made0  27892  madecut  27901  negsid  28045  negsex  28047  subadds  28072  divsmo  28180  muls0ord  28181  divsval  28185  norecdiv  28186  divsmulw  28188  divs1  28199  precsexlem8  28208  precsexlem9  28209  precsexlem11  28211  precsex  28212  recsex  28213  abssor  28236  elons  28242  noseqrdgfn  28275  renegscl  28344  istrkg3ld  28383  axtgcgrid  28385  axtgsegcon  28386  axtg5seg  28387  axtgupdim2  28393  tgjustc1  28397  tgjustc2  28398  iscgrg  28434  isismt  28456  legov  28507  legov2  28508  hlcgreu  28540  mirreu3  28576  mircgr  28579  mirbtwn  28580  ismir  28581  mireq  28587  ismidb  28700  lmiopp  28724  dfcgra2  28752  inaghl  28767  f1otrg  28793  ttgval  28797  ttgvalOLD  28798  ttgelitv  28811  brbtwn  28828  brcgr  28829  colinearalglem2  28836  colinearalg  28839  axsegconlem1  28846  axsegcon  28856  ax5seglem4  28861  ax5seglem5  28862  axpaschlem  28869  axpasch  28870  axlowdimlem16  28886  axeuclidlem  28891  axeuclid  28892  axcontlem2  28894  axcontlem4  28896  axcontlem5  28897  edglnl  29074  usgredg2ALT  29124  usgredgprvALT  29126  usgrnloopvALT  29132  ushgredgedgloop  29162  edg0usgr  29184  nb3grpr  29313  cplgr1v  29361  cusgrsize  29386  vtxdgfval  29399  vtxdeqd  29409  vtxdun  29413  vtxd0nedgb  29420  vtxdusgr0edgnelALT  29428  1loopgrvd2  29435  usgruvtxvdb  29461  usgrvd0nedg  29465  vtxdginducedm1  29475  rusgrpropedg  29516  wksfval  29541  wlklenvclwlk  29587  iswlkon  29589  ispth  29655  upgrwlkdvdelem  29668  crctcshwlkn0lem6  29744  wwlknon  29786  wwlksm1edg  29810  wwlksnextbi  29823  wwlksnextfun  29827  wwlksnextinj  29828  wwlksnextsurj  29829  wwlksnextbij  29831  wlksnwwlknvbij  29837  wwlksnextproplem3  29840  wwlksnextprop  29841  wspn0  29853  umgr2adedgwlkonALT  29876  umgr2adedgspth  29877  umgr2wlkon  29879  rusgrnumwwlkslem  29898  rusgrnumwwlkb0  29900  rusgrnumwwlks  29903  clwlkclwwlklem2a4  29925  clwlknf1oclwwlknlem2  30010  clwlknf1oclwwlkn  30012  isclwwlknon  30019  clwwlknon1loop  30026  s2elclwwlknon2  30032  clwwlknonwwlknonb  30034  clwwlkvbij  30041  uhgr3cyclex  30110  fusgreg2wsplem  30261  fusgr2wsp2nb  30262  fusgreghash2wsp  30266  frrusgrord0  30268  2clwwlkel  30277  extwwlkfab  30280  extwwlkfabel  30281  clwwlknonclwlknonf1o  30290  dlwwlknondlwlknonf1o  30293  wlkl0  30295  numclwwlk2lem1  30304  numclwlk2lem2f  30305  numclwlk2lem2f1o  30307  numclwwlk5  30316  ex-opab  30360  isgrpo  30425  isgrpoi  30426  grpoidinvlem3  30434  grpoideu  30437  gidval  30440  grpoidinv2  30443  grpoinveu  30447  grpoinvval  30451  grpoinv  30453  vciOLD  30489  isvclem  30505  cnidOLD  30510  isnvlem  30538  nvmul0or  30578  imsmetlem  30618  diporthcom  30644  ipz  30647  nmlno0  30723  ajfval  30737  hmoval  30738  isphg  30745  isph  30750  ip2eqi  30784  ajval  30789  hvmul0or  30953  hvsubeq0  30996  hvaddeq0  30997  hvaddcan  30998  hvmulcan  31000  hvmulcan2  31001  hvsubadd  31005  his6  31027  hial0  31030  hial02  31031  hi2eq  31033  orthcom  31036  normlem7tALT  31047  normsub0  31064  normpyth  31073  hilid  31089  hhssnv  31192  ocel  31209  ocsh  31211  ocorth  31219  ocin  31224  occllem  31231  choc0  31254  pjpreeq  31326  omlsi  31332  pjoc1  31362  pjoml  31364  pjoc2  31367  chm0  31419  chocin  31423  chlejb1  31440  chlejb2  31441  chjo  31443  h1deoi  31477  h1de2i  31481  pjoml6i  31517  pjoml2  31539  pjoml3  31540  pjch  31622  hodsi  31703  hodid  31720  eigorth  31766  elunop  31800  adjeu  31817  adjval  31818  eigvecval  31824  unopf1o  31844  adj1  31861  adjeq  31863  hmdmadj  31868  lnopeq0i  31935  lnopeqi  31936  lnopeq  31937  lnfn0  31975  riesz4i  31991  riesz4  31992  riesz1  31993  cnlnadjlem3  31997  cnlnadjlem5  31999  cnlnadjeu  32006  cnlnssadj  32008  nmopadjlei  32016  opsqrlem1  32068  hmopidmpji  32080  pjimai  32104  isst  32141  ishst  32142  hstel2  32147  stadd3i  32176  stri  32185  largei  32195  golem2  32200  superpos  32282  sumdmdii  32343  mddmdin0i  32359  opreu2reuALT  32400  difeq  32444  elim2if  32463  disji2f  32495  disjif2  32499  disjxpin  32506  iundisj2f  32508  disjunsn  32512  fmptco1f1o  32548  ofpreima  32580  fnpreimac  32586  ressupprn  32600  curry2ima  32618  preiman0  32619  xrofsup  32672  iundisj2fi  32700  f1ocnt  32705  fzo0opth  32708  fprodex01  32727  xdivval  32781  xrecex  32782  xreceu  32784  xdivmul  32787  rexdiv  32788  wrdt2ind  32818  gsummpt2d  32919  fzo0pmtrlast  32972  cyc3genpm  33032  cycpmconjslem2  33035  isslmd  33068  slmdlema  33069  urpropd  33099  erlcl1  33118  erlcl2  33119  erldi  33120  erlbrd  33121  erler  33123  rloccring  33128  domnlcanOLD  33135  isdrng4  33150  fracerl  33159  fracfld  33161  resv1r  33219  islinds5  33246  linds2eq  33260  dvdsruassoi  33263  dvdsruasso  33264  dvdsruasso2  33265  quslsm  33284  rhmimaidl  33311  qsidomlem2  33332  ssdifidllem  33335  ssdifidl  33336  ssdifidlprm  33337  opprqus0g  33369  qsdrngilem  33373  unitmulrprm  33407  1arithidom  33416  1arithufdlem3  33425  1arithufdlem4  33426  ply1dg1rt  33455  r1pid2OLD  33480  lbsdiflsp0  33525  fedgmullem1  33528  fedgmullem2  33529  irngss  33567  irngnzply1lem  33570  ply1annidllem  33574  ply1annnr  33576  minplymindeg  33581  minplyann  33582  minplyirredlem  33583  minplyirred  33584  irngnminplynz  33585  irredminply  33587  algextdeglem6  33593  algextdeglem7  33594  rtelextdg2lem  33597  fldext2chn  33599  constrsuc  33608  constrsslem  33611  constrconj  33615  1smat1  33630  iscref  33670  metidval  33716  metidv  33718  metider  33720  pstmxmet  33723  xrmulc1cn  33756  ind1a  33863  prodindf  33867  esumfsup  33914  esumpcvgval  33922  esumcvg  33930  inelsros  34022  diffiunisros  34023  ismeas  34043  isrnmeas  34044  brae  34085  braew  34086  dya2iocuni  34128  elcarsg  34150  eulerpartleme  34208  eulerpartlemv  34209  eulerpartlemb  34213  eulerpartgbij  34217  eulerpartlemr  34219  eulerpartlemgvv  34221  eulerpartlemgh  34223  eulerpartlemn  34226  elprob  34254  ballotlemi  34345  ballotlemi1  34347  ballotlemii  34348  ballotlemsima  34360  ballotlemfrcn0  34374  sgn0bi  34392  signsw0g  34413  signswmnd  34414  signstfvc  34431  prodfzo03  34460  reprval  34467  reprsum  34470  reprsuc  34472  reprpmtf1o  34483  axtgupdim2ALTV  34525  brafs  34529  bnj125  34728  bnj154  34734  bnj526  34744  bnj609  34773  bnj893  34784  bnj1321  34883  bnj1491  34913  nummin  34939  subgrwlk  34971  loop1cycl  34976  subfacp1lem3  35021  subfacp1lem5  35023  subfacp1lem6  35024  cnpconn  35069  txpconn  35071  ptpconn  35072  indispconn  35073  connpconn  35074  cvxpconn  35081  cvmscbv  35097  cvmsi  35104  cvmsval  35105  cvmsdisj  35109  cvmsss2  35113  cvmliftmo  35123  cvmliftlem14  35136  cvmliftiota  35140  cvmlift2lem12  35153  cvmlift2lem13  35154  cvmlift2  35155  cvmliftphtlem  35156  cvmlift3lem2  35159  cvmlift3lem4  35161  cvmlift3lem6  35163  cvmlift3lem7  35164  cvmlift3lem9  35166  cvmlift3  35167  snmlval  35170  satffunlem  35240  prv1n  35270  mrsub0  35355  mrsubcn  35358  ismfs  35388  sinccvglem  35511  br6  35590  brbigcup  35733  imageval  35765  funpartlem  35777  dfrdg4  35786  altopthsn  35796  brsegle  35943  rankeq1o  36006  subtr  36037  opnbnd  36048  cldbnd  36049  isfne  36062  topfneec  36078  neibastop3  36085  cnndvlem2  36252  bj-imdirval2  36901  bj-imdirid  36904  bj-imdirco  36908  bj-inftyexpiinj  36927  bj-isrvecd  37016  bj-isrvec2  37018  bj-bary1lem1  37029  bj-bary1  37030  finxp00  37120  nlpfvineqsn  37127  pibp19  37132  pibt2  37135  unccur  37315  matunitlindflem2  37329  ptrecube  37332  poimirlem4  37336  poimirlem19  37351  poimirlem23  37355  poimirlem25  37357  poimirlem27  37359  poimirlem28  37360  poimirlem31  37363  poimirlem32  37364  broucube  37366  mblfinlem2  37370  ovoliunnfl  37374  voliunnfl  37376  volsupnfl  37377  mbfresfi  37378  itg2addnclem  37383  itg2addnclem3  37385  itg2addnc  37386  ftc2nc  37414  cover2  37427  sdclem2  37454  fdc  37457  metf1o  37467  istotbnd3  37483  0totbnd  37485  sstotbnd2  37486  equivtotbnd  37490  totbndbnd  37501  prdstotbnd  37506  heibor1  37522  rrnmet  37541  isexid  37559  ismgmOLD  37562  opidonOLD  37564  exidu1  37568  cmpidelt  37571  exidreslem  37589  exidres  37590  exidresid  37591  grpoeqdivid  37593  elghomlem1OLD  37597  grpokerinj  37605  isrngo  37609  isrngod  37610  rngoideu  37615  isgrpda  37667  isdrngo2  37670  isdrngo3  37671  isrngohom  37677  divrngidl  37740  dmnnzd  37787  dmncan1  37788  disjeccnvep  37993  disjressuc2  38097  qsdisjALTV  38324  dmqseqeq1  38352  unidmqseq  38364  disjdmqseq  38514  eldisjlem19  38519  riotasvd  38665  toycom  38682  islshpsm  38689  lshpnel2N  38694  lsatfixedN  38718  islshpat  38726  lcvexchlem4  38746  l1cvpat  38763  lkr0f  38803  lkrsc  38806  lshpkrlem1  38819  lkreqN  38879  isopos  38889  oposlem  38891  opcon2b  38906  cmtbr3N  38963  cvlcvrp  39049  hlrelat5N  39111  cvrval5  39125  cvrat4  39153  3atlem5  39197  2at0mat0  39235  psubclsetN  39646  4atex2  39787  isldil  39820  ltrnu  39831  ltrnid  39845  isdilN  39864  trlnid  39889  cdleme21k  40048  cdleme29b  40085  cdlemefrs29pre00  40105  cdlemefrs29bpre0  40106  cdlemefrs29cpre1  40108  cdleme32fva  40147  cdleme42b  40188  cdleme50ex  40269  cdleme  40270  cdlemg1a  40280  ltrniotaval  40291  cdlemeiota  40295  tendoid0  40535  cdlemksv2  40557  cdlemkuv2  40577  cdlemk36  40623  cdlemk42  40651  cdlemk  40684  tendoex  40685  cdleml3N  40688  cdleml5N  40690  tendospcanN  40733  cdlemm10N  40828  dihffval  40940  dihfval  40941  dihlsscpre  40944  islpolN  41193  mapdhval  41434  mapdheq  41438  hdmap1fval  41506  hdmap1val  41508  hdmap1eq  41511  hdmap1cbv  41512  hdmapval2lem  41541  hdmap11  41558  hdmap14lem2a  41577  hdmap14lem6  41583  hgmapval  41597  hlhillcs  41672  hlhilphllem  41673  aks4d1  41799  isprimroot  41803  mndmolinv  41805  linvh  41806  primrootsunit1  41807  primrootsunit  41808  primrootscoprmpow  41809  primrootscoprbij  41812  primrootlekpowne0  41815  primrootspoweq0  41816  ringexp0nn  41844  aks6d1c5lem1  41846  sticksstones8  41863  sticksstones9  41864  sticksstones10  41865  sticksstones11  41866  sticksstones12a  41867  sticksstones12  41868  sticksstones16  41872  sticksstones17  41873  sticksstones18  41874  sticksstones19  41875  aks6d1c6lem4  41883  aks6d1c6isolem3  41886  rhmqusspan  41895  grpods  41904  unitscyglem1  41905  unitscyglem2  41906  unitscyglem3  41907  metakunt6  41916  metakunt15  41925  metakunt16  41926  metakunt27  41937  metakunt28  41938  metakunt32  41942  expeq1d  42048  zdivgd  42061  ef11d  42064  resubval  42076  renegadd  42081  resubeu  42086  resubadd  42088  sn-negex12  42125  addinvcom  42140  sn-mul02  42149  mulgt0con1d  42167  mulgt0con2d  42168  fimgmcyclem  42221  fidomncyc  42223  evlsval3  42247  fsuppind  42278  mhphflem  42284  prjspnfv01  42312  prjspner01  42313  prjspner1  42314  prjcrvval  42320  dffltz  42322  flt4lem7  42347  nna4b4nsq  42348  negexpidd  42374  mzpcompact2lem  42443  eldioph  42450  eldioph2lem1  42452  eldioph2lem2  42453  eldioph2  42454  eldioph2b  42455  eldioph3  42458  diophin  42464  diophun  42465  eq0rabdioph  42468  dvdsrabdioph  42502  eldioph4i  42504  diophren  42505  rabren3dioph  42507  fphpd  42508  pellexlem5  42525  pellexlem6  42526  pellex  42527  pell1qrval  42538  pell14qrval  42540  pell1234qrval  42542  pell1234qrreccl  42546  pell1234qrmulcl  42547  pell1234qrdich  42553  pell14qrdich  42561  pell1qr1  42563  pellqrexplicit  42569  rmxycomplete  42610  jm2.27  42701  rmydioph  42707  rmxdiophlem  42708  rmxdioph  42709  pw2f1ocnv  42730  pwssplit4  42785  elmnc  42832  dgraalem  42841  dgraaub  42844  dgraa0p  42845  mpaaeu  42846  mpaaval  42847  mpaalem  42848  aaitgo  42858  rngunsnply  42869  proot1ex  42896  cantnfresb  43025  tfsconcatfv  43042  tfsconcatb0  43045  tfsconcat0i  43046  tfsconcat0b  43047  tfsconcat00  43048  tfsconcatrev  43049  naddwordnexlem4  43103  sqrtcval  43343  relexpnul  43380  relexpxpnnidm  43405  relexpiidm  43406  trclfvdecomr  43430  rfovcnvf1od  43706  ntrkbimka  43740  ntrk0kbimka  43741  clsk3nimkb  43742  clsk1independent  43748  ntrclsfveq1  43762  ntrclsfveq2  43763  ntrclskb  43771  k0004val  43852  k0004val0  43856  mnringmulrcld  43937  expgrowth  44044  bcc0  44049  disjinfi  44833  fsumf1of  45229  limsupmnflem  45375  liminfpnfuz  45471  climxlim2lem  45500  coseq0  45519  icccncfext  45542  dvnmptconst  45596  dvnprodlem1  45601  dvnprodlem2  45602  dvnprodlem3  45603  dvnprod  45604  stoweidlem15  45670  stoweidlem31  45686  stoweidlem35  45690  stoweidlem36  45691  stoweidlem37  45692  stoweidlem43  45698  stoweidlem44  45699  stoweidlem46  45701  stoweidlem55  45710  stoweidlem59  45714  dirkerval2  45749  dirkertrigeqlem1  45753  dirkeritg  45757  dirkercncf  45762  fourierdlem2  45764  fourierdlem3  45765  fourierdlem42  45804  fourierdlem48  45809  fourierdlem49  45810  fourierdlem71  45832  fourierdlem112  45873  fourierdlem113  45874  elaa2lem  45888  etransclem11  45900  etransclem24  45913  etransclem26  45915  etransclem28  45917  etransclem35  45924  ioorrnopnxr  45962  salgenval  45976  intsaluni  45984  salgenn0  45986  salgencl  45987  sssalgen  45990  salgenss  45991  salgenuni  45992  issalgend  45993  dfsalgen2  45996  subsaliuncl  46013  sge0f1o  46037  sge0fodjrnlem  46071  ismea  46106  nnfoctbdjlem  46110  iundjiun  46115  isome  46149  caragenel  46150  ovn0lem  46220  ovnsubaddlem1  46225  smflimlem4  46429  smflim  46432  sigarcol  46519  cfsetsnfsetf  46707  cfsetsnfsetfo  46709  fnbrafvb  46801  afv2fv0  46912  readdcnnred  46950  resubcnnred  46951  cndivrenred  46953  fargshiftf1  47047  fargshiftfo  47048  ichexmpl2  47076  ichnreuop  47078  ichreuopeq  47079  elsprel  47081  prproropf1olem4  47112  reupr  47128  reuopreuprim  47132  goldbachthlem2  47152  fmtnoprmfac2lem1  47172  fmtnofac2lem  47174  prmdvdsfmtnof1lem2  47191  mod42tp1mod8  47208  lighneallem2  47212  lighneallem3  47213  lighneallem4  47216  proththd  47220  41prothprm  47225  requad01  47227  requad2  47229  dfeven2  47255  dfeven5  47272  dfodd7  47273  fpprel  47334  fppr2odd  47337  fpprwppr  47345  fpprwpprb  47346  nnsum3primesgbe  47398  ushggricedg  47509  uhgrimisgrgric  47512  upwlksfval  47546  0nodd  47581  2nodd  47583  nnsgrpnmnd  47589  nn0mnd  47590  lidldomn1  47642  zlidlring  47645  uzlidlring  47646  2zrngamgm  47656  2zrngamnd  47658  2zrngagrp  47660  2zrngnmlid2  47668  ztprmneprm  47760  dmatALTbasel  47819  linindslinci  47865  lindslinindsimp1  47874  lindslinindimp2lem4  47878  lindslinindsimp2lem5  47879  linds0  47882  el0ldep  47883  lindsrng01  47885  snlindsntorlem  47887  snlindsntor  47888  ldepspr  47890  lincresunit3  47898  islindeps2  47900  isldepslvec2  47902  zlmodzxzldep  47921  blen1b  48010  dig2bits  48036  nn0sumshdiglem1  48043  0aryfvalelfv  48057  itcovalsuc  48089  prelrrx2b  48136  eenglngeehlnmlem1  48159  eenglngeehlnmlem2  48160  rrx2linest2  48166  elrrx2linest2  48167  spheres  48168  2sphere  48171  2sphere0  48172  line2ylem  48173  line2  48174  line2xlem  48175  line2x  48176  line2y  48177  itscnhlc0yqe  48181  itschlc0yqe  48182  itscnhlc0xyqsol  48187  itschlc0xyqsol1  48188  itsclc0xyqsolr  48191  itsclc0  48193  itsclc0b  48194  itsclinecirc0b  48196  itsclquadb  48198  itsclquadeu  48199  itscnhlinecirc02p  48207  sepnsepolem2  48290  sepnsepo  48291  sepfsepc  48295  iscnrm3rlem8  48315  iscnrm3r  48316  iscnrm3llem2  48318  iscnrm3l  48319  functhinclem2  48397  fullthinc2  48402  thincciso  48404  aacllem  48583