Theorem eqeq1d 2739

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

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

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

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

This theorem is referenced by:  eqeq1  2741  eqcomd  2743  eqeq2d  2748  eqeqan12d  2751  neeq1d  3000  rspcedeq1vd  3629  csbconstg  3918  csbhypf  3927  csbiebt  3928  csbiebg  3931  sbceq2g  4419  csbie2df  4443  disjeq0  4456  disjssun  4468  mosneq  4842  preq12b  4850  preq12bg  4853  elpreqprlem  4866  disji2  5127  invdisjrab  5130  disjprg  5139  disjxun  5141  iin0  5362  opthg  5482  opeqsng  5508  propeqop  5512  wefrc  5679  xpcan  6196  xpcan2  6197  dmsnopg  6233  rnmpt0f  6263  reuop  6313  dfpo2  6316  sspred  6330  onfr  6423  unisucg  6462  nsuceq0  6467  iotaeq  6526  iotabi  6527  fneq1  6659  fnun  6682  fnresdisj  6688  fnimadisj  6700  fnimaeq0  6701  foeq1  6816  fveqeq2d  6914  fvun1  7000  fvmptdv2  7034  fndmdifeq0  7064  fneqeql  7066  dffo3  7122  dffo3f  7126  fnnfpeq0  7198  foeqcnvco  7320  f1eqcocnv  7321  isofrlem  7360  eqfunresadj  7380  ovanraleqv  7455  f1opr  7489  eloprabga  7542  ovmpodv2  7591  ov3  7596  ovelimab  7611  caovcang  7634  caovcan  7637  caovmo  7670  caofinvl  7729  caofid1  7732  caofid2  7733  caofidlcan  7735  caonncan  7741  tfisi  7880  mptcnfimad  8011  oteqimp  8033  br1steqg  8036  br2ndeqg  8037  eqop  8056  reldm  8069  mposn  8128  fparlem1  8137  fparlem2  8138  fsplit  8142  frxp  8151  xporderlem  8152  fnwelem  8156  xpord2lem  8167  xpord3lem  8174  poseq  8183  soseq  8184  fnsuppeq0  8217  suppssov1  8222  suppssov2  8223  suppofss1d  8229  suppofss2d  8230  tposfo2  8274  mpocurryd  8294  iinon  8380  onnseq  8384  tz7.49  8485  seqomlem2  8491  oe0m1  8559  om0r  8577  oe1m  8583  oawordeulem  8592  oawordeu  8593  oarec  8600  omord  8606  oneo  8619  omeu  8623  oeeui  8640  nnm0r  8648  nnmord  8670  nnawordex  8675  nnaordex2  8677  nnneo  8693  nneob  8694  omopth  8700  nnasmo  8701  ereq1  8752  eqerlem  8780  qsdisj  8834  erov  8854  eceqoveq  8862  mapsnd  8926  endisj  9098  pw2f1olem  9116  enfixsn  9121  disjenex  9175  domssex2  9177  xpf1o  9179  mapxpen  9183  unxpdomlem2  9287  enp1ilem  9312  fodomfib  9369  fodomfibOLD  9371  fipreima  9398  opthreg  9658  cantnfp1lem3  9720  ssttrcl  9755  ttrcltr  9756  ttrclss  9760  ttrclselem2  9766  frmin  9789  updjud  9974  pm54.43  10041  dfac5  10169  dfacacn  10182  kmlem9  10199  cfeq0  10296  cfss  10305  cfslb  10306  fin23lem22  10367  fin23lem12  10371  fin23lem19  10376  fin23lem30  10382  fin23lem33  10385  fin1a2lem6  10445  axcc2lem  10476  axdc3lem2  10491  axdc3lem3  10492  axdc3lem4  10493  axdc3  10494  axdc4lem  10495  zorn2lem7  10542  ttukeylem3  10551  ttukeylem6  10554  ttukey2g  10556  fodomb  10566  axacndlem5  10651  fpwwe2cbv  10670  fpwwe2lem2  10672  fpwwe2lem3  10673  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwe  10686  pwfseqlem2  10699  pwxpndom2  10705  addnidpi  10941  ltexpi  10942  recmulnq  11004  ltexnq  11015  halfnq  11016  archnq  11020  ltexpri  11083  recexpr  11091  addsrpr  11115  mulsrpr  11116  00sr  11139  negexsr  11142  recexsrlem  11143  recexsr  11147  axrnegex  11202  axrrecex  11203  00id  11436  mul02  11439  addrid  11441  cnegex  11442  cnegex2  11443  subval  11499  subadd  11511  subadd2  11512  subsub23  11513  addsubeq4  11523  subcan2  11534  negcon1  11561  subcan  11564  addrsub  11680  ltordlem  11788  ltord1  11789  recex  11895  mul0or  11903  muleqadd  11907  receu  11908  mulcan1g  11916  divval  11924  divmul  11925  rec11  11965  ldiv  12101  rdiv  12102  zdiv  12688  uzin  12918  xaddval  13265  xmulval  13267  xnn0xadd0  13289  xnegdi  13290  ioo0  13412  ico0  13433  ioc0  13434  icc0  13435  1fv  13687  fzon  13720  fvinim0ffz  13825  flbi  13856  mod0  13916  modmuladdnn0  13956  modirr  13983  addmodlteq  13987  uzrdgfni  13999  axdc4uzlem  14024  fsuppmapnn0fiubex  14033  mptnn0fsupp  14038  seqid  14088  seqz  14091  expval  14104  expeq0  14133  sqeqor  14255  nn0opth2  14311  hashdom  14418  elprchashprn2  14435  hashbc  14492  hashf1lem1  14494  hash2pwpr  14515  ccat0  14614  wrdl1s1  14652  ccatws1lenp1b  14659  pfxsuff1eqwrdeq  14737  swrdccatin2  14767  pfxccatin12lem2  14769  2cshwcshw  14864  scshwfzeqfzo  14865  cshimadifsn  14868  cshimadifsn0  14869  s2f1o  14955  wrdlen2i  14981  2swrd2eqwrdeq  14992  wwlktovf  14995  wwlktovf1  14996  wwlktovfo  14997  wrd2f1tovbij  14999  relexp0g  15061  relexpsucnnr  15064  dfrtrcl2  15101  mulre  15160  rennim  15278  cnpart  15279  01sqrex  15288  resqrex  15289  sqrmo  15290  resqrtcl  15292  resqrtthlem  15293  sqrtgt0  15297  sqrtneg  15306  sqrtsq2  15307  absmod0  15342  sqreulem  15398  sqreu  15399  sqrtthlem  15401  eqsqrtd  15406  reusq0  15501  fsum00  15834  telfsumo  15838  prodss  15983  fprodle  16032  tanaddlem  16202  absefib  16234  efieq1re  16235  divides  16292  dvdsval2  16293  nndivides  16300  dvds0lem  16304  dvds1lem  16305  dvds2lem  16306  negdvdsb  16310  muldvds1  16318  muldvds2  16319  dvdscmulr  16322  dvdsmulcr  16323  dvdstr  16331  dvdsabseq  16350  divconjdvds  16352  odd2np1lem  16377  odd2np1  16378  even2n  16379  oddm1even  16380  2tp1odd  16389  opeo  16402  omeo  16403  m1exp1  16413  divalglem4  16433  divalglem8  16437  divalgb  16441  bitsuz  16511  smupvallem  16520  gcdaddmlem  16561  gcdabs1  16566  bezoutlem3  16578  rplpwr  16595  rprpwr  16596  alginv  16612  algcvga  16616  algfx  16617  eucalgval2  16618  coprmdvds  16690  qredeq  16694  qredeu  16695  coprmprod  16698  coprmproddvdslem  16699  divgcdcoprm0  16702  divgcdcoprmex  16703  cncongr1  16704  rpexp  16759  rpexp12i  16761  cncongrprm  16766  qnumdenbi  16781  phival  16804  phicl2  16805  dfphi2  16811  phiprmpw  16813  phimullem  16816  eulerthlem1  16818  eulerthlem2  16819  eulerth  16820  fermltl  16821  hashgcdlem  16825  phisum  16828  odzval  16829  odzdvds  16833  reumodprminv  16842  modprm0  16843  nnnn0modprm0  16844  modprmn0modprm0  16845  coprimeprodsq  16846  coprimeprodsq2  16847  pythagtriplem2  16855  pythagtrip  16872  pcval  16882  pceulem  16883  pcqmul  16891  pcqcl  16894  pcabs  16913  pcgcd1  16915  pc2dvds  16917  pcaddlem  16926  pcadd  16927  pcmpt  16930  prmpwdvds  16942  pockthi  16945  unbenlem  16946  4sqlem12  16994  ramz  17063  ramcl  17067  cshwrepswhash1  17140  imasval  17556  fvprif  17606  iscat  17715  iscatd  17716  catidex  17717  catideu  17718  cidfval  17719  cidval  17720  catidd  17723  catlid  17726  catrid  17727  catpropd  17752  cidpropd  17753  issect  17797  dfiso2  17816  invcoisoid  17836  isocoinvid  17837  setcepi  18133  latleeqj2  18497  latleeqm2  18513  oduclatb  18552  mgmidmo  18673  grpidval  18674  grpidpropd  18675  ismgmid  18678  ismgmid2  18681  mgmidsssn0  18685  grpinvalem  18686  grprida  18688  gsumvalx  18689  gsumpropd  18691  gsumpropd2lem  18692  gsumress  18695  gsumval2  18699  ismnddef  18749  sgrpidmnd  18752  ismndd  18769  mndpropd  18772  mndinvmod  18777  mnd1  18792  ismhm  18798  gsumvallem2  18847  frmdgsum  18875  frmdup3  18880  efmndmnd  18902  smndex1mnd  18923  sgrp2rid2  18939  sgrp2rid2ex  18940  pwmnd  18950  grpinvex  18961  isgrpd2  18974  isgrpd  18976  dfgrp2  18980  grpinveu  18992  grpinvval  18998  grplinv  19007  isgrpinv  19011  grplrinv  19014  grpidinv2  19015  grpidinv  19016  grplmulf1o  19031  grpraddf1o  19032  grpsubeq0  19044  grpsubadd  19046  dfgrp3lem  19056  dfgrp3  19057  grp1  19065  imasgrp2  19073  qusgrp2  19076  mhmmnd  19082  ghmgrp  19084  mulgval  19089  mulgaddcom  19116  eqg0el  19201  cycsubmel  19218  ghmeqker  19261  ghmf1  19264  conjnmzb  19271  ghmqusker  19305  isga  19309  subgga  19318  gaorb  19325  gaorber  19326  gastacl  19327  gastacos  19328  orbsta  19331  symgfix2  19434  gsmsymgrfixlem1  19445  gsmsymgrfix  19446  gsmsymgreq  19450  symgfixelq  19451  f1omvdconj  19464  pmtrdifwrdel2  19504  psgnunilem1  19511  psgnunilem2  19513  psgnunilem3  19514  psgnunilem4  19515  odval  19552  odid  19556  odlem2  19557  oddvdsnn0  19562  odnncl  19563  oddvds  19565  odcong  19567  odeq  19568  odmulgid  19572  odmulgeq  19575  gexval  19596  gexid  19599  gexlem2  19600  gexdvdsi  19601  gexdvds  19602  subgpgp  19615  sylow1lem1  19616  sylow1lem4  19619  sylow2alem1  19635  sylow2alem2  19636  sylow2blem2  19639  sylow3lem6  19650  lsmdisj3a  19707  lsmdisj3b  19708  pj1val  19713  pj1eq  19718  efgredlemd  19762  efgredlem  19765  efgred  19766  efgrelexlema  19767  frgpup3  19796  ablsubadd  19827  ablsubsub23  19842  iscyggen  19898  cyggenod  19902  gsumval3lem2  19924  gsumval3  19925  gsummptnn0fz  20004  dmdprd  20018  dprddisj  20029  dprdfeq0  20042  dprdf11  20043  dmdprdpr  20069  dpjeq  20079  ablfacrp  20086  pgpfac1lem2  20095  pgpfac1lem3  20097  pgpfac1lem5  20099  pgpfac1  20100  pgpfaclem1  20101  pgpfaclem2  20102  pgpfaclem3  20103  ablfaclem2  20106  ablfaclem3  20107  ablfac2  20109  rngmneg1  20164  rngmneg2  20165  ringurd  20182  srgrz  20204  srglz  20205  srgisid  20206  srg1zr  20212  ringid  20271  qusring2  20331  opprring  20347  dvdsrval  20361  dvdsrmul  20364  dvdsr01  20371  dvdsr02  20372  crngunit  20378  ringunitnzdiv  20398  dvreq1  20411  dvdsrpropd  20416  irredn0  20423  irredrmul  20427  irredmul  20429  rngisomring  20467  rhmdvdsr  20508  lringuplu  20544  subrg1  20582  subrgdvds  20586  isrrg  20698  rrgeq0i  20699  rrgeq0  20700  domneq0  20708  isdomn4  20716  domnlcanb  20720  domnrcanb  20722  drngid2  20752  drngmul0orOLD  20761  isdrngd  20765  isdrngdOLD  20767  fidomndrnglem  20773  isabv  20812  issrngd  20856  islmod  20862  islmodd  20864  lmodprop2d  20922  mptscmfsupp0  20925  lss1d  20961  lspextmo  21055  lvecvs0or  21110  lvecvscan  21113  lvecvscan2  21114  lbsacsbs  21158  rngqiprngimf1lem  21304  rng2idl1cntr  21315  prmirredlem  21483  pzriprnglem7  21498  pzriprnglem13  21504  chrdvds  21541  chrnzr  21545  domnchr  21547  znval  21550  zncyg  21567  znfld  21579  znunit  21582  znrrg  21584  frgpcyg  21592  psgndiflemB  21618  psgndiflemA  21619  ipeq0  21656  ip2eq  21671  elocv  21686  ocvi  21687  obsne0  21745  dsmmacl  21761  dsmmlss  21764  frlmphl  21801  frlmup4  21821  islindf4  21858  islindf5  21859  mplsubrglem  22024  mplmon2  22085  evlslem1  22106  evlseu  22107  evlsval  22110  evlsval2  22111  ismhp3  22146  mhpsclcl  22151  mhpvarcl  22152  mhpmulcl  22153  psdmul  22170  psdmvr  22173  cply1coe0bi  22306  gsummoncoe1  22312  evl1vsd  22348  dmatel  22499  dmatelnd  22502  dmatmulcl  22506  scmateALT  22518  mdetdiaglem  22604  mdetunilem1  22618  mdetunilem3  22620  mdetunilem4  22621  mdetunilem9  22626  symgmatr01lem  22659  symgmatr01  22660  gsummatr01lem1  22661  gsummatr01lem4  22664  gsummatr01  22665  smadiadetlem3  22674  cramerlem3  22695  pmatcoe1fsupp  22707  cpmatel  22717  1elcpmat  22721  cpmatmcllem  22724  cpmatmcl  22725  d1mat2pmat  22745  m2cpminvid2lem  22760  m2cpminvid2  22761  decpmatmulsumfsupp  22779  pmatcollpw2lem  22783  pmatcollpwscmatlem1  22795  mp2pm2mplem4  22815  pm2mpmhmlem1  22824  chpscmat  22848  cpmidpmatlem3  22878  cayleyhamilton0  22895  cayleyhamiltonALT  22897  cayleyhamilton1  22898  0ntr  23079  ntreq0  23085  cldlp  23158  pnrmopn  23351  hausnei2  23361  cnhaus  23362  nrmsep  23365  isnrm2  23366  regsep2  23384  dishaus  23390  ordthauslem  23391  iscmp  23396  cmpsublem  23407  cmpsub  23408  tgcmp  23409  sscmp  23413  hauscmplem  23414  cmpfi  23416  bwth  23418  connsuba  23428  nconnsubb  23431  isref  23517  islocfin  23525  elpt  23580  elptr  23581  pthaus  23646  txcmp  23651  hausdiag  23653  txhaus  23655  txkgen  23660  xkohaus  23661  xkococnlem  23667  regr1lem  23747  fbasrn  23892  fmfnfmlem3  23964  flimtopon  23978  fclstopon  24020  alexsubb  24054  symgtgp  24114  qustgpopn  24128  qustgphaus  24131  ustuqtop  24255  isusp  24270  ispsmet  24314  psmet0  24318  ismet  24333  isxmet  24334  xmeteq0  24348  metn0  24370  xmetres2  24371  imasf1oxmet  24385  xblss2ps  24411  xblss2  24412  xmseq0  24474  comet  24526  stdbdxmet  24528  methaus  24533  dscmet  24585  nrmmetd  24587  nmeq0  24631  tngngp  24675  tngngp3  24677  nlmmul0or  24704  cnmet  24792  xrsxmet  24831  metnrmlem3  24883  icopnfcnv  24973  iccpnfcnv  24975  ishtpy  25004  isphtpy  25013  phtpyi  25016  om1elbas  25065  elpi1i  25079  pi1grplem  25082  isclmp  25130  cphsqrtcl2  25220  tcphcph  25271  bcth3  25365  rrxcph  25426  rrxmet  25442  ivth2  25490  iundisj2  25584  dyaddisj  25631  volivth  25642  mbfinf  25700  i1f1lem  25724  i1fmullem  25729  i1fmulclem  25737  i1fres  25740  itg1climres  25749  mbfi1fseqlem4  25753  dvnres  25967  dvcobr  25983  dvcobrOLD  25984  rolle  26028  cmvth  26029  cmvthOLD  26030  deg1leb  26134  ismon1p  26182  q1peqb  26195  dvdsr1p  26203  ply1remlem  26204  fta1glem2  26208  idomrootle  26212  elply2  26235  ne0p  26246  coeeu  26264  coelem  26265  coeeq  26266  dgrle  26282  coeaddlem  26288  plymul0or  26322  ofmulrt  26323  plydivlem3  26337  plydivlem4  26338  plydivex  26339  plydiveu  26340  plydivalg  26341  quotlem  26342  plyremlem  26346  quotcan  26351  plyexmo  26355  elqaalem3  26363  qaa  26365  iaa  26367  aareccl  26368  aacjcl  26369  aannenlem2  26371  reeff1o  26491  sineq0  26566  coseq1  26567  efeq1  26570  recosf1o  26577  logeftb  26625  cosarg0d  26651  logtayl  26702  cxpval  26706  cxpeq0  26720  root1eq1  26798  cxpeq  26800  logbgcd1irr  26837  angrtmuld  26851  affineequiv  26866  affineequiv3  26868  angpieqvdlem2  26872  quad2  26882  dcubic1lem  26886  dcubic2  26887  dcubic  26889  mcubic  26890  cubic2  26891  dquartlem1  26894  dquart  26896  quart  26904  atandm2  26920  atandm4  26922  atantan  26966  wilthlem2  27112  wilthlem3  27113  muval2  27177  isnsqf  27178  mumullem2  27223  sqff1o  27225  muinv  27236  mpodvdsmulf1o  27237  dvdsmulf1o  27239  dchrelbas2  27281  dchrmullid  27296  dchrfi  27299  lgsval  27345  lgsdir  27376  lgsne0  27379  lgsprme0  27383  lgsdirnn0  27388  lgsqrlem1  27390  lgsqr  27395  gausslemma2dlem0c  27402  gausslemma2dlem0i  27408  gausslemma2dlem7  27417  gausslemma2d  27418  lgseisenlem2  27420  lgsquadlem1  27424  lgsquadlem2  27425  lgsquad2lem2  27429  lgsquad3  27431  m1lgs  27432  2lgs  27451  2sqlem7  27468  2sqlem8  27470  2sqlem9  27471  2sqlem11  27473  2sq  27474  2sq2  27477  2sqmo  27481  addsq2reu  27484  addsqn2reu  27485  addsqrexnreu  27486  addsqnreup  27487  addsq2nreurex  27488  2sqreulem1  27490  2sqreultlem  27491  2sqreunnlem1  27493  2sqreunnltlem  27494  2sqreulem4  27498  2sqreuop  27506  2sqreuopnn  27507  2sqreuoplt  27508  2sqreuopltb  27509  2sqreuopnnlt  27510  2sqreuopnnltb  27511  2sqreuopb  27512  dchrisumlem1  27533  dchrvmaeq0  27548  dchrisum0re  27557  ostth3  27682  sltval  27692  nosepssdm  27731  nosupprefixmo  27745  noinfprefixmo  27746  nosupcbv  27747  nosupdm  27749  nosupfv  27751  nosupres  27752  nosupbnd1lem1  27753  nosupbnd1lem3  27755  nosupbnd1lem5  27757  noinfcbv  27762  noinfdm  27764  noinffv  27766  noinfres  27767  noinfbnd1lem3  27770  noinfbnd1lem5  27772  eqscut  27850  scutbdaylt  27863  made0  27912  madecut  27921  negsid  28073  negsex  28075  subadds  28100  divsmo  28210  muls0ord  28211  divsval  28215  norecdiv  28216  divsmulw  28218  divs1  28229  precsexlem8  28238  precsexlem9  28239  precsexlem11  28241  precsex  28242  recsex  28243  abssor  28270  elons  28276  noseqrdgfn  28312  n0seo  28405  zseo  28406  nohalf  28407  expsne0  28414  renegscl  28430  istrkg3ld  28469  axtgcgrid  28471  axtgsegcon  28472  axtg5seg  28473  axtgupdim2  28479  tgjustc1  28483  tgjustc2  28484  iscgrg  28520  isismt  28542  legov  28593  legov2  28594  hlcgreu  28626  mirreu3  28662  mircgr  28665  mirbtwn  28666  ismir  28667  mireq  28673  ismidb  28786  lmiopp  28810  dfcgra2  28838  inaghl  28853  f1otrg  28879  ttgval  28883  ttgvalOLD  28884  ttgelitv  28897  brbtwn  28914  brcgr  28915  colinearalglem2  28922  colinearalg  28925  axsegconlem1  28932  axsegcon  28942  ax5seglem4  28947  ax5seglem5  28948  axpaschlem  28955  axpasch  28956  axlowdimlem16  28972  axeuclidlem  28977  axeuclid  28978  axcontlem2  28980  axcontlem4  28982  axcontlem5  28983  edglnl  29160  usgredg2ALT  29210  usgredgprvALT  29212  usgrnloopvALT  29218  ushgredgedgloop  29248  edg0usgr  29270  nb3grpr  29399  cplgr1v  29447  cusgrsize  29472  vtxdgfval  29485  vtxdeqd  29495  vtxdun  29499  vtxd0nedgb  29506  vtxdusgr0edgnelALT  29514  1loopgrvd2  29521  usgruvtxvdb  29547  usgrvd0nedg  29551  vtxdginducedm1  29561  rusgrpropedg  29602  wksfval  29627  wlklenvclwlk  29673  iswlkon  29675  ispth  29741  dfpth2  29749  upgrwlkdvdelem  29756  crctcshwlkn0lem6  29835  wwlknon  29877  wwlksm1edg  29901  wwlksnextbi  29914  wwlksnextfun  29918  wwlksnextinj  29919  wwlksnextsurj  29920  wwlksnextbij  29922  wlksnwwlknvbij  29928  wwlksnextproplem3  29931  wwlksnextprop  29932  wspn0  29944  umgr2adedgwlkonALT  29967  umgr2adedgspth  29968  umgr2wlkon  29970  rusgrnumwwlkslem  29989  rusgrnumwwlkb0  29991  rusgrnumwwlks  29994  clwlkclwwlklem2a4  30016  clwlknf1oclwwlknlem2  30101  clwlknf1oclwwlkn  30103  isclwwlknon  30110  clwwlknon1loop  30117  s2elclwwlknon2  30123  clwwlknonwwlknonb  30125  clwwlkvbij  30132  uhgr3cyclex  30201  fusgreg2wsplem  30352  fusgr2wsp2nb  30353  fusgreghash2wsp  30357  frrusgrord0  30359  2clwwlkel  30368  extwwlkfab  30371  extwwlkfabel  30372  clwwlknonclwlknonf1o  30381  dlwwlknondlwlknonf1o  30384  wlkl0  30386  numclwwlk2lem1  30395  numclwlk2lem2f  30396  numclwlk2lem2f1o  30398  numclwwlk5  30407  ex-opab  30451  isgrpo  30516  isgrpoi  30517  grpoidinvlem3  30525  grpoideu  30528  gidval  30531  grpoidinv2  30534  grpoinveu  30538  grpoinvval  30542  grpoinv  30544  vciOLD  30580  isvclem  30596  cnidOLD  30601  isnvlem  30629  nvmul0or  30669  imsmetlem  30709  diporthcom  30735  ipz  30738  nmlno0  30814  ajfval  30828  hmoval  30829  isphg  30836  isph  30841  ip2eqi  30875  ajval  30880  hvmul0or  31044  hvsubeq0  31087  hvaddeq0  31088  hvaddcan  31089  hvmulcan  31091  hvmulcan2  31092  hvsubadd  31096  his6  31118  hial0  31121  hial02  31122  hi2eq  31124  orthcom  31127  normlem7tALT  31138  normsub0  31155  normpyth  31164  hilid  31180  hhssnv  31283  ocel  31300  ocsh  31302  ocorth  31310  ocin  31315  occllem  31322  choc0  31345  pjpreeq  31417  omlsi  31423  pjoc1  31453  pjoml  31455  pjoc2  31458  chm0  31510  chocin  31514  chlejb1  31531  chlejb2  31532  chjo  31534  h1deoi  31568  h1de2i  31572  pjoml6i  31608  pjoml2  31630  pjoml3  31631  pjch  31713  hodsi  31794  hodid  31811  eigorth  31857  elunop  31891  adjeu  31908  adjval  31909  eigvecval  31915  unopf1o  31935  adj1  31952  adjeq  31954  hmdmadj  31959  lnopeq0i  32026  lnopeqi  32027  lnopeq  32028  lnfn0  32066  riesz4i  32082  riesz4  32083  riesz1  32084  cnlnadjlem3  32088  cnlnadjlem5  32090  cnlnadjeu  32097  cnlnssadj  32099  nmopadjlei  32107  opsqrlem1  32159  hmopidmpji  32171  pjimai  32195  isst  32232  ishst  32233  hstel2  32238  stadd3i  32267  stri  32276  largei  32286  golem2  32291  superpos  32373  sumdmdii  32434  mddmdin0i  32450  opreu2reuALT  32496  difeq  32537  elim2if  32557  disji2f  32590  disjif2  32594  disjxpin  32601  iundisj2f  32603  disjunsn  32607  fmptco1f1o  32643  ofpreima  32675  fnpreimac  32681  ressupprn  32699  curry2ima  32718  preiman0  32719  xrofsup  32771  iundisj2fi  32799  f1ocnt  32804  fzo0opth  32807  fprodex01  32827  ind1a  32844  prodindf  32848  xdivval  32901  xrecex  32902  xreceu  32904  xdivmul  32907  rexdiv  32908  wrdt2ind  32938  mndlrinvb  33030  mndlactfo  33032  mndractfo  33034  mndlactf1o  33035  mndractf1o  33036  gsummpt2d  33052  gsumwun  33068  fzo0pmtrlast  33112  cyc3genpm  33172  cycpmconjslem2  33175  isslmd  33208  slmdlema  33209  urpropd  33236  elrgspnlem4  33249  elrgspnsubrunlem2  33252  erlcl1  33264  erlcl2  33265  erldi  33266  erlbrd  33267  erler  33269  rloccring  33274  domnlcanOLD  33283  isdrng4  33298  fracerl  33308  fracfld  33310  resv1r  33368  islinds5  33395  linds2eq  33409  dvdsruassoi  33412  dvdsruasso  33413  dvdsruasso2  33414  quslsm  33433  rhmimaidl  33460  qsidomlem2  33481  ssdifidllem  33484  ssdifidl  33485  ssdifidlprm  33486  opprqus0g  33518  qsdrngilem  33522  unitmulrprm  33556  1arithidom  33565  1arithufdlem3  33574  1arithufdlem4  33575  ply1dg1rt  33604  r1pid2OLD  33629  lbsdiflsp0  33677  fedgmullem1  33680  fedgmullem2  33681  irngss  33737  irngnzply1lem  33740  ply1annidllem  33744  ply1annnr  33746  minplymindeg  33751  minplyann  33752  minplyirredlem  33753  minplyirred  33754  irngnminplynz  33755  irredminply  33757  algextdeglem6  33763  algextdeglem7  33764  rtelextdg2lem  33767  fldext2chn  33769  constrsuc  33779  constrsslem  33782  constrconj  33786  constrextdg2lem  33789  constrextdg2  33790  1smat1  33803  iscref  33843  metidval  33889  metidv  33891  metider  33893  pstmxmet  33896  xrmulc1cn  33929  esumfsup  34071  esumpcvgval  34079  esumcvg  34087  inelsros  34179  diffiunisros  34180  ismeas  34200  isrnmeas  34201  brae  34242  braew  34243  dya2iocuni  34285  elcarsg  34307  eulerpartleme  34365  eulerpartlemv  34366  eulerpartlemb  34370  eulerpartgbij  34374  eulerpartlemr  34376  eulerpartlemgvv  34378  eulerpartlemgh  34380  eulerpartlemn  34383  elprob  34411  ballotlemi  34503  ballotlemi1  34505  ballotlemii  34506  ballotlemsima  34518  ballotlemfrcn0  34532  sgn0bi  34550  signsw0g  34571  signswmnd  34572  signstfvc  34589  prodfzo03  34618  reprval  34625  reprsum  34628  reprsuc  34630  reprpmtf1o  34641  axtgupdim2ALTV  34683  brafs  34687  bnj125  34886  bnj154  34892  bnj526  34902  bnj609  34931  bnj893  34942  bnj1321  35041  bnj1491  35071  nummin  35105  subgrwlk  35137  loop1cycl  35142  subfacp1lem3  35187  subfacp1lem5  35189  subfacp1lem6  35190  cnpconn  35235  txpconn  35237  ptpconn  35238  indispconn  35239  connpconn  35240  cvxpconn  35247  cvmscbv  35263  cvmsi  35270  cvmsval  35271  cvmsdisj  35275  cvmsss2  35279  cvmliftmo  35289  cvmliftlem14  35302  cvmliftiota  35306  cvmlift2lem12  35319  cvmlift2lem13  35320  cvmlift2  35321  cvmliftphtlem  35322  cvmlift3lem2  35325  cvmlift3lem4  35327  cvmlift3lem6  35329  cvmlift3lem7  35330  cvmlift3lem9  35332  cvmlift3  35333  snmlval  35336  satffunlem  35406  prv1n  35436  mrsub0  35521  mrsubcn  35524  ismfs  35554  sinccvglem  35677  br6  35757  brbigcup  35899  imageval  35931  funpartlem  35943  dfrdg4  35952  altopthsn  35962  brsegle  36109  rankeq1o  36172  cbviotadavw  36270  subtr  36315  opnbnd  36326  cldbnd  36327  isfne  36340  topfneec  36356  neibastop3  36363  cnndvlem2  36539  bj-imdirval2  37184  bj-imdirid  37187  bj-imdirco  37191  bj-inftyexpiinj  37210  bj-isrvecd  37299  bj-isrvec2  37301  bj-bary1lem1  37312  bj-bary1  37313  finxp00  37403  nlpfvineqsn  37410  pibp19  37415  pibt2  37418  unccur  37610  matunitlindflem2  37624  ptrecube  37627  poimirlem4  37631  poimirlem19  37646  poimirlem23  37650  poimirlem25  37652  poimirlem27  37654  poimirlem28  37655  poimirlem31  37658  poimirlem32  37659  broucube  37661  mblfinlem2  37665  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  mbfresfi  37673  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  ftc2nc  37709  cover2  37722  sdclem2  37749  fdc  37752  metf1o  37762  istotbnd3  37778  0totbnd  37780  sstotbnd2  37781  equivtotbnd  37785  totbndbnd  37796  prdstotbnd  37801  heibor1  37817  rrnmet  37836  isexid  37854  ismgmOLD  37857  opidonOLD  37859  exidu1  37863  cmpidelt  37866  exidreslem  37884  exidres  37885  exidresid  37886  grpoeqdivid  37888  elghomlem1OLD  37892  grpokerinj  37900  isrngo  37904  isrngod  37905  rngoideu  37910  isgrpda  37962  isdrngo2  37965  isdrngo3  37966  isrngohom  37972  divrngidl  38035  dmnnzd  38082  dmncan1  38083  disjeccnvep  38285  disjressuc2  38389  qsdisjALTV  38616  dmqseqeq1  38644  unidmqseq  38656  disjdmqseq  38806  eldisjlem19  38811  riotasvd  38957  toycom  38974  islshpsm  38981  lshpnel2N  38986  lsatfixedN  39010  islshpat  39018  lcvexchlem4  39038  l1cvpat  39055  lkr0f  39095  lkrsc  39098  lshpkrlem1  39111  lkreqN  39171  isopos  39181  oposlem  39183  opcon2b  39198  cmtbr3N  39255  cvlcvrp  39341  hlrelat5N  39403  cvrval5  39417  cvrat4  39445  3atlem5  39489  2at0mat0  39527  psubclsetN  39938  4atex2  40079  isldil  40112  ltrnu  40123  ltrnid  40137  isdilN  40156  trlnid  40181  cdleme21k  40340  cdleme29b  40377  cdlemefrs29pre00  40397  cdlemefrs29bpre0  40398  cdlemefrs29cpre1  40400  cdleme32fva  40439  cdleme42b  40480  cdleme50ex  40561  cdleme  40562  cdlemg1a  40572  ltrniotaval  40583  cdlemeiota  40587  tendoid0  40827  cdlemksv2  40849  cdlemkuv2  40869  cdlemk36  40915  cdlemk42  40943  cdlemk  40976  tendoex  40977  cdleml3N  40980  cdleml5N  40982  tendospcanN  41025  cdlemm10N  41120  dihffval  41232  dihfval  41233  dihlsscpre  41236  islpolN  41485  mapdhval  41726  mapdheq  41730  hdmap1fval  41798  hdmap1val  41800  hdmap1eq  41803  hdmap1cbv  41804  hdmapval2lem  41833  hdmap11  41850  hdmap14lem2a  41869  hdmap14lem6  41875  hgmapval  41889  hlhillcs  41964  hlhilphllem  41965  aks4d1  42090  isprimroot  42094  mndmolinv  42096  linvh  42097  primrootsunit1  42098  primrootsunit  42099  primrootscoprmpow  42100  primrootscoprbij  42103  primrootlekpowne0  42106  primrootspoweq0  42107  ringexp0nn  42135  aks6d1c5lem1  42137  sticksstones8  42154  sticksstones9  42155  sticksstones10  42156  sticksstones11  42157  sticksstones12a  42158  sticksstones12  42159  sticksstones16  42163  sticksstones17  42164  sticksstones18  42165  sticksstones19  42166  aks6d1c6lem4  42174  aks6d1c6isolem3  42177  rhmqusspan  42186  grpods  42195  unitscyglem1  42196  unitscyglem2  42197  unitscyglem3  42198  unitscyglem5  42200  metakunt6  42211  metakunt15  42220  metakunt16  42221  metakunt27  42232  metakunt28  42233  metakunt32  42237  expeq1d  42359  zdivgd  42372  ef11d  42375  resubval  42397  renegadd  42402  resubeu  42407  resubadd  42409  sn-negex12  42446  addinvcom  42461  sn-mul02  42470  mulgt0con1d  42488  mulgt0con2d  42489  fimgmcyclem  42543  fidomncyc  42545  evlsval3  42569  fsuppind  42600  mhphflem  42606  prjspnfv01  42634  prjspner01  42635  prjspner1  42636  prjcrvval  42642  dffltz  42644  flt4lem7  42669  nna4b4nsq  42670  negexpidd  42693  mzpcompact2lem  42762  eldioph  42769  eldioph2lem1  42771  eldioph2lem2  42772  eldioph2  42773  eldioph2b  42774  eldioph3  42777  diophin  42783  diophun  42784  eq0rabdioph  42787  dvdsrabdioph  42821  eldioph4i  42823  diophren  42824  rabren3dioph  42826  fphpd  42827  pellexlem5  42844  pellexlem6  42845  pellex  42846  pell1qrval  42857  pell14qrval  42859  pell1234qrval  42861  pell1234qrreccl  42865  pell1234qrmulcl  42866  pell1234qrdich  42872  pell14qrdich  42880  pell1qr1  42882  pellqrexplicit  42888  rmxycomplete  42929  jm2.27  43020  rmydioph  43026  rmxdiophlem  43027  rmxdioph  43028  pw2f1ocnv  43049  pwssplit4  43101  elmnc  43148  dgraalem  43157  dgraaub  43160  dgraa0p  43161  mpaaeu  43162  mpaaval  43163  mpaalem  43164  aaitgo  43174  rngunsnply  43181  proot1ex  43208  cantnfresb  43337  tfsconcatfv  43354  tfsconcatb0  43357  tfsconcat0i  43358  tfsconcat0b  43359  tfsconcat00  43360  tfsconcatrev  43361  naddwordnexlem4  43414  sqrtcval  43654  relexpnul  43691  relexpxpnnidm  43716  relexpiidm  43717  trclfvdecomr  43741  rfovcnvf1od  44017  ntrkbimka  44051  ntrk0kbimka  44052  clsk3nimkb  44053  clsk1independent  44059  ntrclsfveq1  44073  ntrclsfveq2  44074  ntrclskb  44082  k0004val  44163  k0004val0  44167  mnringmulrcld  44247  expgrowth  44354  bcc0  44359  relpfrlem  44974  disjinfi  45197  fsumf1of  45589  limsupmnflem  45735  liminfpnfuz  45831  climxlim2lem  45860  coseq0  45879  icccncfext  45902  dvnmptconst  45956  dvnprodlem1  45961  dvnprodlem2  45962  dvnprodlem3  45963  dvnprod  45964  stoweidlem15  46030  stoweidlem31  46046  stoweidlem35  46050  stoweidlem36  46051  stoweidlem37  46052  stoweidlem43  46058  stoweidlem44  46059  stoweidlem46  46061  stoweidlem55  46070  stoweidlem59  46074  dirkerval2  46109  dirkertrigeqlem1  46113  dirkeritg  46117  dirkercncf  46122  fourierdlem2  46124  fourierdlem3  46125  fourierdlem42  46164  fourierdlem48  46169  fourierdlem49  46170  fourierdlem71  46192  fourierdlem112  46233  fourierdlem113  46234  elaa2lem  46248  etransclem11  46260  etransclem24  46273  etransclem26  46275  etransclem28  46277  etransclem35  46284  ioorrnopnxr  46322  salgenval  46336  intsaluni  46344  salgenn0  46346  salgencl  46347  sssalgen  46350  salgenss  46351  salgenuni  46352  issalgend  46353  dfsalgen2  46356  subsaliuncl  46373  sge0f1o  46397  sge0fodjrnlem  46431  ismea  46466  nnfoctbdjlem  46470  iundjiun  46475  isome  46509  caragenel  46510  ovn0lem  46580  ovnsubaddlem1  46585  smflimlem4  46789  smflim  46792  sigarcol  46879  cfsetsnfsetf  47070  cfsetsnfsetfo  47072  fnbrafvb  47166  afv2fv0  47277  readdcnnred  47315  resubcnnred  47316  cndivrenred  47318  minusmodnep2tmod  47355  fargshiftf1  47428  fargshiftfo  47429  ichexmpl2  47457  ichnreuop  47459  ichreuopeq  47460  elsprel  47462  prproropf1olem4  47493  reupr  47509  reuopreuprim  47513  goldbachthlem2  47533  fmtnoprmfac2lem1  47553  fmtnofac2lem  47555  prmdvdsfmtnof1lem2  47572  mod42tp1mod8  47589  lighneallem2  47593  lighneallem3  47594  lighneallem4  47597  proththd  47601  41prothprm  47606  requad01  47608  requad2  47610  dfeven2  47636  dfeven5  47653  dfodd7  47654  fpprel  47715  fppr2odd  47718  fpprwppr  47726  fpprwpprb  47727  nnsum3primesgbe  47779  isubgredg  47852  ushggricedg  47896  uhgrimisgrgric  47899  isubgr3stgrlem3  47935  isubgr3stgrlem4  47936  isubgr3stgrlem6  47938  grlimgrtrilem2  47962  gpgedgvtx0  48019  gpgedgvtx1  48020  gpgvtxedg0  48021  gpgvtxedg1  48022  gpg3kgrtriexlem5  48043  upwlksfval  48051  0nodd  48086  2nodd  48088  nnsgrpnmnd  48094  nn0mnd  48095  lidldomn1  48147  zlidlring  48150  uzlidlring  48151  2zrngamgm  48161  2zrngamnd  48163  2zrngagrp  48165  2zrngnmlid2  48173  ztprmneprm  48263  dmatALTbasel  48319  linindslinci  48365  lindslinindsimp1  48374  lindslinindimp2lem4  48378  lindslinindsimp2lem5  48379  linds0  48382  el0ldep  48383  lindsrng01  48385  snlindsntorlem  48387  snlindsntor  48388  ldepspr  48390  lincresunit3  48398  islindeps2  48400  isldepslvec2  48402  zlmodzxzldep  48421  blen1b  48509  dig2bits  48535  nn0sumshdiglem1  48542  0aryfvalelfv  48556  itcovalsuc  48588  prelrrx2b  48635  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  rrx2linest2  48665  elrrx2linest2  48666  spheres  48667  2sphere  48670  2sphere0  48671  line2ylem  48672  line2  48673  line2xlem  48674  line2x  48675  line2y  48676  itscnhlc0yqe  48680  itschlc0yqe  48681  itscnhlc0xyqsol  48686  itschlc0xyqsol1  48687  itsclc0xyqsolr  48690  itsclc0  48692  itsclc0b  48693  itsclinecirc0b  48695  itsclquadb  48697  itsclquadeu  48698  itscnhlinecirc02p  48706  resinsnALT  48773  sepnsepolem2  48820  sepnsepo  48821  sepfsepc  48825  iscnrm3rlem8  48844  iscnrm3r  48845  iscnrm3llem2  48847  iscnrm3l  48848  oppcendc  48906  isisod  48910  oppcthinendcALT  49090  functhinclem2  49094  fullthinc2  49100  thincciso  49102  thinccisod  49103  termcpropd  49135  fulltermc2  49144  oduoppcciso  49170  aacllem  49320