Theorem eqeq1d 2764

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 2755	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	biimpi 218	. . 3 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		bibi1 353	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	alimi 1831	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		albi 1838	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)) → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
7	1, 3, 5, 6	4syl 19	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
8		dfcleq 2755	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
9		dfcleq 2755	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
10	7, 8, 9	3bitr4g 316	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1558   = wceq 1560   ∈ wcel 2142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  eqeq1  2766  eqcomd  2768  eqeq2d  2773  eqeqan12d  2776  neeq1d  3016  csbconstg  3871  csbhypf  3880  csbiebt  3881  csbiebg  3884  sbceq2g  4373  csbie2df  4397  disjeq0  4410  disjssun  4422  mosneq  4800  preq12b  4808  preq12bg  4811  elpreqprlem  4824  disji2  5084  invdisjrab  5087  disjprg  5096  disjxun  5098  iin0  5319  opthg  5445  opeqsng  5472  propeqop  5476  wefrc  5641  xpcan  6162  xpcan2  6163  dmsnopg  6200  rnmpt0f  6230  reuop  6280  dfpo2  6283  sspred  6297  onfr  6385  unisucg  6426  nsuceq0  6431  iotaeq  6489  iotabi  6490  fneq1  6612  fnun  6635  fnresdisj  6641  fnimadisj  6653  fnimaeq0  6654  foeq1  6774  fveqeq2d  6875  fvun1  6958  fvmptdv2  6994  fndmdifeq0  7025  fneqeql  7027  dffo3  7083  dffo3f  7087  fnnfpeq0  7162  foeqcnvco  7284  f1eqcocnv  7285  isofrlem  7324  eqfunresadj  7344  ovanraleqv  7420  f1opr  7452  eloprabga  7505  ovmpodv2  7554  ov3  7559  ovelimab  7574  caovcang  7597  caovcan  7600  caovmo  7633  caofinvl  7692  caofid1  7695  caofid2  7696  caofidlcan  7698  caonncan  7704  tfisi  7839  mptcnfimad  7967  oteqimp  7989  br1steqg  7992  br2ndeqg  7993  eqop  8012  reldm  8025  mposn  8082  fparlem1  8091  fparlem2  8092  fsplit  8096  frxp  8106  xporderlem  8107  fnwelem  8111  xpord2lem  8122  xpord3lem  8129  poseq  8138  soseq  8139  fnsuppeq0  8172  suppssov1  8177  suppssov2  8178  suppofss1d  8184  suppofss2d  8185  tposfo2  8229  mpocurryd  8249  iinon  8311  onnseq  8315  tz7.49  8416  seqomlem2  8422  oe0m1  8490  om0r  8508  oe1m  8514  oawordeulem  8523  oawordeu  8524  oarec  8531  omord  8537  oneo  8550  omeu  8554  oeeui  8572  nnm0r  8580  nnmord  8602  nnawordex  8607  nnaordex2  8609  nnneo  8625  nneob  8626  omopth  8632  nnasmo  8633  ereq1  8686  eqerlem  8714  qsdisj  8776  erov  8796  eceqoveq  8804  mapsnd  8868  endisj  9036  pw2f1olem  9053  enfixsn  9058  disjenex  9107  domssex2  9109  xpf1o  9111  mapxpen  9115  unxpdomlem2  9201  enp1ilem  9222  fodomfib  9273  fodomfibOLD  9274  fipreima  9301  opthreg  9573  cantnfp1lem3  9635  ssttrcl  9670  ttrcltr  9671  ttrclss  9675  ttrclselem2  9681  frmin  9707  updjud  9892  pm54.43  9959  dfac5  10085  dfacacn  10098  kmlem9  10115  cfeq0  10213  cfss  10222  cfslb  10223  fin23lem22  10284  fin23lem12  10288  fin23lem19  10293  fin23lem30  10299  fin23lem33  10302  fin1a2lem6  10362  axcc2lem  10393  axdc3lem2  10408  axdc3lem3  10409  axdc3lem4  10410  axdc3  10411  axdc4lem  10412  zorn2lem7  10459  ttukeylem3  10468  ttukeylem6  10471  ttukey2g  10473  fodomb  10483  axacndlem5  10569  fpwwe2cbv  10588  fpwwe2lem2  10590  fpwwe2lem3  10591  fpwwe2lem11  10599  fpwwe2lem12  10600  fpwwe  10604  pwfseqlem2  10617  pwxpndom2  10623  addnidpi  10859  ltexpi  10860  recmulnq  10922  ltexnq  10933  halfnq  10934  archnq  10938  ltexpri  11001  recexpr  11009  addsrpr  11033  mulsrpr  11034  00sr  11057  negexsr  11060  recexsrlem  11061  recexsr  11065  axrnegex  11120  axrrecex  11121  00id  11358  mul02  11361  addrid  11363  cnegex  11364  cnegex2  11365  subval  11421  subadd  11433  subadd2  11434  subsub23  11435  addsubeq4  11445  subcan2  11456  negcon1  11483  subcan  11486  addrsub  11604  ltordlem  11712  ltord1  11713  recex  11819  mul0or  11827  muleqadd  11831  receu  11832  mulcan1g  11840  divval  11847  divmul  11848  rec11  11889  ldiv  12025  rdiv  12026  ind1a  12206  zdiv  12643  uzin  12875  xaddval  13226  xmulval  13228  xnn0xadd0  13250  xnegdi  13251  ioo0  13374  ico0  13395  ioc0  13396  icc0  13397  1fv  13652  fzon  13686  fvinim0ffz  13795  flbi  13826  mod0  13886  modmuladdnn0  13928  modirr  13955  addmodlteq  13959  uzrdgfni  13971  axdc4uzlem  13996  fsuppmapnn0fiubex  14005  mptnn0fsupp  14010  seqid  14060  seqz  14063  expval  14076  expeq0  14105  sqeqor  14229  nn0opth2  14285  hashdom  14392  elprchashprn2  14409  hashbc  14466  hashf1lem1  14468  hash2pwpr  14489  ccat0  14589  wrdl1s1  14628  ccatws1lenp1b  14635  pfxsuff1eqwrdeq  14712  swrdccatin2  14742  pfxccatin12lem2  14744  2cshwcshw  14838  scshwfzeqfzo  14839  cshimadifsn  14842  cshimadifsn0  14843  s2f1o  14929  wrdlen2i  14955  2swrd2eqwrdeq  14966  wwlktovf  14969  wwlktovf1  14970  wwlktovfo  14971  wrd2f1tovbij  14973  relexp0g  15035  relexpsucnnr  15038  dfrtrcl2  15075  sgn0bi  15116  mulre  15148  rennim  15266  cnpart  15267  01sqrex  15276  resqrex  15277  sqrmo  15278  resqrtcl  15280  resqrtthlem  15281  sqrtgt0  15285  sqrtneg  15294  sqrtsq2  15295  absmod0  15330  sqreulem  15387  sqreu  15388  sqrtthlem  15390  eqsqrtd  15395  reusq0  15492  fsum00  15826  telfsumo  15830  prodss  15977  fprodle  16026  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  difmod0  16321  dvdstr  16328  dvdsabseq  16347  divconjdvds  16349  odd2np1lem  16374  odd2np1  16375  even2n  16376  oddm1even  16377  2tp1odd  16386  opeo  16399  omeo  16400  m1exp1  16410  divalglem4  16430  divalglem8  16434  divalgb  16438  bitsuz  16508  smupvallem  16517  gcdaddmlem  16558  gcdabs1  16563  bezoutlem3  16575  rplpwr  16592  rprpwr  16593  alginv  16609  algcvga  16613  algfx  16614  eucalgval2  16615  coprmdvds  16687  qredeq  16691  qredeu  16692  coprmprod  16695  coprmproddvdslem  16696  divgcdcoprm0  16699  divgcdcoprmex  16700  cncongr1  16701  rpexp  16757  rpexp12i  16759  cncongrprm  16764  qnumdenbi  16779  phival  16802  phicl2  16803  dfphi2  16809  phiprmpw  16811  phimullem  16814  eulerthlem1  16816  eulerthlem2  16817  eulerth  16818  fermltl  16819  hashgcdlem  16823  phisum  16826  odzval  16827  odzdvds  16831  reumodprminv  16840  modprm0  16841  nnnn0modprm0  16842  modprmn0modprm0  16843  coprimeprodsq  16844  coprimeprodsq2  16845  pythagtriplem2  16853  pythagtrip  16870  pcval  16880  pceulem  16881  pcqmul  16889  pcqcl  16892  pcabs  16911  pcgcd1  16913  pc2dvds  16915  pcaddlem  16924  pcadd  16925  pcmpt  16928  prmpwdvds  16940  pockthi  16943  unbenlem  16944  4sqlem12  16992  ramz  17061  ramcl  17065  cshwrepswhash1  17138  imasval  17541  fvprif  17591  iscat  17704  iscatd  17705  catidex  17706  catideu  17707  cidfval  17708  cidval  17709  catidd  17712  catlid  17715  catrid  17716  catpropd  17741  cidpropd  17742  issect  17786  dfiso2  17805  invcoisoid  17825  isocoinvid  17826  setcepi  18121  latleeqj2  18484  latleeqm2  18500  oduclatb  18539  mgmidmo  18694  grpidval  18695  grpidpropd  18696  ismgmid  18699  ismgmid2  18702  mgmidsssn0  18706  grpinvalem  18707  grprida  18709  gsumvalx  18710  gsumpropd  18712  gsumpropd2lem  18713  gsumress  18716  gsumval2  18720  ismnddef  18770  sgrpidmnd  18773  ismndd  18790  mndpropd  18793  mndinvmod  18798  mnd1  18813  ismhm  18819  gsumvallem2  18868  frmdgsum  18896  frmdup3  18901  efmndmnd  18923  smndex1mnd  18947  sgrp2rid2  18963  sgrp2rid2ex  18964  pwmnd  18974  grpinvex  18985  isgrpd2  18998  isgrpd  19000  dfgrp2  19004  grpinveu  19016  grpinvval  19022  grplinv  19031  isgrpinv  19035  grplrinv  19038  grpidinv2  19039  grpidinv  19040  grplmulf1o  19055  grpraddf1o  19056  grpsubeq0  19068  grpsubadd  19070  dfgrp3lem  19080  dfgrp3  19081  grp1  19089  imasgrp2  19097  qusgrp2  19100  mhmmnd  19106  ghmgrp  19108  mulgval  19113  mulgaddcom  19140  eqg0el  19224  cycsubmel  19241  ghmeqker  19283  ghmf1  19286  conjnmzb  19293  ghmqusker  19327  isga  19331  subgga  19340  gaorb  19347  gaorber  19348  gastacl  19349  gastacos  19350  orbsta  19353  symgfix2  19456  gsmsymgrfixlem1  19467  gsmsymgrfix  19468  gsmsymgreq  19472  symgfixelq  19473  f1omvdconj  19486  pmtrdifwrdel2  19526  psgnunilem1  19533  psgnunilem2  19535  psgnunilem3  19536  psgnunilem4  19537  odval  19574  odid  19578  odlem2  19579  oddvdsnn0  19584  odnncl  19585  oddvds  19587  odcong  19589  odeq  19590  odmulgid  19594  odmulgeq  19597  gexval  19618  gexid  19621  gexlem2  19622  gexdvdsi  19623  gexdvds  19624  subgpgp  19637  sylow1lem1  19638  sylow1lem4  19641  sylow2alem1  19657  sylow2alem2  19658  sylow2blem2  19661  sylow3lem6  19672  lsmdisj3a  19729  lsmdisj3b  19730  pj1val  19735  pj1eq  19740  efgredlemd  19784  efgredlem  19787  efgred  19788  efgrelexlema  19789  frgpup3  19818  ablsubadd  19849  ablsubsub23  19864  iscyggen  19920  cyggenod  19924  gsumval3lem2  19946  gsumval3  19947  gsummptnn0fz  20026  dmdprd  20040  dprddisj  20051  dprdfeq0  20064  dprdf11  20065  dmdprdpr  20091  dpjeq  20101  ablfacrp  20108  pgpfac1lem2  20117  pgpfac1lem3  20119  pgpfac1lem5  20121  pgpfac1  20122  pgpfaclem1  20123  pgpfaclem2  20124  pgpfaclem3  20125  ablfaclem2  20128  ablfaclem3  20129  ablfac2  20131  rngmneg1  20213  rngmneg2  20214  rng1zrlem  20227  ringurd  20235  srgrz  20257  srglz  20258  srgisid  20259  ringid  20324  qusring2  20383  opprring  20396  dvdsrval  20410  dvdsrmul  20413  dvdsr01  20420  dvdsr02  20421  crngunit  20427  ringunitnzdiv  20447  dvreq1  20460  dvdsrpropd  20465  irredn0  20472  irredrmul  20476  irredmul  20478  rngisomring  20516  rhmdvdsr  20558  lringuplu  20594  subrg1  20632  subrgdvds  20636  isrrg  20748  rrgeq0i  20749  rrgeq0  20750  domneq0  20758  isdomn4  20766  domnlcanb  20770  domnrcanb  20772  drngid2  20802  drngmul0orOLD  20811  isdrngd  20815  isdrngdOLD  20817  fidomndrnglem  20822  isabv  20860  issrngd  20904  islmod  20931  islmodd  20933  lmodprop2d  20991  mptscmfsupp0  20994  lss1d  21030  lspextmo  21123  lvecvs0or  21178  lvecvscan  21181  lvecvscan2  21182  lbsacsbs  21226  rngqiprngimf1lem  21364  rng2idl1cntr  21375  prmirredlem  21524  pzriprnglem7  21539  pzriprnglem13  21545  chrdvds  21578  chrnzr  21582  domnchr  21584  znval  21587  zncyg  21600  znfld  21612  znunit  21615  znrrg  21617  frgpcyg  21625  psgndiflemB  21652  psgndiflemA  21653  ipeq0  21690  ip2eq  21705  elocv  21720  ocvi  21721  obsne0  21777  dsmmacl  21793  dsmmlss  21796  frlmphl  21833  frlmup4  21853  islindf4  21890  islindf5  21891  mplsubrglem  22055  mplmon2  22114  evlslem1  22135  evlseu  22136  evlsval  22139  evlsval2  22140  evlsval3  22142  ismhp3  22207  mhpsclcl  22212  mhpvarcl  22213  mhpmulcl  22214  psdmul  22231  psdmvr  22234  cply1coe0bi  22365  gsummoncoe1  22371  evl1vsd  22407  dmatel  22553  dmatelnd  22556  dmatmulcl  22560  scmateALT  22572  mdetdiaglem  22658  mdetunilem1  22672  mdetunilem3  22674  mdetunilem4  22675  mdetunilem9  22680  symgmatr01lem  22713  symgmatr01  22714  gsummatr01lem1  22715  gsummatr01lem4  22718  gsummatr01  22719  smadiadetlem3  22728  cramerlem3  22749  pmatcoe1fsupp  22761  cpmatel  22771  1elcpmat  22775  cpmatmcllem  22778  cpmatmcl  22779  d1mat2pmat  22799  m2cpminvid2lem  22814  m2cpminvid2  22815  decpmatmulsumfsupp  22833  pmatcollpw2lem  22837  pmatcollpwscmatlem1  22849  mp2pm2mplem4  22869  pm2mpmhmlem1  22878  chpscmat  22902  cpmidpmatlem3  22932  cayleyhamilton0  22949  cayleyhamiltonALT  22951  cayleyhamilton1  22952  0ntr  23131  ntreq0  23137  cldlp  23210  pnrmopn  23403  hausnei2  23413  cnhaus  23414  nrmsep  23417  isnrm2  23418  regsep2  23436  dishaus  23442  ordthauslem  23443  iscmp  23448  cmpsublem  23459  cmpsub  23460  tgcmp  23461  sscmp  23465  hauscmplem  23466  cmpfi  23468  bwth  23470  connsuba  23480  nconnsubb  23483  isref  23569  islocfin  23577  elpt  23632  elptr  23633  pthaus  23698  txcmp  23703  hausdiag  23705  txhaus  23707  txkgen  23712  xkohaus  23713  xkococnlem  23719  regr1lem  23799  fbasrn  23944  fmfnfmlem3  24016  flimtopon  24030  fclstopon  24072  alexsubb  24106  symgtgp  24166  qustgpopn  24180  qustgphaus  24183  ustuqtop  24306  isusp  24321  ispsmet  24364  psmet0  24368  ismet  24383  isxmet  24384  xmeteq0  24398  metn0  24420  xmetres2  24421  imasf1oxmet  24435  xblss2ps  24461  xblss2  24462  xmseq0  24524  comet  24573  stdbdxmet  24575  methaus  24580  dscmet  24632  nrmmetd  24634  nmeq0  24678  tngngp  24714  tngngp3  24716  nlmmul0or  24743  cnmet  24831  xrsxmet  24870  metnrmlem3  24922  icopnfcnv  25004  iccpnfcnv  25006  ishtpy  25034  isphtpy  25043  phtpyi  25046  om1elbas  25094  elpi1i  25108  pi1grplem  25111  isclmp  25159  cphsqrtcl2  25248  tcphcph  25299  bcth3  25393  rrxcph  25454  rrxmet  25470  ivth2  25517  iundisj2  25611  dyaddisj  25658  volivth  25669  mbfinf  25727  i1f1lem  25751  i1fmullem  25756  i1fmulclem  25764  i1fres  25767  itg1climres  25776  mbfi1fseqlem4  25780  dvnres  25993  dvcobr  26008  rolle  26052  cmvth  26053  deg1leb  26155  ismon1p  26203  q1peqb  26216  dvdsr1p  26224  ply1remlem  26225  fta1glem2  26229  idomrootle  26233  elply2  26256  ne0p  26267  coeeu  26285  coelem  26286  coeeq  26287  dgrle  26303  coeaddlem  26309  plymul0or  26342  ofmulrt  26343  plydivlem3  26359  plydivlem4  26360  plydivex  26361  plydiveu  26362  plydivalg  26363  quotlem  26364  plyremlem  26368  quotcan  26373  plyexmo  26377  elqaalem3  26385  qaa  26387  iaa  26389  aareccl  26390  aacjcl  26391  aannenlem2  26393  reeff1o  26510  sineq0  26589  coseq1  26590  efeq1  26593  recosf1o  26600  logeftb  26648  cosarg0d  26674  logtayl  26725  cxpval  26729  cxpeq0  26743  root1eq1  26820  cxpeq  26822  logbgcd1irr  26859  angrtmuld  26873  affineequiv  26888  affineequiv3  26890  angpieqvdlem2  26894  quad2  26904  dcubic1lem  26908  dcubic2  26909  dcubic  26911  mcubic  26912  cubic2  26913  dquartlem1  26916  dquart  26918  quart  26926  atandm2  26942  atandm4  26944  atantan  26988  wilthlem2  27133  wilthlem3  27134  muval2  27198  isnsqf  27199  mumullem2  27244  sqff1o  27246  muinv  27257  mpodvdsmulf1o  27258  dvdsmulf1o  27260  dchrelbas2  27301  dchrmullid  27316  dchrfi  27319  lgsval  27365  lgsdir  27396  lgsne0  27399  lgsprme0  27403  lgsdirnn0  27408  lgsqrlem1  27410  lgsqr  27415  gausslemma2dlem0c  27422  gausslemma2dlem0i  27428  gausslemma2dlem7  27437  gausslemma2d  27438  lgseisenlem2  27440  lgsquadlem1  27444  lgsquadlem2  27445  lgsquad2lem2  27449  lgsquad3  27451  m1lgs  27452  2lgs  27471  2sqlem7  27488  2sqlem8  27490  2sqlem9  27491  2sqlem11  27493  2sq  27494  2sq2  27497  2sqmo  27501  addsq2reu  27504  addsqn2reu  27505  addsqrexnreu  27506  addsqnreup  27507  addsq2nreurex  27508  2sqreulem1  27510  2sqreultlem  27511  2sqreunnlem1  27513  2sqreunnltlem  27514  2sqreulem4  27518  2sqreuop  27526  2sqreuopnn  27527  2sqreuoplt  27528  2sqreuopltb  27529  2sqreuopnnlt  27530  2sqreuopnnltb  27531  2sqreuopb  27532  dchrisumlem1  27553  dchrvmaeq0  27568  dchrisum0re  27577  ostth3  27702  ltsval  27711  nosepssdm  27750  nosupprefixmo  27764  noinfprefixmo  27765  nosupcbv  27766  nosupdm  27768  nosupfv  27770  nosupres  27771  nosupbnd1lem1  27772  nosupbnd1lem3  27774  nosupbnd1lem5  27776  noinfcbv  27781  noinfdm  27783  noinffv  27785  noinfres  27786  noinfbnd1lem3  27789  noinfbnd1lem5  27791  eqcuts  27878  cutbdaylt  27891  made0  27956  madecut  27976  negsid  28134  negsex  28136  subadds  28163  divsmo  28277  muls0ord  28278  divsval  28282  norecdiv  28283  recsne0  28285  divmulsw  28286  divs1  28297  precsexlem8  28307  precsexlem9  28308  precsexlem11  28310  precsex  28311  recsex  28312  abssor  28339  elons  28346  noseqrdgfn  28399  bdayn0sf1o  28463  eucliddivs  28469  zsoring  28502  n0seo  28514  zseo  28515  nohalf  28517  expsne0  28529  pw2recs  28531  halfcut  28551  z12negscl  28571  z12zsodd  28575  z12sge0  28576  renegscl  28591  istrkg3ld  28630  axtgcgrid  28632  axtgsegcon  28633  axtg5seg  28634  axtgupdim2  28640  tgjustc1  28644  tgjustc2  28645  iscgrg  28681  isismt  28703  legov  28754  legov2  28755  hlcgreu  28787  mirreu3  28827  mircgr  28830  mirbtwn  28831  ismir  28832  mireq  28838  ismidb  28951  lmiopp  28975  lnssplng  28999  dfcgra2  29024  inaghl  29039  brprlng  29065  prlngsym  29068  f1otrg  29071  ttgval  29075  ttgelitv  29083  brbtwn  29100  brcgr  29101  colinearalglem2  29108  colinearalg  29111  axsegconlem1  29118  axsegcon  29128  ax5seglem4  29133  ax5seglem5  29134  axpaschlem  29141  axpasch  29142  axlowdimlem16  29158  axeuclidlem  29163  axeuclid  29164  axcontlem2  29166  axcontlem4  29168  axcontlem5  29169  edglnl  29344  usgredg2ALT  29394  usgredgprvALT  29396  usgrnloopvALT  29402  ushgredgedgloop  29432  edg0usgr  29454  nb3grpr  29583  cplgr1v  29631  cusgrsize  29655  vtxdgfval  29668  vtxdeqd  29678  vtxdun  29682  vtxd0nedgb  29689  vtxdusgr0edgnelALT  29697  1loopgrvd2  29704  usgruvtxvdb  29730  usgrvd0nedg  29734  vtxdginducedm1  29744  rusgrpropedg  29785  wksfval  29810  wlklenvclwlk  29854  iswlkon  29856  ispth  29921  dfpth2  29929  upgrwlkdvdelem  29936  crctcshwlkn0lem6  30015  wwlknon  30057  wwlksm1edg  30081  wwlksnextbi  30094  wwlksnextfun  30098  wwlksnextinj  30099  wwlksnextsurj  30100  wwlksnextbij  30102  wlksnwwlknvbij  30108  wwlksnextproplem3  30111  wwlksnextprop  30112  wspn0  30124  umgr2adedgwlkonALT  30147  umgr2adedgspth  30148  umgr2wlkon  30150  rusgrnumwwlkslem  30172  rusgrnumwwlkb0  30174  rusgrnumwwlks  30177  clwlkclwwlklem2a4  30199  clwlknf1oclwwlknlem2  30284  clwlknf1oclwwlkn  30286  isclwwlknon  30293  clwwlknon1loop  30300  s2elclwwlknon2  30306  clwwlknonwwlknonb  30308  clwwlkvbij  30315  uhgr3cyclex  30384  fusgreg2wsplem  30535  fusgr2wsp2nb  30536  fusgreghash2wsp  30540  frrusgrord0  30542  2clwwlkel  30551  extwwlkfab  30554  extwwlkfabel  30555  clwwlknonclwlknonf1o  30564  dlwwlknondlwlknonf1o  30567  wlkl0  30569  numclwwlk2lem1  30578  numclwlk2lem2f  30579  numclwlk2lem2f1o  30581  numclwwlk5  30590  ex-opab  30634  isgrpo  30700  isgrpoi  30701  grpoidinvlem3  30709  grpoideu  30712  gidval  30715  grpoidinv2  30718  grpoinveu  30722  grpoinvval  30726  grpoinv  30728  vciOLD  30764  isvclem  30780  cnidOLD  30785  isnvlem  30813  nvmul0or  30853  imsmetlem  30893  diporthcom  30919  ipz  30922  nmlno0  30998  ajfval  31012  hmoval  31013  isphg  31020  isph  31025  ip2eqi  31059  ajval  31064  hvmul0or  31228  hvsubeq0  31271  hvaddeq0  31272  hvaddcan  31273  hvmulcan  31275  hvmulcan2  31276  hvsubadd  31280  his6  31302  hial0  31305  hial02  31306  hi2eq  31308  orthcom  31311  normlem7tALT  31322  normsub0  31339  normpyth  31348  hilid  31364  hhssnv  31467  ocel  31484  ocsh  31486  ocorth  31494  ocin  31499  occllem  31506  choc0  31529  pjpreeq  31601  omlsi  31607  pjoc1  31637  pjoml  31639  pjoc2  31642  chm0  31694  chocin  31698  chlejb1  31715  chlejb2  31716  chjo  31718  h1deoi  31752  h1de2i  31756  pjoml6i  31792  pjoml2  31814  pjoml3  31815  pjch  31897  hodsi  31978  hodid  31995  eigorth  32041  elunop  32075  adjeu  32092  adjval  32093  eigvecval  32099  unopf1o  32119  adj1  32136  adjeq  32138  hmdmadj  32143  lnopeq0i  32210  lnopeqi  32211  lnopeq  32212  lnfn0  32250  riesz4i  32266  riesz4  32267  riesz1  32268  cnlnadjlem3  32272  cnlnadjlem5  32274  cnlnadjeu  32281  cnlnssadj  32283  nmopadjlei  32291  opsqrlem1  32343  hmopidmpji  32355  pjimai  32379  isst  32416  ishst  32417  hstel2  32422  stadd3i  32451  stri  32460  largei  32470  golem2  32475  superpos  32557  sumdmdii  32618  mddmdin0i  32634  opreu2reuALT  32676  difeq  32717  elim2if  32743  disji2f  32777  disjif2  32781  disjxpin  32788  iundisj2f  32790  disjunsn  32794  fmptco1f1o  32835  ofpreima  32867  fnpreimac  32872  ressupprn  32892  curry2ima  32911  preiman0  32912  receqid  32946  xrofsup  32969  iundisj2fi  32999  f1ocnt  33002  fzo0opth  33005  elq2  33014  fprodex01  33027  prodindf  33040  xdivval  33096  xrecex  33097  xreceu  33099  xdivmul  33102  rexdiv  33103  wrdt2ind  33131  mndlrinvb  33203  mndlactfo  33205  mndractfo  33207  mndlactf1o  33208  mndractf1o  33209  gsummpt2d  33229  gsumwun  33256  fzo0pmtrlast  33272  cyc3genpm  33332  cycpmconjslem2  33335  fxpval  33345  fxpgaeq  33349  cntrval2  33351  isslmd  33382  slmdlema  33383  urpropd  33411  isunitc  33422  elrgspnlem4  33426  elrgspnsubrunlem2  33429  erlcl1  33441  erlcl2  33442  erldi  33443  erlbrd  33444  erler  33446  erld2  33447  rloccring  33452  rlocinvunit  33456  rlocisunit  33457  domnprodeq0  33460  domnlcanOLD  33464  isdrng4  33482  fracerl  33493  fracfld  33495  resv1r  33525  islinds5  33553  linds2eq  33567  dvdsruassoi  33570  dvdsruasso  33571  dvdsruasso2  33572  quslsm  33591  rhmimaidl  33618  qsidomlem2  33640  ssdifidllem  33643  ssdifidl  33644  ssdifidlprm  33645  opprqus0g  33678  qsdrngilem  33682  unitmulrprm  33724  1arithidom  33733  1arithufdlem3  33742  1arithufdlem4  33743  ply1dg1rt  33776  r1pid2OLD  33805  extvfvv  33831  extvfvcl  33833  evlextv  33839  esplysply  33868  esplyind  33872  lbsdiflsp0  33923  fedgmullem1  33926  fedgmullem2  33927  irngss  33984  irngnzply1lem  33987  extdgfialglem2  33990  ply1annidllem  33998  ply1annnr  34000  minplymindeg  34005  minplyann  34006  minplyirredlem  34007  minplyirred  34008  irngnminplynz  34009  minplyelirng  34012  irredminply  34013  algextdeglem6  34019  algextdeglem7  34020  rtelextdg2lem  34023  fldext2chn  34025  constrsuc  34035  constrsslem  34038  constrconj  34042  constrextdg2lem  34045  constrextdg2  34046  constrlccllem  34050  constrcccllem  34051  constrcbvlem  34052  constrext2chn  34056  constrcon  34071  1smat1  34101  iscref  34141  metidval  34187  metidv  34189  metider  34191  pstmxmet  34194  xrmulc1cn  34227  esumfsup  34367  esumpcvgval  34375  esumcvg  34383  inelsros  34475  diffiunisros  34476  ismeas  34496  isrnmeas  34497  brae  34538  braew  34539  dya2iocuni  34580  elcarsg  34602  eulerpartleme  34660  eulerpartlemv  34661  eulerpartlemb  34665  eulerpartgbij  34669  eulerpartlemr  34671  eulerpartlemgvv  34673  eulerpartlemgh  34675  eulerpartlemn  34678  elprob  34706  ballotlemi  34798  ballotlemi1  34800  ballotlemii  34801  ballotlemsima  34813  ballotlemfrcn0  34827  signsw0g  34850  signswmnd  34851  signstfvc  34868  prodfzo03  34897  reprval  34904  reprsum  34907  reprsuc  34909  reprpmtf1o  34920  axtgupdim2ALTV  34962  brafs  34969  bnj125  35167  bnj154  35173  bnj526  35183  bnj609  35212  bnj893  35223  bnj1321  35322  bnj1491  35352  nummin  35389  fineqvnttrclselem2  35418  fineqvnttrclselem3  35419  fineqvnttrclse  35420  noinfepfnregs  35428  subgrwlk  35482  loop1cycl  35487  subfacp1lem3  35532  subfacp1lem5  35534  subfacp1lem6  35535  cnpconn  35580  txpconn  35582  ptpconn  35583  indispconn  35584  connpconn  35585  cvxpconn  35592  cvmscbv  35608  cvmsi  35615  cvmsval  35616  cvmsdisj  35620  cvmsss2  35624  cvmliftmo  35634  cvmliftlem14  35647  cvmliftiota  35651  cvmlift2lem12  35664  cvmlift2lem13  35665  cvmlift2  35666  cvmliftphtlem  35667  cvmlift3lem2  35670  cvmlift3lem4  35672  cvmlift3lem6  35674  cvmlift3lem7  35675  cvmlift3lem9  35677  cvmlift3  35678  snmlval  35681  satffunlem  35751  prv1n  35781  mrsub0  35866  mrsubcn  35869  ismfs  35899  sinccvglem  36022  br6  36107  brbigcup  36246  imageval  36278  funpartlem  36292  dfrdg4  36301  altopthsn  36311  brsegle  36458  rankeq1o  36521  cbviotadavw  36629  subtr  36674  opnbnd  36685  cldbnd  36686  isfne  36699  topfneec  36715  neibastop3  36722  dfttc4lem1  36888  dfttc4lem2  36889  dfttc4  36890  elttcirr  36891  cnndvlem2  36976  bj-imdirval2  37675  bj-imdirid  37678  bj-imdirco  37682  bj-inftyexpiinj  37701  bj-isrvecd  37790  bj-isrvec2  37792  bj-bary1lem1  37803  bj-bary1  37804  qdiff  37819  finxp00  37896  nlpfvineqsn  37903  pibp19  37908  pibt2  37911  unccur  38102  matunitlindflem2  38116  ptrecube  38119  poimirlem4  38123  poimirlem19  38138  poimirlem23  38142  poimirlem25  38144  poimirlem27  38146  poimirlem28  38147  poimirlem31  38150  poimirlem32  38151  broucube  38153  mblfinlem2  38157  ovoliunnfl  38161  voliunnfl  38163  volsupnfl  38164  mbfresfi  38165  itg2addnclem  38170  itg2addnclem3  38172  itg2addnc  38173  ftc2nc  38201  cover2  38214  sdclem2  38241  fdc  38244  metf1o  38254  istotbnd3  38270  0totbnd  38272  sstotbnd2  38273  equivtotbnd  38277  totbndbnd  38288  prdstotbnd  38293  heibor1  38309  rrnmet  38328  isexid  38346  ismgmOLD  38349  opidonOLD  38351  exidu1  38355  cmpidelt  38358  exidreslem  38376  exidres  38377  exidresid  38378  grpoeqdivid  38380  elghomlem1OLD  38384  grpokerinj  38392  isrngo  38396  isrngod  38397  rngoideu  38402  isgrpda  38454  isdrngo2  38457  isdrngo3  38458  isrngohom  38464  divrngidl  38527  dmnnzd  38574  dmncan1  38575  disjeccnvep  38789  disjressuc2  38910  mopre  38970  qsdisjALTV  39198  dmqseqeq1  39226  unidmqseq  39239  disjdmqseq  39407  eldisjlem19  39412  riotasvd  39580  toycom  39597  islshpsm  39604  lshpnel2N  39609  lsatfixedN  39633  islshpat  39641  lcvexchlem4  39661  l1cvpat  39678  lkr0f  39718  lkrsc  39721  lshpkrlem1  39734  lkreqN  39794  isopos  39804  oposlem  39806  opcon2b  39821  cmtbr3N  39878  cvlcvrp  39964  hlrelat5N  40025  cvrval5  40039  cvrat4  40067  3atlem5  40111  2at0mat0  40149  psubclsetN  40560  4atex2  40701  isldil  40734  ltrnu  40745  ltrnid  40759  isdilN  40778  trlnid  40803  cdleme21k  40962  cdleme29b  40999  cdlemefrs29pre00  41019  cdlemefrs29bpre0  41020  cdlemefrs29cpre1  41022  cdleme32fva  41061  cdleme42b  41102  cdleme50ex  41183  cdleme  41184  cdlemg1a  41194  ltrniotaval  41205  cdlemeiota  41209  tendoid0  41449  cdlemksv2  41471  cdlemkuv2  41491  cdlemk36  41537  cdlemk42  41565  cdlemk  41598  tendoex  41599  cdleml3N  41602  cdleml5N  41604  tendospcanN  41647  cdlemm10N  41742  dihffval  41854  dihfval  41855  dihlsscpre  41858  islpolN  42107  mapdhval  42348  mapdheq  42352  hdmap1fval  42420  hdmap1val  42422  hdmap1eq  42425  hdmap1cbv  42426  hdmapval2lem  42455  hdmap11  42472  hdmap14lem2a  42491  hdmap14lem6  42497  hgmapval  42511  hlhillcs  42582  hlhilphllem  42583  aks4d1  42706  isprimroot  42710  mndmolinv  42712  linvh  42713  primrootsunit1  42714  primrootsunit  42715  primrootscoprmpow  42716  primrootscoprbij  42719  primrootlekpowne0  42722  primrootspoweq0  42723  ringexp0nn  42751  aks6d1c5lem1  42753  sticksstones8  42770  sticksstones9  42771  sticksstones10  42772  sticksstones11  42773  sticksstones12a  42774  sticksstones12  42775  sticksstones16  42779  sticksstones17  42780  sticksstones18  42781  sticksstones19  42782  aks6d1c6lem4  42790  aks6d1c6isolem3  42793  rhmqusspan  42802  grpods  42811  unitscyglem1  42812  unitscyglem2  42813  unitscyglem3  42814  unitscyglem5  42816  expeq1d  42933  zdivgd  42946  ef11d  42948  resubval  42976  renegadd  42981  resubeu  42986  resubadd  42988  sn-remul0ord  43017  sn-negex12  43026  addinvcom  43041  redivvald  43051  rediveud  43052  redivmuld  43054  sn-mul02  43074  mulgt0con1d  43092  mulgt0con2d  43093  fimgmcyclem  43151  fidomncyc  43153  fsuppind  43172  mhphflem  43178  prjspnfv01  43206  prjspner01  43207  prjspner1  43208  prjcrvval  43214  dffltz  43216  flt4lem7  43241  nna4b4nsq  43242  negexpidd  43263  mzpcompact2lem  43332  eldioph  43339  eldioph2lem1  43341  eldioph2lem2  43342  eldioph2  43343  eldioph2b  43344  eldioph3  43347  diophin  43353  diophun  43354  eq0rabdioph  43357  dvdsrabdioph  43387  eldioph4i  43389  diophren  43390  rabren3dioph  43392  fphpd  43393  pellexlem5  43410  pellexlem6  43411  pellex  43412  pell1qrval  43423  pell14qrval  43425  pell1234qrval  43427  pell1234qrreccl  43431  pell1234qrmulcl  43432  pell1234qrdich  43438  pell14qrdich  43446  pell1qr1  43448  pellqrexplicit  43454  rmxycomplete  43494  jm2.27  43585  rmydioph  43591  rmxdiophlem  43592  rmxdioph  43593  pw2f1ocnv  43614  pwssplit4  43666  elmnc  43713  dgraalem  43722  dgraaub  43725  dgraa0p  43726  mpaaeu  43727  mpaaval  43728  mpaalem  43729  aaitgo  43739  rngunsnply  43746  proot1ex  43773  cantnfresb  43901  tfsconcatfv  43918  tfsconcatb0  43921  tfsconcat0i  43922  tfsconcat0b  43923  tfsconcat00  43924  tfsconcatrev  43925  naddwordnexlem4  43978  sqrtcval  44217  relexpnul  44254  relexpxpnnidm  44279  relexpiidm  44280  trclfvdecomr  44304  rfovcnvf1od  44580  ntrkbimka  44614  ntrk0kbimka  44615  clsk3nimkb  44616  clsk1independent  44622  ntrclsfveq1  44636  ntrclsfveq2  44637  ntrclskb  44645  k0004val  44726  k0004val0  44730  mnringmulrcld  44804  expgrowth  44911  bcc0  44916  relpfrlem  45529  permac8prim  45590  disjinfi  45770  fsumf1of  46150  limsupmnflem  46294  liminfpnfuz  46390  climxlim2lem  46419  coseq0  46438  icccncfext  46461  dvnmptconst  46515  dvnprodlem1  46520  dvnprodlem2  46521  dvnprodlem3  46522  dvnprod  46523  stoweidlem15  46589  stoweidlem31  46605  stoweidlem35  46609  stoweidlem36  46610  stoweidlem37  46611  stoweidlem43  46617  stoweidlem44  46618  stoweidlem46  46620  stoweidlem55  46629  stoweidlem59  46633  dirkerval2  46668  dirkertrigeqlem1  46672  dirkeritg  46676  dirkercncf  46681  fourierdlem2  46683  fourierdlem3  46684  fourierdlem42  46723  fourierdlem71  46751  fourierdlem112  46792  fourierdlem113  46793  elaa2lem  46807  etransclem11  46819  etransclem24  46832  etransclem26  46834  etransclem28  46836  etransclem35  46843  ioorrnopnxr  46881  salgenval  46895  intsaluni  46903  salgenn0  46905  salgencl  46906  sssalgen  46909  salgenss  46910  salgenuni  46911  issalgend  46912  dfsalgen2  46915  subsaliuncl  46932  sge0f1o  46956  sge0fodjrnlem  46990  ismea  47025  nnfoctbdjlem  47029  iundjiun  47034  isome  47068  caragenel  47069  ovn0lem  47139  ovnsubaddlem1  47144  smflimlem4  47348  smflim  47351  sigarcol  47438  chnsubseqwl  47455  nthrucw  47462  cfsetsnfsetf  47652  cfsetsnfsetfo  47654  fnbrafvb  47748  afv2fv0  47859  readdcnnred  47897  resubcnnred  47898  cndivrenred  47900  nnmul2  47924  ceilbi  47931  minusmodnep2tmod  47953  modmkpkne  47961  nndivides2  47978  fargshiftf1  48047  fargshiftfo  48048  ichexmpl2  48076  ichnreuop  48078  ichreuopeq  48079  elsprel  48081  prproropf1olem4  48112  reupr  48128  reuopreuprim  48132  goldbachthlem2  48155  fmtnoprmfac2lem1  48175  fmtnofac2lem  48177  prmdvdsfmtnof1lem2  48194  mod42tp1mod8  48211  lighneallem2  48215  lighneallem3  48216  lighneallem4  48219  proththd  48223  41prothprm  48228  requad01  48243  requad2  48245  dfeven2  48271  dfeven5  48288  dfodd7  48289  fpprel  48350  fppr2odd  48353  fpprwppr  48361  fpprwpprb  48362  nnsum3primesgbe  48414  isubgredg  48488  upgrimpths  48531  ushggricedg  48549  uhgrimisgrgric  48553  isubgr3stgrlem3  48590  isubgr3stgrlem4  48591  isubgr3stgrlem6  48593  grlimprclnbgr  48618  grlimgrtrilem2  48624  gpgedgvtx0  48683  gpgedgvtx1  48684  gpgvtxedg0  48685  gpgvtxedg1  48686  gpg3kgrtriexlem5  48709  gpgprismgr4cycllem3  48719  pgnbgreunbgrlem2lem1  48736  pgnbgreunbgrlem2lem2  48737  pgnbgreunbgrlem2lem3  48738  upwlksfval  48757  0nodd  48792  2nodd  48794  nnsgrpnmnd  48800  nn0mnd  48801  lidldomn1  48853  zlidlring  48856  uzlidlring  48857  2zrngamgm  48867  2zrngamnd  48869  2zrngagrp  48871  2zrngnmlid2  48879  ztprmneprm  48969  dmatALTbasel  49024  linindslinci  49070  lindslinindsimp1  49079  lindslinindimp2lem4  49083  lindslinindsimp2lem5  49084  linds0  49087  el0ldep  49088  lindsrng01  49090  snlindsntorlem  49092  snlindsntor  49093  ldepspr  49095  lincresunit3  49103  islindeps2  49105  isldepslvec2  49107  zlmodzxzldep  49126  blen1b  49210  dig2bits  49236  nn0sumshdiglem1  49243  0aryfvalelfv  49257  itcovalsuc  49289  prelrrx2b  49336  eenglngeehlnmlem1  49359  eenglngeehlnmlem2  49360  rrx2linest2  49366  elrrx2linest2  49367  spheres  49368  2sphere  49371  2sphere0  49372  line2ylem  49373  line2  49374  line2xlem  49375  line2x  49376  line2y  49377  itscnhlc0yqe  49381  itschlc0yqe  49382  itscnhlc0xyqsol  49387  itschlc0xyqsol1  49388  itsclc0xyqsolr  49391  itsclc0  49393  itsclc0b  49394  itsclinecirc0b  49396  itsclquadb  49398  itsclquadeu  49399  itscnhlinecirc02p  49407  resinsnALT  49494  sepnsepolem2  49544  sepnsepo  49545  sepfsepc  49549  iscnrm3rlem8  49568  iscnrm3r  49569  iscnrm3llem2  49571  iscnrm3l  49572  oppcendc  49639  isisod  49648  sectpropdlem  49657  ssccatid  49693  resccatlem  49694  imasubc  49772  uptrlem1  49831  oppcthinendcALT  50062  functhinclem2  50066  fullthinc2  50072  thincciso  50074  thinccisod  50075  termcpropd  50124  fulltermc2  50133  oduoppcciso  50187  discsnterm  50195  aacllem  50422