Theorem eqeq1d 2736

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 2727	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	biimpi 216	. . 3 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		bibi1 351	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	alimi 1807	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		albi 1814	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)) → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
7	1, 3, 5, 6	4syl 19	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
8		dfcleq 2727	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
9		dfcleq 2727	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
10	7, 8, 9	3bitr4g 314	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1534   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  eqeq1  2738  eqcomd  2740  eqeq2d  2745  eqeqan12d  2748  neeq1d  2997  rspcedeq1vd  3628  csbconstg  3926  csbhypf  3936  csbiebt  3937  csbiebg  3940  sbceq2g  4424  csbie2df  4448  disjeq0  4461  disjssun  4473  mosneq  4846  preq12b  4854  preq12bg  4857  elpreqprlem  4870  disji2  5131  invdisjrab  5134  disjprg  5143  disjxun  5145  iin0  5367  opthg  5487  opeqsng  5512  propeqop  5516  wefrc  5682  xpcan  6197  xpcan2  6198  dmsnopg  6234  rnmpt0f  6264  reuop  6314  dfpo2  6317  sspred  6331  onfr  6424  unisucg  6463  nsuceq0  6468  iotaeq  6527  iotabi  6528  fneq1  6659  fnun  6682  fnresdisj  6688  fnimadisj  6700  fnimaeq0  6701  foeq1  6816  fveqeq2d  6914  fvun1  6999  fvmptdv2  7033  fndmdifeq0  7063  fneqeql  7065  dffo3  7121  dffo3f  7125  fnnfpeq0  7197  foeqcnvco  7319  f1eqcocnv  7320  isofrlem  7359  eqfunresadj  7379  ovanraleqv  7454  f1opr  7488  eloprabga  7540  eloprabgaOLD  7541  ovmpodv2  7590  ov3  7595  ovelimab  7610  caovcang  7633  caovcan  7636  caovmo  7669  caofinvl  7728  caofid1  7731  caofid2  7732  caonncan  7739  tfisi  7879  mptcnfimad  8009  oteqimp  8031  br1steqg  8034  br2ndeqg  8035  eqop  8054  reldm  8067  mposn  8126  fparlem1  8135  fparlem2  8136  fsplit  8140  frxp  8149  xporderlem  8150  fnwelem  8154  xpord2lem  8165  xpord3lem  8172  poseq  8181  soseq  8182  fnsuppeq0  8215  suppssov1  8220  suppssov2  8221  suppofss1d  8227  suppofss2d  8228  tposfo2  8272  mpocurryd  8292  iinon  8378  onnseq  8382  tz7.49  8483  seqomlem2  8489  oe0m1  8557  om0r  8575  oe1m  8581  oawordeulem  8590  oawordeu  8591  oarec  8598  omord  8604  oneo  8617  omeu  8621  oeeui  8638  nnm0r  8646  nnmord  8668  nnawordex  8673  nnaordex2  8675  nnneo  8691  nneob  8692  omopth  8698  nnasmo  8699  ereq1  8750  eqerlem  8778  qsdisj  8832  erov  8852  eceqoveq  8860  mapsnd  8924  endisj  9096  pw2f1olem  9114  enfixsn  9119  disjenex  9173  domssex2  9175  xpf1o  9177  mapxpen  9181  unxpdomlem2  9284  enp1ilem  9309  fodomfib  9366  fodomfibOLD  9368  fipreima  9395  opthreg  9655  cantnfp1lem3  9717  ssttrcl  9752  ttrcltr  9753  ttrclss  9757  ttrclselem2  9763  frmin  9786  updjud  9971  pm54.43  10038  dfac5  10166  dfacacn  10179  kmlem9  10196  cfeq0  10293  cfss  10302  cfslb  10303  fin23lem22  10364  fin23lem12  10368  fin23lem19  10373  fin23lem30  10379  fin23lem33  10382  fin1a2lem6  10442  axcc2lem  10473  axdc3lem2  10488  axdc3lem3  10489  axdc3lem4  10490  axdc3  10491  axdc4lem  10492  zorn2lem7  10539  ttukeylem3  10548  ttukeylem6  10551  ttukey2g  10553  fodomb  10563  axacndlem5  10648  fpwwe2cbv  10667  fpwwe2lem2  10669  fpwwe2lem3  10670  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe  10683  pwfseqlem2  10696  pwxpndom2  10702  addnidpi  10938  ltexpi  10939  recmulnq  11001  ltexnq  11012  halfnq  11013  archnq  11017  ltexpri  11080  recexpr  11088  addsrpr  11112  mulsrpr  11113  00sr  11136  negexsr  11139  recexsrlem  11140  recexsr  11144  axrnegex  11199  axrrecex  11200  00id  11433  mul02  11436  addrid  11438  cnegex  11439  cnegex2  11440  subval  11496  subadd  11508  subadd2  11509  subsub23  11510  addsubeq4  11520  subcan2  11531  negcon1  11558  subcan  11561  addrsub  11677  ltordlem  11785  ltord1  11786  recex  11892  mul0or  11900  muleqadd  11904  receu  11905  mulcan1g  11913  divval  11921  divmul  11922  rec11  11962  ldiv  12098  rdiv  12099  zdiv  12685  uzin  12915  xaddval  13261  xmulval  13263  xnn0xadd0  13285  xnegdi  13286  ioo0  13408  ico0  13429  ioc0  13430  icc0  13431  1fv  13683  fzon  13716  fvinim0ffz  13821  flbi  13852  mod0  13912  modmuladdnn0  13952  modirr  13979  addmodlteq  13983  uzrdgfni  13995  axdc4uzlem  14020  fsuppmapnn0fiubex  14029  mptnn0fsupp  14034  seqid  14084  seqz  14087  expval  14100  expeq0  14129  sqeqor  14251  nn0opth2  14307  hashdom  14414  elprchashprn2  14431  hashbc  14488  hashf1lem1  14490  hash2pwpr  14511  ccat0  14610  wrdl1s1  14648  ccatws1lenp1b  14655  pfxsuff1eqwrdeq  14733  swrdccatin2  14763  pfxccatin12lem2  14765  2cshwcshw  14860  scshwfzeqfzo  14861  cshimadifsn  14864  cshimadifsn0  14865  s2f1o  14951  wrdlen2i  14977  2swrd2eqwrdeq  14988  wwlktovf  14991  wwlktovf1  14992  wwlktovfo  14993  wrd2f1tovbij  14995  relexp0g  15057  relexpsucnnr  15060  dfrtrcl2  15097  mulre  15156  rennim  15274  cnpart  15275  01sqrex  15284  resqrex  15285  sqrmo  15286  resqrtcl  15288  resqrtthlem  15289  sqrtgt0  15293  sqrtneg  15302  sqrtsq2  15303  absmod0  15338  sqreulem  15394  sqreu  15395  sqrtthlem  15397  eqsqrtd  15402  reusq0  15497  fsum00  15830  telfsumo  15834  prodss  15979  fprodle  16028  tanaddlem  16198  absefib  16230  efieq1re  16231  divides  16288  dvdsval2  16289  nndivides  16296  dvds0lem  16300  dvds1lem  16301  dvds2lem  16302  negdvdsb  16306  muldvds1  16314  muldvds2  16315  dvdscmulr  16318  dvdsmulcr  16319  dvdstr  16327  dvdsabseq  16346  divconjdvds  16348  odd2np1lem  16373  odd2np1  16374  even2n  16375  oddm1even  16376  2tp1odd  16385  opeo  16398  omeo  16399  m1exp1  16409  divalglem4  16429  divalglem8  16433  divalgb  16437  bitsuz  16507  smupvallem  16516  gcdaddmlem  16557  gcdabs1  16562  bezoutlem3  16574  rplpwr  16591  rprpwr  16592  alginv  16608  algcvga  16612  algfx  16613  eucalgval2  16614  coprmdvds  16686  qredeq  16690  qredeu  16691  coprmprod  16694  coprmproddvdslem  16695  divgcdcoprm0  16698  divgcdcoprmex  16699  cncongr1  16700  rpexp  16755  rpexp12i  16757  cncongrprm  16762  qnumdenbi  16777  phival  16800  phicl2  16801  dfphi2  16807  phiprmpw  16809  phimullem  16812  eulerthlem1  16814  eulerthlem2  16815  eulerth  16816  fermltl  16817  hashgcdlem  16821  phisum  16823  odzval  16824  odzdvds  16828  reumodprminv  16837  modprm0  16838  nnnn0modprm0  16839  modprmn0modprm0  16840  coprimeprodsq  16841  coprimeprodsq2  16842  pythagtriplem2  16850  pythagtrip  16867  pcval  16877  pceulem  16878  pcqmul  16886  pcqcl  16889  pcabs  16908  pcgcd1  16910  pc2dvds  16912  pcaddlem  16921  pcadd  16922  pcmpt  16925  prmpwdvds  16937  pockthi  16940  unbenlem  16941  4sqlem12  16989  ramz  17058  ramcl  17062  cshwrepswhash1  17136  imasval  17557  fvprif  17607  iscat  17716  iscatd  17717  catidex  17718  catideu  17719  cidfval  17720  cidval  17721  catidd  17724  catlid  17727  catrid  17728  catpropd  17753  cidpropd  17754  issect  17800  dfiso2  17819  invcoisoid  17839  isocoinvid  17840  setcepi  18141  latleeqj2  18509  latleeqm2  18525  oduclatb  18564  mgmidmo  18685  grpidval  18686  grpidpropd  18687  ismgmid  18690  ismgmid2  18693  mgmidsssn0  18697  grpinvalem  18698  grprida  18700  gsumvalx  18701  gsumpropd  18703  gsumpropd2lem  18704  gsumress  18707  gsumval2  18711  ismnddef  18761  sgrpidmnd  18764  ismndd  18781  mndpropd  18784  mndinvmod  18789  mnd1  18804  ismhm  18810  gsumvallem2  18859  frmdgsum  18887  frmdup3  18892  efmndmnd  18914  smndex1mnd  18935  sgrp2rid2  18951  sgrp2rid2ex  18952  pwmnd  18962  grpinvex  18973  isgrpd2  18986  isgrpd  18988  dfgrp2  18992  grpinveu  19004  grpinvval  19010  grplinv  19019  isgrpinv  19023  grplrinv  19026  grpidinv2  19027  grpidinv  19028  grplmulf1o  19043  grpraddf1o  19044  grpsubeq0  19056  grpsubadd  19058  dfgrp3lem  19068  dfgrp3  19069  grp1  19077  imasgrp2  19085  qusgrp2  19088  mhmmnd  19094  ghmgrp  19096  mulgval  19101  mulgaddcom  19128  eqg0el  19213  cycsubmel  19230  ghmeqker  19273  ghmf1  19276  conjnmzb  19283  ghmqusker  19317  isga  19321  subgga  19330  gaorb  19337  gaorber  19338  gastacl  19339  gastacos  19340  orbsta  19343  symgfix2  19448  gsmsymgrfixlem1  19459  gsmsymgrfix  19460  gsmsymgreq  19464  symgfixelq  19465  f1omvdconj  19478  pmtrdifwrdel2  19518  psgnunilem1  19525  psgnunilem2  19527  psgnunilem3  19528  psgnunilem4  19529  odval  19566  odid  19570  odlem2  19571  oddvdsnn0  19576  odnncl  19577  oddvds  19579  odcong  19581  odeq  19582  odmulgid  19586  odmulgeq  19589  gexval  19610  gexid  19613  gexlem2  19614  gexdvdsi  19615  gexdvds  19616  subgpgp  19629  sylow1lem1  19630  sylow1lem4  19633  sylow2alem1  19649  sylow2alem2  19650  sylow2blem2  19653  sylow3lem6  19664  lsmdisj3a  19721  lsmdisj3b  19722  pj1val  19727  pj1eq  19732  efgredlemd  19776  efgredlem  19779  efgred  19780  efgrelexlema  19781  frgpup3  19810  ablsubadd  19841  ablsubsub23  19856  iscyggen  19912  cyggenod  19916  gsumval3lem2  19938  gsumval3  19939  gsummptnn0fz  20018  dmdprd  20032  dprddisj  20043  dprdfeq0  20056  dprdf11  20057  dmdprdpr  20083  dpjeq  20093  ablfacrp  20100  pgpfac1lem2  20109  pgpfac1lem3  20111  pgpfac1lem5  20113  pgpfac1  20114  pgpfaclem1  20115  pgpfaclem2  20116  pgpfaclem3  20117  ablfaclem2  20120  ablfaclem3  20121  ablfac2  20123  rngmneg1  20184  rngmneg2  20185  ringurd  20202  srgrz  20224  srglz  20225  srgisid  20226  srg1zr  20232  ringid  20287  qusring2  20347  opprring  20363  dvdsrval  20377  dvdsrmul  20380  dvdsr01  20387  dvdsr02  20388  crngunit  20394  ringunitnzdiv  20414  dvreq1  20427  dvdsrpropd  20432  irredn0  20439  irredrmul  20443  irredmul  20445  rngisomring  20483  rhmdvdsr  20524  lringuplu  20560  subrg1  20598  subrgdvds  20602  isrrg  20714  rrgeq0i  20715  rrgeq0  20716  domneq0  20724  isdomn4  20732  domnlcanb  20736  domnrcanb  20738  drngid2  20768  drngmul0orOLD  20777  isdrngd  20781  isdrngdOLD  20783  fidomndrnglem  20789  isabv  20828  issrngd  20872  islmod  20878  islmodd  20880  lmodprop2d  20938  mptscmfsupp0  20941  lss1d  20978  lspextmo  21072  lvecvs0or  21127  lvecvscan  21130  lvecvscan2  21131  lbsacsbs  21175  rngqiprngimf1lem  21321  rng2idl1cntr  21332  prmirredlem  21500  pzriprnglem7  21515  pzriprnglem13  21521  chrdvds  21558  chrnzr  21562  domnchr  21564  znval  21567  zncyg  21584  znfld  21596  znunit  21599  znrrg  21601  frgpcyg  21609  psgndiflemB  21635  psgndiflemA  21636  ipeq0  21673  ip2eq  21688  elocv  21703  ocvi  21704  obsne0  21762  dsmmacl  21778  dsmmlss  21781  frlmphl  21818  frlmup4  21838  islindf4  21875  islindf5  21876  mplsubrglem  22041  mplmon2  22102  evlslem1  22123  evlseu  22124  evlsval  22127  evlsval2  22128  ismhp3  22163  mhpsclcl  22168  mhpvarcl  22169  mhpmulcl  22170  psdmul  22187  cply1coe0bi  22321  gsummoncoe1  22327  evl1vsd  22363  dmatel  22514  dmatelnd  22517  dmatmulcl  22521  scmateALT  22533  mdetdiaglem  22619  mdetunilem1  22633  mdetunilem3  22635  mdetunilem4  22636  mdetunilem9  22641  symgmatr01lem  22674  symgmatr01  22675  gsummatr01lem1  22676  gsummatr01lem4  22679  gsummatr01  22680  smadiadetlem3  22689  cramerlem3  22710  pmatcoe1fsupp  22722  cpmatel  22732  1elcpmat  22736  cpmatmcllem  22739  cpmatmcl  22740  d1mat2pmat  22760  m2cpminvid2lem  22775  m2cpminvid2  22776  decpmatmulsumfsupp  22794  pmatcollpw2lem  22798  pmatcollpwscmatlem1  22810  mp2pm2mplem4  22830  pm2mpmhmlem1  22839  chpscmat  22863  cpmidpmatlem3  22893  cayleyhamilton0  22910  cayleyhamiltonALT  22912  cayleyhamilton1  22913  0ntr  23094  ntreq0  23100  cldlp  23173  pnrmopn  23366  hausnei2  23376  cnhaus  23377  nrmsep  23380  isnrm2  23381  regsep2  23399  dishaus  23405  ordthauslem  23406  iscmp  23411  cmpsublem  23422  cmpsub  23423  tgcmp  23424  sscmp  23428  hauscmplem  23429  cmpfi  23431  bwth  23433  connsuba  23443  nconnsubb  23446  isref  23532  islocfin  23540  elpt  23595  elptr  23596  pthaus  23661  txcmp  23666  hausdiag  23668  txhaus  23670  txkgen  23675  xkohaus  23676  xkococnlem  23682  regr1lem  23762  fbasrn  23907  fmfnfmlem3  23979  flimtopon  23993  fclstopon  24035  alexsubb  24069  symgtgp  24129  qustgpopn  24143  qustgphaus  24146  ustuqtop  24270  isusp  24285  ispsmet  24329  psmet0  24333  ismet  24348  isxmet  24349  xmeteq0  24363  metn0  24385  xmetres2  24386  imasf1oxmet  24400  xblss2ps  24426  xblss2  24427  xmseq0  24489  comet  24541  stdbdxmet  24543  methaus  24548  dscmet  24600  nrmmetd  24602  nmeq0  24646  tngngp  24690  tngngp3  24692  nlmmul0or  24719  cnmet  24807  xrsxmet  24844  metnrmlem3  24896  icopnfcnv  24986  iccpnfcnv  24988  ishtpy  25017  isphtpy  25026  phtpyi  25029  om1elbas  25078  elpi1i  25092  pi1grplem  25095  isclmp  25143  cphsqrtcl2  25233  tcphcph  25284  bcth3  25378  rrxcph  25439  rrxmet  25455  ivth2  25503  iundisj2  25597  dyaddisj  25644  volivth  25655  mbfinf  25713  i1f1lem  25737  i1fmullem  25742  i1fmulclem  25751  i1fres  25754  itg1climres  25763  mbfi1fseqlem4  25767  dvnres  25981  dvcobr  25997  dvcobrOLD  25998  rolle  26042  cmvth  26043  cmvthOLD  26044  deg1leb  26148  ismon1p  26196  q1peqb  26209  dvdsr1p  26217  ply1remlem  26218  fta1glem2  26222  idomrootle  26226  elply2  26249  ne0p  26260  coeeu  26278  coelem  26279  coeeq  26280  dgrle  26296  coeaddlem  26302  plymul0or  26336  ofmulrt  26337  plydivlem3  26351  plydivlem4  26352  plydivex  26353  plydiveu  26354  plydivalg  26355  quotlem  26356  plyremlem  26360  quotcan  26365  plyexmo  26369  elqaalem3  26377  qaa  26379  iaa  26381  aareccl  26382  aacjcl  26383  aannenlem2  26385  reeff1o  26505  sineq0  26580  coseq1  26581  efeq1  26584  recosf1o  26591  logeftb  26639  cosarg0d  26665  logtayl  26716  cxpval  26720  cxpeq0  26734  root1eq1  26812  cxpeq  26814  logbgcd1irr  26851  angrtmuld  26865  affineequiv  26880  affineequiv3  26882  angpieqvdlem2  26886  quad2  26896  dcubic1lem  26900  dcubic2  26901  dcubic  26903  mcubic  26904  cubic2  26905  dquartlem1  26908  dquart  26910  quart  26918  atandm2  26934  atandm4  26936  atantan  26980  wilthlem2  27126  wilthlem3  27127  muval2  27191  isnsqf  27192  mumullem2  27237  sqff1o  27239  muinv  27250  mpodvdsmulf1o  27251  dvdsmulf1o  27253  dchrelbas2  27295  dchrmullid  27310  dchrfi  27313  lgsval  27359  lgsdir  27390  lgsne0  27393  lgsprme0  27397  lgsdirnn0  27402  lgsqrlem1  27404  lgsqr  27409  gausslemma2dlem0c  27416  gausslemma2dlem0i  27422  gausslemma2dlem7  27431  gausslemma2d  27432  lgseisenlem2  27434  lgsquadlem1  27438  lgsquadlem2  27439  lgsquad2lem2  27443  lgsquad3  27445  m1lgs  27446  2lgs  27465  2sqlem7  27482  2sqlem8  27484  2sqlem9  27485  2sqlem11  27487  2sq  27488  2sq2  27491  2sqmo  27495  addsq2reu  27498  addsqn2reu  27499  addsqrexnreu  27500  addsqnreup  27501  addsq2nreurex  27502  2sqreulem1  27504  2sqreultlem  27505  2sqreunnlem1  27507  2sqreunnltlem  27508  2sqreulem4  27512  2sqreuop  27520  2sqreuopnn  27521  2sqreuoplt  27522  2sqreuopltb  27523  2sqreuopnnlt  27524  2sqreuopnnltb  27525  2sqreuopb  27526  dchrisumlem1  27547  dchrvmaeq0  27562  dchrisum0re  27571  ostth3  27696  sltval  27706  nosepssdm  27745  nosupprefixmo  27759  noinfprefixmo  27760  nosupcbv  27761  nosupdm  27763  nosupfv  27765  nosupres  27766  nosupbnd1lem1  27767  nosupbnd1lem3  27769  nosupbnd1lem5  27771  noinfcbv  27776  noinfdm  27778  noinffv  27780  noinfres  27781  noinfbnd1lem3  27784  noinfbnd1lem5  27786  eqscut  27864  scutbdaylt  27877  made0  27926  madecut  27935  negsid  28087  negsex  28089  subadds  28114  divsmo  28224  muls0ord  28225  divsval  28229  norecdiv  28230  divsmulw  28232  divs1  28243  precsexlem8  28252  precsexlem9  28253  precsexlem11  28255  precsex  28256  recsex  28257  abssor  28284  elons  28290  noseqrdgfn  28326  n0seo  28419  zseo  28420  nohalf  28421  expsne0  28428  renegscl  28444  istrkg3ld  28483  axtgcgrid  28485  axtgsegcon  28486  axtg5seg  28487  axtgupdim2  28493  tgjustc1  28497  tgjustc2  28498  iscgrg  28534  isismt  28556  legov  28607  legov2  28608  hlcgreu  28640  mirreu3  28676  mircgr  28679  mirbtwn  28680  ismir  28681  mireq  28687  ismidb  28800  lmiopp  28824  dfcgra2  28852  inaghl  28867  f1otrg  28893  ttgval  28897  ttgvalOLD  28898  ttgelitv  28911  brbtwn  28928  brcgr  28929  colinearalglem2  28936  colinearalg  28939  axsegconlem1  28946  axsegcon  28956  ax5seglem4  28961  ax5seglem5  28962  axpaschlem  28969  axpasch  28970  axlowdimlem16  28986  axeuclidlem  28991  axeuclid  28992  axcontlem2  28994  axcontlem4  28996  axcontlem5  28997  edglnl  29174  usgredg2ALT  29224  usgredgprvALT  29226  usgrnloopvALT  29232  ushgredgedgloop  29262  edg0usgr  29284  nb3grpr  29413  cplgr1v  29461  cusgrsize  29486  vtxdgfval  29499  vtxdeqd  29509  vtxdun  29513  vtxd0nedgb  29520  vtxdusgr0edgnelALT  29528  1loopgrvd2  29535  usgruvtxvdb  29561  usgrvd0nedg  29565  vtxdginducedm1  29575  rusgrpropedg  29616  wksfval  29641  wlklenvclwlk  29687  iswlkon  29689  ispth  29755  upgrwlkdvdelem  29768  crctcshwlkn0lem6  29844  wwlknon  29886  wwlksm1edg  29910  wwlksnextbi  29923  wwlksnextfun  29927  wwlksnextinj  29928  wwlksnextsurj  29929  wwlksnextbij  29931  wlksnwwlknvbij  29937  wwlksnextproplem3  29940  wwlksnextprop  29941  wspn0  29953  umgr2adedgwlkonALT  29976  umgr2adedgspth  29977  umgr2wlkon  29979  rusgrnumwwlkslem  29998  rusgrnumwwlkb0  30000  rusgrnumwwlks  30003  clwlkclwwlklem2a4  30025  clwlknf1oclwwlknlem2  30110  clwlknf1oclwwlkn  30112  isclwwlknon  30119  clwwlknon1loop  30126  s2elclwwlknon2  30132  clwwlknonwwlknonb  30134  clwwlkvbij  30141  uhgr3cyclex  30210  fusgreg2wsplem  30361  fusgr2wsp2nb  30362  fusgreghash2wsp  30366  frrusgrord0  30368  2clwwlkel  30377  extwwlkfab  30380  extwwlkfabel  30381  clwwlknonclwlknonf1o  30390  dlwwlknondlwlknonf1o  30393  wlkl0  30395  numclwwlk2lem1  30404  numclwlk2lem2f  30405  numclwlk2lem2f1o  30407  numclwwlk5  30416  ex-opab  30460  isgrpo  30525  isgrpoi  30526  grpoidinvlem3  30534  grpoideu  30537  gidval  30540  grpoidinv2  30543  grpoinveu  30547  grpoinvval  30551  grpoinv  30553  vciOLD  30589  isvclem  30605  cnidOLD  30610  isnvlem  30638  nvmul0or  30678  imsmetlem  30718  diporthcom  30744  ipz  30747  nmlno0  30823  ajfval  30837  hmoval  30838  isphg  30845  isph  30850  ip2eqi  30884  ajval  30889  hvmul0or  31053  hvsubeq0  31096  hvaddeq0  31097  hvaddcan  31098  hvmulcan  31100  hvmulcan2  31101  hvsubadd  31105  his6  31127  hial0  31130  hial02  31131  hi2eq  31133  orthcom  31136  normlem7tALT  31147  normsub0  31164  normpyth  31173  hilid  31189  hhssnv  31292  ocel  31309  ocsh  31311  ocorth  31319  ocin  31324  occllem  31331  choc0  31354  pjpreeq  31426  omlsi  31432  pjoc1  31462  pjoml  31464  pjoc2  31467  chm0  31519  chocin  31523  chlejb1  31540  chlejb2  31541  chjo  31543  h1deoi  31577  h1de2i  31581  pjoml6i  31617  pjoml2  31639  pjoml3  31640  pjch  31722  hodsi  31803  hodid  31820  eigorth  31866  elunop  31900  adjeu  31917  adjval  31918  eigvecval  31924  unopf1o  31944  adj1  31961  adjeq  31963  hmdmadj  31968  lnopeq0i  32035  lnopeqi  32036  lnopeq  32037  lnfn0  32075  riesz4i  32091  riesz4  32092  riesz1  32093  cnlnadjlem3  32097  cnlnadjlem5  32099  cnlnadjeu  32106  cnlnssadj  32108  nmopadjlei  32116  opsqrlem1  32168  hmopidmpji  32180  pjimai  32204  isst  32241  ishst  32242  hstel2  32247  stadd3i  32276  stri  32285  largei  32295  golem2  32300  superpos  32382  sumdmdii  32443  mddmdin0i  32459  opreu2reuALT  32504  difeq  32545  elim2if  32564  disji2f  32596  disjif2  32600  disjxpin  32607  iundisj2f  32609  disjunsn  32613  fmptco1f1o  32649  ofpreima  32681  fnpreimac  32687  ressupprn  32704  curry2ima  32723  preiman0  32724  xrofsup  32777  iundisj2fi  32804  f1ocnt  32809  fzo0opth  32812  fprodex01  32831  xdivval  32885  xrecex  32886  xreceu  32888  xdivmul  32891  rexdiv  32892  wrdt2ind  32922  mndlrinvb  33012  mndlactfo  33014  mndractfo  33016  mndlactf1o  33017  mndractf1o  33018  gsummpt2d  33034  gsumwun  33050  fzo0pmtrlast  33094  cyc3genpm  33154  cycpmconjslem2  33157  isslmd  33190  slmdlema  33191  urpropd  33221  elrgspnlem4  33234  erlcl1  33246  erlcl2  33247  erldi  33248  erlbrd  33249  erler  33251  rloccring  33256  domnlcanOLD  33263  isdrng4  33278  fracerl  33287  fracfld  33289  resv1r  33347  islinds5  33374  linds2eq  33388  dvdsruassoi  33391  dvdsruasso  33392  dvdsruasso2  33393  quslsm  33412  rhmimaidl  33439  qsidomlem2  33460  ssdifidllem  33463  ssdifidl  33464  ssdifidlprm  33465  opprqus0g  33497  qsdrngilem  33501  unitmulrprm  33535  1arithidom  33544  1arithufdlem3  33553  1arithufdlem4  33554  ply1dg1rt  33583  r1pid2OLD  33608  lbsdiflsp0  33653  fedgmullem1  33656  fedgmullem2  33657  irngss  33701  irngnzply1lem  33704  ply1annidllem  33708  ply1annnr  33710  minplymindeg  33715  minplyann  33716  minplyirredlem  33717  minplyirred  33718  irngnminplynz  33719  irredminply  33721  algextdeglem6  33727  algextdeglem7  33728  rtelextdg2lem  33731  fldext2chn  33733  constrsuc  33742  constrsslem  33745  constrconj  33749  1smat1  33764  iscref  33804  metidval  33850  metidv  33852  metider  33854  pstmxmet  33857  xrmulc1cn  33890  ind1a  33999  prodindf  34003  esumfsup  34050  esumpcvgval  34058  esumcvg  34066  inelsros  34158  diffiunisros  34159  ismeas  34179  isrnmeas  34180  brae  34221  braew  34222  dya2iocuni  34264  elcarsg  34286  eulerpartleme  34344  eulerpartlemv  34345  eulerpartlemb  34349  eulerpartgbij  34353  eulerpartlemr  34355  eulerpartlemgvv  34357  eulerpartlemgh  34359  eulerpartlemn  34362  elprob  34390  ballotlemi  34481  ballotlemi1  34483  ballotlemii  34484  ballotlemsima  34496  ballotlemfrcn0  34510  sgn0bi  34528  signsw0g  34549  signswmnd  34550  signstfvc  34567  prodfzo03  34596  reprval  34603  reprsum  34606  reprsuc  34608  reprpmtf1o  34619  axtgupdim2ALTV  34661  brafs  34665  bnj125  34864  bnj154  34870  bnj526  34880  bnj609  34909  bnj893  34920  bnj1321  35019  bnj1491  35049  nummin  35083  subgrwlk  35116  loop1cycl  35121  subfacp1lem3  35166  subfacp1lem5  35168  subfacp1lem6  35169  cnpconn  35214  txpconn  35216  ptpconn  35217  indispconn  35218  connpconn  35219  cvxpconn  35226  cvmscbv  35242  cvmsi  35249  cvmsval  35250  cvmsdisj  35254  cvmsss2  35258  cvmliftmo  35268  cvmliftlem14  35281  cvmliftiota  35285  cvmlift2lem12  35298  cvmlift2lem13  35299  cvmlift2  35300  cvmliftphtlem  35301  cvmlift3lem2  35304  cvmlift3lem4  35306  cvmlift3lem6  35308  cvmlift3lem7  35309  cvmlift3lem9  35311  cvmlift3  35312  snmlval  35315  satffunlem  35385  prv1n  35415  mrsub0  35500  mrsubcn  35503  ismfs  35533  sinccvglem  35656  br6  35736  brbigcup  35879  imageval  35911  funpartlem  35923  dfrdg4  35932  altopthsn  35942  brsegle  36089  rankeq1o  36152  cbviotadavw  36251  subtr  36296  opnbnd  36307  cldbnd  36308  isfne  36321  topfneec  36337  neibastop3  36344  cnndvlem2  36520  bj-imdirval2  37165  bj-imdirid  37168  bj-imdirco  37172  bj-inftyexpiinj  37191  bj-isrvecd  37280  bj-isrvec2  37282  bj-bary1lem1  37293  bj-bary1  37294  finxp00  37384  nlpfvineqsn  37391  pibp19  37396  pibt2  37399  unccur  37589  matunitlindflem2  37603  ptrecube  37606  poimirlem4  37610  poimirlem19  37625  poimirlem23  37629  poimirlem25  37631  poimirlem27  37633  poimirlem28  37634  poimirlem31  37637  poimirlem32  37638  broucube  37640  mblfinlem2  37644  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  mbfresfi  37652  itg2addnclem  37657  itg2addnclem3  37659  itg2addnc  37660  ftc2nc  37688  cover2  37701  sdclem2  37728  fdc  37731  metf1o  37741  istotbnd3  37757  0totbnd  37759  sstotbnd2  37760  equivtotbnd  37764  totbndbnd  37775  prdstotbnd  37780  heibor1  37796  rrnmet  37815  isexid  37833  ismgmOLD  37836  opidonOLD  37838  exidu1  37842  cmpidelt  37845  exidreslem  37863  exidres  37864  exidresid  37865  grpoeqdivid  37867  elghomlem1OLD  37871  grpokerinj  37879  isrngo  37883  isrngod  37884  rngoideu  37889  isgrpda  37941  isdrngo2  37944  isdrngo3  37945  isrngohom  37951  divrngidl  38014  dmnnzd  38061  dmncan1  38062  disjeccnvep  38265  disjressuc2  38369  qsdisjALTV  38596  dmqseqeq1  38624  unidmqseq  38636  disjdmqseq  38786  eldisjlem19  38791  riotasvd  38937  toycom  38954  islshpsm  38961  lshpnel2N  38966  lsatfixedN  38990  islshpat  38998  lcvexchlem4  39018  l1cvpat  39035  lkr0f  39075  lkrsc  39078  lshpkrlem1  39091  lkreqN  39151  isopos  39161  oposlem  39163  opcon2b  39178  cmtbr3N  39235  cvlcvrp  39321  hlrelat5N  39383  cvrval5  39397  cvrat4  39425  3atlem5  39469  2at0mat0  39507  psubclsetN  39918  4atex2  40059  isldil  40092  ltrnu  40103  ltrnid  40117  isdilN  40136  trlnid  40161  cdleme21k  40320  cdleme29b  40357  cdlemefrs29pre00  40377  cdlemefrs29bpre0  40378  cdlemefrs29cpre1  40380  cdleme32fva  40419  cdleme42b  40460  cdleme50ex  40541  cdleme  40542  cdlemg1a  40552  ltrniotaval  40563  cdlemeiota  40567  tendoid0  40807  cdlemksv2  40829  cdlemkuv2  40849  cdlemk36  40895  cdlemk42  40923  cdlemk  40956  tendoex  40957  cdleml3N  40960  cdleml5N  40962  tendospcanN  41005  cdlemm10N  41100  dihffval  41212  dihfval  41213  dihlsscpre  41216  islpolN  41465  mapdhval  41706  mapdheq  41710  hdmap1fval  41778  hdmap1val  41780  hdmap1eq  41783  hdmap1cbv  41784  hdmapval2lem  41813  hdmap11  41830  hdmap14lem2a  41849  hdmap14lem6  41855  hgmapval  41869  hlhillcs  41944  hlhilphllem  41945  aks4d1  42070  isprimroot  42074  mndmolinv  42076  linvh  42077  primrootsunit1  42078  primrootsunit  42079  primrootscoprmpow  42080  primrootscoprbij  42083  primrootlekpowne0  42086  primrootspoweq0  42087  ringexp0nn  42115  aks6d1c5lem1  42117  sticksstones8  42134  sticksstones9  42135  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  sticksstones12  42139  sticksstones16  42143  sticksstones17  42144  sticksstones18  42145  sticksstones19  42146  aks6d1c6lem4  42154  aks6d1c6isolem3  42157  rhmqusspan  42166  grpods  42175  unitscyglem1  42176  unitscyglem2  42177  unitscyglem3  42178  unitscyglem5  42180  metakunt6  42191  metakunt15  42200  metakunt16  42201  metakunt27  42212  metakunt28  42213  metakunt32  42217  expeq1d  42337  zdivgd  42350  ef11d  42353  resubval  42373  renegadd  42378  resubeu  42383  resubadd  42385  sn-negex12  42422  addinvcom  42437  sn-mul02  42446  mulgt0con1d  42464  mulgt0con2d  42465  fimgmcyclem  42519  fidomncyc  42521  evlsval3  42545  fsuppind  42576  mhphflem  42582  prjspnfv01  42610  prjspner01  42611  prjspner1  42612  prjcrvval  42618  dffltz  42620  flt4lem7  42645  nna4b4nsq  42646  negexpidd  42669  mzpcompact2lem  42738  eldioph  42745  eldioph2lem1  42747  eldioph2lem2  42748  eldioph2  42749  eldioph2b  42750  eldioph3  42753  diophin  42759  diophun  42760  eq0rabdioph  42763  dvdsrabdioph  42797  eldioph4i  42799  diophren  42800  rabren3dioph  42802  fphpd  42803  pellexlem5  42820  pellexlem6  42821  pellex  42822  pell1qrval  42833  pell14qrval  42835  pell1234qrval  42837  pell1234qrreccl  42841  pell1234qrmulcl  42842  pell1234qrdich  42848  pell14qrdich  42856  pell1qr1  42858  pellqrexplicit  42864  rmxycomplete  42905  jm2.27  42996  rmydioph  43002  rmxdiophlem  43003  rmxdioph  43004  pw2f1ocnv  43025  pwssplit4  43077  elmnc  43124  dgraalem  43133  dgraaub  43136  dgraa0p  43137  mpaaeu  43138  mpaaval  43139  mpaalem  43140  aaitgo  43150  rngunsnply  43157  proot1ex  43184  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  44223  expgrowth  44330  bcc0  44335  disjinfi  45134  fsumf1of  45529  limsupmnflem  45675  liminfpnfuz  45771  climxlim2lem  45800  coseq0  45819  icccncfext  45842  dvnmptconst  45896  dvnprodlem1  45901  dvnprodlem2  45902  dvnprodlem3  45903  dvnprod  45904  stoweidlem15  45970  stoweidlem31  45986  stoweidlem35  45990  stoweidlem36  45991  stoweidlem37  45992  stoweidlem43  45998  stoweidlem44  45999  stoweidlem46  46001  stoweidlem55  46010  stoweidlem59  46014  dirkerval2  46049  dirkertrigeqlem1  46053  dirkeritg  46057  dirkercncf  46062  fourierdlem2  46064  fourierdlem3  46065  fourierdlem42  46104  fourierdlem48  46109  fourierdlem49  46110  fourierdlem71  46132  fourierdlem112  46173  fourierdlem113  46174  elaa2lem  46188  etransclem11  46200  etransclem24  46213  etransclem26  46215  etransclem28  46217  etransclem35  46224  ioorrnopnxr  46262  salgenval  46276  intsaluni  46284  salgenn0  46286  salgencl  46287  sssalgen  46290  salgenss  46291  salgenuni  46292  issalgend  46293  dfsalgen2  46296  subsaliuncl  46313  sge0f1o  46337  sge0fodjrnlem  46371  ismea  46406  nnfoctbdjlem  46410  iundjiun  46415  isome  46449  caragenel  46450  ovn0lem  46520  ovnsubaddlem1  46525  smflimlem4  46729  smflim  46732  sigarcol  46819  cfsetsnfsetf  47007  cfsetsnfsetfo  47009  fnbrafvb  47103  afv2fv0  47214  readdcnnred  47252  resubcnnred  47253  cndivrenred  47255  minusmodnep2tmod  47292  fargshiftf1  47365  fargshiftfo  47366  ichexmpl2  47394  ichnreuop  47396  ichreuopeq  47397  elsprel  47399  prproropf1olem4  47430  reupr  47446  reuopreuprim  47450  goldbachthlem2  47470  fmtnoprmfac2lem1  47490  fmtnofac2lem  47492  prmdvdsfmtnof1lem2  47509  mod42tp1mod8  47526  lighneallem2  47530  lighneallem3  47531  lighneallem4  47534  proththd  47538  41prothprm  47543  requad01  47545  requad2  47547  dfeven2  47573  dfeven5  47590  dfodd7  47591  fpprel  47652  fppr2odd  47655  fpprwppr  47663  fpprwpprb  47664  nnsum3primesgbe  47716  isubgredg  47789  ushggricedg  47833  uhgrimisgrgric  47836  isubgr3stgrlem3  47870  isubgr3stgrlem4  47871  isubgr3stgrlem6  47873  grlimgrtrilem2  47897  gpgedgvtx0  47953  gpgedgvtx1  47954  gpgvtxedg0  47955  gpgvtxedg1  47956  upwlksfval  47978  0nodd  48013  2nodd  48015  nnsgrpnmnd  48021  nn0mnd  48022  lidldomn1  48074  zlidlring  48077  uzlidlring  48078  2zrngamgm  48088  2zrngamnd  48090  2zrngagrp  48092  2zrngnmlid2  48100  ztprmneprm  48191  dmatALTbasel  48247  linindslinci  48293  lindslinindsimp1  48302  lindslinindimp2lem4  48306  lindslinindsimp2lem5  48307  linds0  48310  el0ldep  48311  lindsrng01  48313  snlindsntorlem  48315  snlindsntor  48316  ldepspr  48318  lincresunit3  48326  islindeps2  48328  isldepslvec2  48330  zlmodzxzldep  48349  blen1b  48437  dig2bits  48463  nn0sumshdiglem1  48470  0aryfvalelfv  48484  itcovalsuc  48516  prelrrx2b  48563  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  rrx2linest2  48593  elrrx2linest2  48594  spheres  48595  2sphere  48598  2sphere0  48599  line2ylem  48600  line2  48601  line2xlem  48602  line2x  48603  line2y  48604  itscnhlc0yqe  48608  itschlc0yqe  48609  itscnhlc0xyqsol  48614  itschlc0xyqsol1  48615  itsclc0xyqsolr  48618  itsclc0  48620  itsclc0b  48621  itsclinecirc0b  48623  itsclquadb  48625  itsclquadeu  48626  itscnhlinecirc02p  48634  sepnsepolem2  48718  sepnsepo  48719  sepfsepc  48723  iscnrm3rlem8  48743  iscnrm3r  48744  iscnrm3llem2  48746  iscnrm3l  48747  isisod  48806  functhinclem2  48841  fullthinc2  48846  thincciso  48848  thinccisod  48849  oduoppcciso  48881  aacllem  49031