Theorem eqeq1d 2738

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  eqeq1  2740  eqcomd  2742  eqeq2d  2747  eqeqan12d  2750  neeq1d  2991  csbconstg  3856  csbhypf  3865  csbiebt  3866  csbiebg  3869  sbceq2g  4359  csbie2df  4383  disjeq0  4396  disjssun  4408  mosneq  4785  preq12b  4793  preq12bg  4796  elpreqprlem  4809  disji2  5069  invdisjrab  5072  disjprg  5081  disjxun  5083  iin0  5304  opthg  5430  opeqsng  5457  propeqop  5461  wefrc  5625  xpcan  6140  xpcan2  6141  dmsnopg  6177  rnmpt0f  6207  reuop  6257  dfpo2  6260  sspred  6274  onfr  6362  unisucg  6403  nsuceq0  6408  iotaeq  6466  iotabi  6467  fneq1  6589  fnun  6612  fnresdisj  6618  fnimadisj  6630  fnimaeq0  6631  foeq1  6748  fveqeq2d  6848  fvun1  6931  fvmptdv2  6966  fndmdifeq0  6996  fneqeql  6998  dffo3  7054  dffo3f  7058  fnnfpeq0  7133  foeqcnvco  7255  f1eqcocnv  7256  isofrlem  7295  eqfunresadj  7315  ovanraleqv  7391  f1opr  7423  eloprabga  7476  ovmpodv2  7525  ov3  7530  ovelimab  7545  caovcang  7568  caovcan  7571  caovmo  7604  caofinvl  7663  caofid1  7666  caofid2  7667  caofidlcan  7669  caonncan  7675  tfisi  7810  mptcnfimad  7939  oteqimp  7961  br1steqg  7964  br2ndeqg  7965  eqop  7984  reldm  7997  mposn  8053  fparlem1  8062  fparlem2  8063  fsplit  8067  frxp  8076  xporderlem  8077  fnwelem  8081  xpord2lem  8092  xpord3lem  8099  poseq  8108  soseq  8109  fnsuppeq0  8142  suppssov1  8147  suppssov2  8148  suppofss1d  8154  suppofss2d  8155  tposfo2  8199  mpocurryd  8219  iinon  8280  onnseq  8284  tz7.49  8384  seqomlem2  8390  oe0m1  8456  om0r  8474  oe1m  8480  oawordeulem  8489  oawordeu  8490  oarec  8497  omord  8503  oneo  8516  omeu  8520  oeeui  8538  nnm0r  8546  nnmord  8568  nnawordex  8573  nnaordex2  8575  nnneo  8591  nneob  8592  omopth  8598  nnasmo  8599  ereq1  8651  eqerlem  8679  qsdisj  8741  erov  8761  eceqoveq  8769  mapsnd  8834  endisj  9002  pw2f1olem  9019  enfixsn  9024  disjenex  9073  domssex2  9075  xpf1o  9077  mapxpen  9081  unxpdomlem2  9167  enp1ilem  9188  fodomfib  9239  fodomfibOLD  9241  fipreima  9268  opthreg  9539  cantnfp1lem3  9601  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  frmin  9673  updjud  9858  pm54.43  9925  dfac5  10051  dfacacn  10064  kmlem9  10081  cfeq0  10178  cfss  10187  cfslb  10188  fin23lem22  10249  fin23lem12  10253  fin23lem19  10258  fin23lem30  10264  fin23lem33  10267  fin1a2lem6  10327  axcc2lem  10358  axdc3lem2  10373  axdc3lem3  10374  axdc3lem4  10375  axdc3  10376  axdc4lem  10377  zorn2lem7  10424  ttukeylem3  10433  ttukeylem6  10436  ttukey2g  10438  fodomb  10448  axacndlem5  10534  fpwwe2cbv  10553  fpwwe2lem2  10555  fpwwe2lem3  10556  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe  10569  pwfseqlem2  10582  pwxpndom2  10588  addnidpi  10824  ltexpi  10825  recmulnq  10887  ltexnq  10898  halfnq  10899  archnq  10903  ltexpri  10966  recexpr  10974  addsrpr  10998  mulsrpr  10999  00sr  11022  negexsr  11025  recexsrlem  11026  recexsr  11030  axrnegex  11085  axrrecex  11086  00id  11321  mul02  11324  addrid  11326  cnegex  11327  cnegex2  11328  subval  11384  subadd  11396  subadd2  11397  subsub23  11398  addsubeq4  11408  subcan2  11419  negcon1  11446  subcan  11449  addrsub  11567  ltordlem  11675  ltord1  11676  recex  11782  mul0or  11790  muleqadd  11794  receu  11795  mulcan1g  11803  divval  11811  divmul  11812  rec11  11853  ldiv  11989  rdiv  11990  ind1a  12170  zdiv  12599  uzin  12824  xaddval  13175  xmulval  13177  xnn0xadd0  13199  xnegdi  13200  ioo0  13323  ico0  13344  ioc0  13345  icc0  13346  1fv  13601  fzon  13635  fvinim0ffz  13744  flbi  13775  mod0  13835  modmuladdnn0  13877  modirr  13904  addmodlteq  13908  uzrdgfni  13920  axdc4uzlem  13945  fsuppmapnn0fiubex  13954  mptnn0fsupp  13959  seqid  14009  seqz  14012  expval  14025  expeq0  14054  sqeqor  14178  nn0opth2  14234  hashdom  14341  elprchashprn2  14358  hashbc  14415  hashf1lem1  14417  hash2pwpr  14438  ccat0  14538  wrdl1s1  14577  ccatws1lenp1b  14584  pfxsuff1eqwrdeq  14661  swrdccatin2  14691  pfxccatin12lem2  14693  2cshwcshw  14787  scshwfzeqfzo  14788  cshimadifsn  14791  cshimadifsn0  14792  s2f1o  14878  wrdlen2i  14904  2swrd2eqwrdeq  14915  wwlktovf  14918  wwlktovf1  14919  wwlktovfo  14920  wrd2f1tovbij  14922  relexp0g  14984  relexpsucnnr  14987  dfrtrcl2  15024  mulre  15083  rennim  15201  cnpart  15202  01sqrex  15211  resqrex  15212  sqrmo  15213  resqrtcl  15215  resqrtthlem  15216  sqrtgt0  15220  sqrtneg  15229  sqrtsq2  15230  absmod0  15265  sqreulem  15322  sqreu  15323  sqrtthlem  15325  eqsqrtd  15330  reusq0  15427  fsum00  15761  telfsumo  15765  prodss  15912  fprodle  15961  tanaddlem  16133  absefib  16165  efieq1re  16166  divides  16223  dvdsval2  16224  nndivides  16231  dvds0lem  16235  dvds1lem  16236  dvds2lem  16237  negdvdsb  16241  muldvds1  16249  muldvds2  16250  dvdscmulr  16253  dvdsmulcr  16254  difmod0  16256  dvdstr  16263  dvdsabseq  16282  divconjdvds  16284  odd2np1lem  16309  odd2np1  16310  even2n  16311  oddm1even  16312  2tp1odd  16321  opeo  16334  omeo  16335  m1exp1  16345  divalglem4  16365  divalglem8  16369  divalgb  16373  bitsuz  16443  smupvallem  16452  gcdaddmlem  16493  gcdabs1  16498  bezoutlem3  16510  rplpwr  16527  rprpwr  16528  alginv  16544  algcvga  16548  algfx  16549  eucalgval2  16550  coprmdvds  16622  qredeq  16626  qredeu  16627  coprmprod  16630  coprmproddvdslem  16631  divgcdcoprm0  16634  divgcdcoprmex  16635  cncongr1  16636  rpexp  16692  rpexp12i  16694  cncongrprm  16699  qnumdenbi  16714  phival  16737  phicl2  16738  dfphi2  16744  phiprmpw  16746  phimullem  16749  eulerthlem1  16751  eulerthlem2  16752  eulerth  16753  fermltl  16754  hashgcdlem  16758  phisum  16761  odzval  16762  odzdvds  16766  reumodprminv  16775  modprm0  16776  nnnn0modprm0  16777  modprmn0modprm0  16778  coprimeprodsq  16779  coprimeprodsq2  16780  pythagtriplem2  16788  pythagtrip  16805  pcval  16815  pceulem  16816  pcqmul  16824  pcqcl  16827  pcabs  16846  pcgcd1  16848  pc2dvds  16850  pcaddlem  16859  pcadd  16860  pcmpt  16863  prmpwdvds  16875  pockthi  16878  unbenlem  16879  4sqlem12  16927  ramz  16996  ramcl  17000  cshwrepswhash1  17073  imasval  17475  fvprif  17525  iscat  17638  iscatd  17639  catidex  17640  catideu  17641  cidfval  17642  cidval  17643  catidd  17646  catlid  17649  catrid  17650  catpropd  17675  cidpropd  17676  issect  17720  dfiso2  17739  invcoisoid  17759  isocoinvid  17760  setcepi  18055  latleeqj2  18418  latleeqm2  18434  oduclatb  18473  mgmidmo  18628  grpidval  18629  grpidpropd  18630  ismgmid  18633  ismgmid2  18636  mgmidsssn0  18640  grpinvalem  18641  grprida  18643  gsumvalx  18644  gsumpropd  18646  gsumpropd2lem  18647  gsumress  18650  gsumval2  18654  ismnddef  18704  sgrpidmnd  18707  ismndd  18724  mndpropd  18727  mndinvmod  18732  mnd1  18747  ismhm  18753  gsumvallem2  18802  frmdgsum  18830  frmdup3  18835  efmndmnd  18857  smndex1mnd  18881  sgrp2rid2  18897  sgrp2rid2ex  18898  pwmnd  18908  grpinvex  18919  isgrpd2  18932  isgrpd  18934  dfgrp2  18938  grpinveu  18950  grpinvval  18956  grplinv  18965  isgrpinv  18969  grplrinv  18972  grpidinv2  18973  grpidinv  18974  grplmulf1o  18989  grpraddf1o  18990  grpsubeq0  19002  grpsubadd  19004  dfgrp3lem  19014  dfgrp3  19015  grp1  19023  imasgrp2  19031  qusgrp2  19034  mhmmnd  19040  ghmgrp  19042  mulgval  19047  mulgaddcom  19074  eqg0el  19158  cycsubmel  19175  ghmeqker  19218  ghmf1  19221  conjnmzb  19228  ghmqusker  19262  isga  19266  subgga  19275  gaorb  19282  gaorber  19283  gastacl  19284  gastacos  19285  orbsta  19288  symgfix2  19391  gsmsymgrfixlem1  19402  gsmsymgrfix  19403  gsmsymgreq  19407  symgfixelq  19408  f1omvdconj  19421  pmtrdifwrdel2  19461  psgnunilem1  19468  psgnunilem2  19470  psgnunilem3  19471  psgnunilem4  19472  odval  19509  odid  19513  odlem2  19514  oddvdsnn0  19519  odnncl  19520  oddvds  19522  odcong  19524  odeq  19525  odmulgid  19529  odmulgeq  19532  gexval  19553  gexid  19556  gexlem2  19557  gexdvdsi  19558  gexdvds  19559  subgpgp  19572  sylow1lem1  19573  sylow1lem4  19576  sylow2alem1  19592  sylow2alem2  19593  sylow2blem2  19596  sylow3lem6  19607  lsmdisj3a  19664  lsmdisj3b  19665  pj1val  19670  pj1eq  19675  efgredlemd  19719  efgredlem  19722  efgred  19723  efgrelexlema  19724  frgpup3  19753  ablsubadd  19784  ablsubsub23  19799  iscyggen  19855  cyggenod  19859  gsumval3lem2  19881  gsumval3  19882  gsummptnn0fz  19961  dmdprd  19975  dprddisj  19986  dprdfeq0  19999  dprdf11  20000  dmdprdpr  20026  dpjeq  20036  ablfacrp  20043  pgpfac1lem2  20052  pgpfac1lem3  20054  pgpfac1lem5  20056  pgpfac1  20057  pgpfaclem1  20058  pgpfaclem2  20059  pgpfaclem3  20060  ablfaclem2  20063  ablfaclem3  20064  ablfac2  20066  rngmneg1  20148  rngmneg2  20149  ringurd  20166  srgrz  20188  srglz  20189  srgisid  20190  srg1zr  20196  ringid  20255  qusring2  20314  opprring  20327  dvdsrval  20341  dvdsrmul  20344  dvdsr01  20351  dvdsr02  20352  crngunit  20358  ringunitnzdiv  20378  dvreq1  20391  dvdsrpropd  20396  irredn0  20403  irredrmul  20407  irredmul  20409  rngisomring  20447  rhmdvdsr  20485  lringuplu  20521  subrg1  20559  subrgdvds  20563  isrrg  20675  rrgeq0i  20676  rrgeq0  20677  domneq0  20685  isdomn4  20693  domnlcanb  20697  domnrcanb  20699  drngid2  20729  drngmul0orOLD  20738  isdrngd  20742  isdrngdOLD  20744  fidomndrnglem  20749  isabv  20788  issrngd  20832  islmod  20859  islmodd  20861  lmodprop2d  20919  mptscmfsupp0  20922  lss1d  20958  lspextmo  21051  lvecvs0or  21106  lvecvscan  21109  lvecvscan2  21110  lbsacsbs  21154  rngqiprngimf1lem  21292  rng2idl1cntr  21303  prmirredlem  21452  pzriprnglem7  21467  pzriprnglem13  21473  chrdvds  21506  chrnzr  21510  domnchr  21512  znval  21515  zncyg  21528  znfld  21540  znunit  21543  znrrg  21545  frgpcyg  21553  psgndiflemB  21580  psgndiflemA  21581  ipeq0  21618  ip2eq  21633  elocv  21648  ocvi  21649  obsne0  21705  dsmmacl  21721  dsmmlss  21724  frlmphl  21761  frlmup4  21781  islindf4  21818  islindf5  21819  mplsubrglem  21982  mplmon2  22039  evlslem1  22060  evlseu  22061  evlsval  22064  evlsval2  22065  evlsval3  22067  ismhp3  22108  mhpsclcl  22113  mhpvarcl  22114  mhpmulcl  22115  psdmul  22132  psdmvr  22135  cply1coe0bi  22267  gsummoncoe1  22273  evl1vsd  22309  dmatel  22458  dmatelnd  22461  dmatmulcl  22465  scmateALT  22477  mdetdiaglem  22563  mdetunilem1  22577  mdetunilem3  22579  mdetunilem4  22580  mdetunilem9  22585  symgmatr01lem  22618  symgmatr01  22619  gsummatr01lem1  22620  gsummatr01lem4  22623  gsummatr01  22624  smadiadetlem3  22633  cramerlem3  22654  pmatcoe1fsupp  22666  cpmatel  22676  1elcpmat  22680  cpmatmcllem  22683  cpmatmcl  22684  d1mat2pmat  22704  m2cpminvid2lem  22719  m2cpminvid2  22720  decpmatmulsumfsupp  22738  pmatcollpw2lem  22742  pmatcollpwscmatlem1  22754  mp2pm2mplem4  22774  pm2mpmhmlem1  22783  chpscmat  22807  cpmidpmatlem3  22837  cayleyhamilton0  22854  cayleyhamiltonALT  22856  cayleyhamilton1  22857  0ntr  23036  ntreq0  23042  cldlp  23115  pnrmopn  23308  hausnei2  23318  cnhaus  23319  nrmsep  23322  isnrm2  23323  regsep2  23341  dishaus  23347  ordthauslem  23348  iscmp  23353  cmpsublem  23364  cmpsub  23365  tgcmp  23366  sscmp  23370  hauscmplem  23371  cmpfi  23373  bwth  23375  connsuba  23385  nconnsubb  23388  isref  23474  islocfin  23482  elpt  23537  elptr  23538  pthaus  23603  txcmp  23608  hausdiag  23610  txhaus  23612  txkgen  23617  xkohaus  23618  xkococnlem  23624  regr1lem  23704  fbasrn  23849  fmfnfmlem3  23921  flimtopon  23935  fclstopon  23977  alexsubb  24011  symgtgp  24071  qustgpopn  24085  qustgphaus  24088  ustuqtop  24211  isusp  24226  ispsmet  24269  psmet0  24273  ismet  24288  isxmet  24289  xmeteq0  24303  metn0  24325  xmetres2  24326  imasf1oxmet  24340  xblss2ps  24366  xblss2  24367  xmseq0  24429  comet  24478  stdbdxmet  24480  methaus  24485  dscmet  24537  nrmmetd  24539  nmeq0  24583  tngngp  24619  tngngp3  24621  nlmmul0or  24648  cnmet  24736  xrsxmet  24775  metnrmlem3  24827  icopnfcnv  24909  iccpnfcnv  24911  ishtpy  24939  isphtpy  24948  phtpyi  24951  om1elbas  24999  elpi1i  25013  pi1grplem  25016  isclmp  25064  cphsqrtcl2  25153  tcphcph  25204  bcth3  25298  rrxcph  25359  rrxmet  25375  ivth2  25422  iundisj2  25516  dyaddisj  25563  volivth  25574  mbfinf  25632  i1f1lem  25656  i1fmullem  25661  i1fmulclem  25669  i1fres  25672  itg1climres  25681  mbfi1fseqlem4  25685  dvnres  25898  dvcobr  25913  rolle  25957  cmvth  25958  deg1leb  26060  ismon1p  26108  q1peqb  26121  dvdsr1p  26129  ply1remlem  26130  fta1glem2  26134  idomrootle  26138  elply2  26161  ne0p  26172  coeeu  26190  coelem  26191  coeeq  26192  dgrle  26208  coeaddlem  26214  plymul0or  26247  ofmulrt  26248  plydivlem3  26261  plydivlem4  26262  plydivex  26263  plydiveu  26264  plydivalg  26265  quotlem  26266  plyremlem  26270  quotcan  26275  plyexmo  26279  elqaalem3  26287  qaa  26289  iaa  26291  aareccl  26292  aacjcl  26293  aannenlem2  26295  reeff1o  26412  sineq0  26488  coseq1  26489  efeq1  26492  recosf1o  26499  logeftb  26547  cosarg0d  26573  logtayl  26624  cxpval  26628  cxpeq0  26642  root1eq1  26719  cxpeq  26721  logbgcd1irr  26758  angrtmuld  26772  affineequiv  26787  affineequiv3  26789  angpieqvdlem2  26793  quad2  26803  dcubic1lem  26807  dcubic2  26808  dcubic  26810  mcubic  26811  cubic2  26812  dquartlem1  26815  dquart  26817  quart  26825  atandm2  26841  atandm4  26843  atantan  26887  wilthlem2  27032  wilthlem3  27033  muval2  27097  isnsqf  27098  mumullem2  27143  sqff1o  27145  muinv  27156  mpodvdsmulf1o  27157  dvdsmulf1o  27159  dchrelbas2  27200  dchrmullid  27215  dchrfi  27218  lgsval  27264  lgsdir  27295  lgsne0  27298  lgsprme0  27302  lgsdirnn0  27307  lgsqrlem1  27309  lgsqr  27314  gausslemma2dlem0c  27321  gausslemma2dlem0i  27327  gausslemma2dlem7  27336  gausslemma2d  27337  lgseisenlem2  27339  lgsquadlem1  27343  lgsquadlem2  27344  lgsquad2lem2  27348  lgsquad3  27350  m1lgs  27351  2lgs  27370  2sqlem7  27387  2sqlem8  27389  2sqlem9  27390  2sqlem11  27392  2sq  27393  2sq2  27396  2sqmo  27400  addsq2reu  27403  addsqn2reu  27404  addsqrexnreu  27405  addsqnreup  27406  addsq2nreurex  27407  2sqreulem1  27409  2sqreultlem  27410  2sqreunnlem1  27412  2sqreunnltlem  27413  2sqreulem4  27417  2sqreuop  27425  2sqreuopnn  27426  2sqreuoplt  27427  2sqreuopltb  27428  2sqreuopnnlt  27429  2sqreuopnnltb  27430  2sqreuopb  27431  dchrisumlem1  27452  dchrvmaeq0  27467  dchrisum0re  27476  ostth3  27601  ltsval  27611  nosepssdm  27650  nosupprefixmo  27664  noinfprefixmo  27665  nosupcbv  27666  nosupdm  27668  nosupfv  27670  nosupres  27671  nosupbnd1lem1  27672  nosupbnd1lem3  27674  nosupbnd1lem5  27676  noinfcbv  27681  noinfdm  27683  noinffv  27685  noinfres  27686  noinfbnd1lem3  27689  noinfbnd1lem5  27691  eqcuts  27777  cutbdaylt  27790  made0  27855  madecut  27875  negsid  28033  negsex  28035  subadds  28062  divsmo  28176  muls0ord  28177  divsval  28181  norecdiv  28182  recsne0  28184  divmulsw  28185  divs1  28196  precsexlem8  28206  precsexlem9  28207  precsexlem11  28209  precsex  28210  recsex  28211  abssor  28238  elons  28245  noseqrdgfn  28298  bdayn0sf1o  28362  eucliddivs  28368  zsoring  28401  n0seo  28413  zseo  28414  nohalf  28416  expsne0  28428  pw2recs  28430  halfcut  28450  z12negscl  28470  z12zsodd  28474  z12sge0  28475  renegscl  28490  istrkg3ld  28529  axtgcgrid  28531  axtgsegcon  28532  axtg5seg  28533  axtgupdim2  28539  tgjustc1  28543  tgjustc2  28544  iscgrg  28580  isismt  28602  legov  28653  legov2  28654  hlcgreu  28686  mirreu3  28722  mircgr  28725  mirbtwn  28726  ismir  28727  mireq  28733  ismidb  28846  lmiopp  28870  dfcgra2  28898  inaghl  28913  f1otrg  28939  ttgval  28943  ttgelitv  28951  brbtwn  28968  brcgr  28969  colinearalglem2  28976  colinearalg  28979  axsegconlem1  28986  axsegcon  28996  ax5seglem4  29001  ax5seglem5  29002  axpaschlem  29009  axpasch  29010  axlowdimlem16  29026  axeuclidlem  29031  axeuclid  29032  axcontlem2  29034  axcontlem4  29036  axcontlem5  29037  edglnl  29212  usgredg2ALT  29262  usgredgprvALT  29264  usgrnloopvALT  29270  ushgredgedgloop  29300  edg0usgr  29322  nb3grpr  29451  cplgr1v  29499  cusgrsize  29523  vtxdgfval  29536  vtxdeqd  29546  vtxdun  29550  vtxd0nedgb  29557  vtxdusgr0edgnelALT  29565  1loopgrvd2  29572  usgruvtxvdb  29598  usgrvd0nedg  29602  vtxdginducedm1  29612  rusgrpropedg  29653  wksfval  29678  wlklenvclwlk  29722  iswlkon  29724  ispth  29789  dfpth2  29797  upgrwlkdvdelem  29804  crctcshwlkn0lem6  29883  wwlknon  29925  wwlksm1edg  29949  wwlksnextbi  29962  wwlksnextfun  29966  wwlksnextinj  29967  wwlksnextsurj  29968  wwlksnextbij  29970  wlksnwwlknvbij  29976  wwlksnextproplem3  29979  wwlksnextprop  29980  wspn0  29992  umgr2adedgwlkonALT  30015  umgr2adedgspth  30016  umgr2wlkon  30018  rusgrnumwwlkslem  30040  rusgrnumwwlkb0  30042  rusgrnumwwlks  30045  clwlkclwwlklem2a4  30067  clwlknf1oclwwlknlem2  30152  clwlknf1oclwwlkn  30154  isclwwlknon  30161  clwwlknon1loop  30168  s2elclwwlknon2  30174  clwwlknonwwlknonb  30176  clwwlkvbij  30183  uhgr3cyclex  30252  fusgreg2wsplem  30403  fusgr2wsp2nb  30404  fusgreghash2wsp  30408  frrusgrord0  30410  2clwwlkel  30419  extwwlkfab  30422  extwwlkfabel  30423  clwwlknonclwlknonf1o  30432  dlwwlknondlwlknonf1o  30435  wlkl0  30437  numclwwlk2lem1  30446  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  numclwwlk5  30458  ex-opab  30502  isgrpo  30568  isgrpoi  30569  grpoidinvlem3  30577  grpoideu  30580  gidval  30583  grpoidinv2  30586  grpoinveu  30590  grpoinvval  30594  grpoinv  30596  vciOLD  30632  isvclem  30648  cnidOLD  30653  isnvlem  30681  nvmul0or  30721  imsmetlem  30761  diporthcom  30787  ipz  30790  nmlno0  30866  ajfval  30880  hmoval  30881  isphg  30888  isph  30893  ip2eqi  30927  ajval  30932  hvmul0or  31096  hvsubeq0  31139  hvaddeq0  31140  hvaddcan  31141  hvmulcan  31143  hvmulcan2  31144  hvsubadd  31148  his6  31170  hial0  31173  hial02  31174  hi2eq  31176  orthcom  31179  normlem7tALT  31190  normsub0  31207  normpyth  31216  hilid  31232  hhssnv  31335  ocel  31352  ocsh  31354  ocorth  31362  ocin  31367  occllem  31374  choc0  31397  pjpreeq  31469  omlsi  31475  pjoc1  31505  pjoml  31507  pjoc2  31510  chm0  31562  chocin  31566  chlejb1  31583  chlejb2  31584  chjo  31586  h1deoi  31620  h1de2i  31624  pjoml6i  31660  pjoml2  31682  pjoml3  31683  pjch  31765  hodsi  31846  hodid  31863  eigorth  31909  elunop  31943  adjeu  31960  adjval  31961  eigvecval  31967  unopf1o  31987  adj1  32004  adjeq  32006  hmdmadj  32011  lnopeq0i  32078  lnopeqi  32079  lnopeq  32080  lnfn0  32118  riesz4i  32134  riesz4  32135  riesz1  32136  cnlnadjlem3  32140  cnlnadjlem5  32142  cnlnadjeu  32149  cnlnssadj  32151  nmopadjlei  32159  opsqrlem1  32211  hmopidmpji  32223  pjimai  32247  isst  32284  ishst  32285  hstel2  32290  stadd3i  32319  stri  32328  largei  32338  golem2  32343  superpos  32425  sumdmdii  32486  mddmdin0i  32502  opreu2reuALT  32546  difeq  32588  elim2if  32614  disji2f  32647  disjif2  32651  disjxpin  32658  iundisj2f  32660  disjunsn  32664  fmptco1f1o  32706  ofpreima  32738  fnpreimac  32743  ressupprn  32763  curry2ima  32782  preiman0  32783  receqid  32817  xrofsup  32840  iundisj2fi  32870  f1ocnt  32873  fzo0opth  32876  elq2  32885  fprodex01  32898  sgn0bi  32913  prodindf  32922  xdivval  32978  xrecex  32979  xreceu  32981  xdivmul  32984  rexdiv  32985  wrdt2ind  33013  mndlrinvb  33085  mndlactfo  33087  mndractfo  33089  mndlactf1o  33090  mndractf1o  33091  gsummpt2d  33110  gsumwun  33137  fzo0pmtrlast  33153  cyc3genpm  33213  cycpmconjslem2  33216  fxpval  33226  fxpgaeq  33230  cntrval2  33232  isslmd  33263  slmdlema  33264  urpropd  33292  elrgspnlem4  33306  elrgspnsubrunlem2  33309  erlcl1  33321  erlcl2  33322  erldi  33323  erlbrd  33324  erler  33326  rloccring  33331  domnprodeq0  33337  domnlcanOLD  33341  isdrng4  33356  fracerl  33367  fracfld  33369  resv1r  33399  islinds5  33427  linds2eq  33441  dvdsruassoi  33444  dvdsruasso  33445  dvdsruasso2  33446  quslsm  33465  rhmimaidl  33492  qsidomlem2  33513  ssdifidllem  33516  ssdifidl  33517  ssdifidlprm  33518  opprqus0g  33550  qsdrngilem  33554  unitmulrprm  33588  1arithidom  33597  1arithufdlem3  33606  1arithufdlem4  33607  ply1dg1rt  33640  r1pid2OLD  33669  extvfvv  33678  extvfvcl  33680  evlextv  33686  esplysply  33715  esplyind  33719  lbsdiflsp0  33770  fedgmullem1  33773  fedgmullem2  33774  irngss  33831  irngnzply1lem  33834  extdgfialglem2  33837  ply1annidllem  33845  ply1annnr  33847  minplymindeg  33852  minplyann  33853  minplyirredlem  33854  minplyirred  33855  irngnminplynz  33856  minplyelirng  33859  irredminply  33860  algextdeglem6  33866  algextdeglem7  33867  rtelextdg2lem  33870  fldext2chn  33872  constrsuc  33882  constrsslem  33885  constrconj  33889  constrextdg2lem  33892  constrextdg2  33893  constrlccllem  33897  constrcccllem  33898  constrcbvlem  33899  constrext2chn  33903  constrcon  33918  1smat1  33948  iscref  33988  metidval  34034  metidv  34036  metider  34038  pstmxmet  34041  xrmulc1cn  34074  esumfsup  34214  esumpcvgval  34222  esumcvg  34230  inelsros  34322  diffiunisros  34323  ismeas  34343  isrnmeas  34344  brae  34385  braew  34386  dya2iocuni  34427  elcarsg  34449  eulerpartleme  34507  eulerpartlemv  34508  eulerpartlemb  34512  eulerpartgbij  34516  eulerpartlemr  34518  eulerpartlemgvv  34520  eulerpartlemgh  34522  eulerpartlemn  34525  elprob  34553  ballotlemi  34645  ballotlemi1  34647  ballotlemii  34648  ballotlemsima  34660  ballotlemfrcn0  34674  signsw0g  34700  signswmnd  34701  signstfvc  34718  prodfzo03  34747  reprval  34754  reprsum  34757  reprsuc  34759  reprpmtf1o  34770  axtgupdim2ALTV  34812  brafs  34816  bnj125  35014  bnj154  35020  bnj526  35030  bnj609  35059  bnj893  35070  bnj1321  35169  bnj1491  35199  nummin  35236  fineqvnttrclselem2  35266  fineqvnttrclselem3  35267  fineqvnttrclse  35268  noinfepfnregs  35276  subgrwlk  35314  loop1cycl  35319  subfacp1lem3  35364  subfacp1lem5  35366  subfacp1lem6  35367  cnpconn  35412  txpconn  35414  ptpconn  35415  indispconn  35416  connpconn  35417  cvxpconn  35424  cvmscbv  35440  cvmsi  35447  cvmsval  35448  cvmsdisj  35452  cvmsss2  35456  cvmliftmo  35466  cvmliftlem14  35479  cvmliftiota  35483  cvmlift2lem12  35496  cvmlift2lem13  35497  cvmlift2  35498  cvmliftphtlem  35499  cvmlift3lem2  35502  cvmlift3lem4  35504  cvmlift3lem6  35506  cvmlift3lem7  35507  cvmlift3lem9  35509  cvmlift3  35510  snmlval  35513  satffunlem  35583  prv1n  35613  mrsub0  35698  mrsubcn  35701  ismfs  35731  sinccvglem  35854  br6  35939  brbigcup  36078  imageval  36110  funpartlem  36124  dfrdg4  36133  altopthsn  36143  brsegle  36290  rankeq1o  36353  cbviotadavw  36451  subtr  36496  opnbnd  36507  cldbnd  36508  isfne  36521  topfneec  36537  neibastop3  36544  dfttc4lem1  36710  dfttc4lem2  36711  dfttc4  36712  elttcirr  36713  cnndvlem2  36798  bj-imdirval2  37497  bj-imdirid  37500  bj-imdirco  37504  bj-inftyexpiinj  37523  bj-isrvecd  37612  bj-isrvec2  37614  bj-bary1lem1  37625  bj-bary1  37626  qdiff  37641  finxp00  37718  nlpfvineqsn  37725  pibp19  37730  pibt2  37733  unccur  37924  matunitlindflem2  37938  ptrecube  37941  poimirlem4  37945  poimirlem19  37960  poimirlem23  37964  poimirlem25  37966  poimirlem27  37968  poimirlem28  37969  poimirlem31  37972  poimirlem32  37973  broucube  37975  mblfinlem2  37979  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  mbfresfi  37987  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  ftc2nc  38023  cover2  38036  sdclem2  38063  fdc  38066  metf1o  38076  istotbnd3  38092  0totbnd  38094  sstotbnd2  38095  equivtotbnd  38099  totbndbnd  38110  prdstotbnd  38115  heibor1  38131  rrnmet  38150  isexid  38168  ismgmOLD  38171  opidonOLD  38173  exidu1  38177  cmpidelt  38180  exidreslem  38198  exidres  38199  exidresid  38200  grpoeqdivid  38202  elghomlem1OLD  38206  grpokerinj  38214  isrngo  38218  isrngod  38219  rngoideu  38224  isgrpda  38276  isdrngo2  38279  isdrngo3  38280  isrngohom  38286  divrngidl  38349  dmnnzd  38396  dmncan1  38397  disjeccnvep  38611  disjressuc2  38732  mopre  38792  qsdisjALTV  39020  dmqseqeq1  39048  unidmqseq  39061  disjdmqseq  39229  eldisjlem19  39234  riotasvd  39402  toycom  39419  islshpsm  39426  lshpnel2N  39431  lsatfixedN  39455  islshpat  39463  lcvexchlem4  39483  l1cvpat  39500  lkr0f  39540  lkrsc  39543  lshpkrlem1  39556  lkreqN  39616  isopos  39626  oposlem  39628  opcon2b  39643  cmtbr3N  39700  cvlcvrp  39786  hlrelat5N  39847  cvrval5  39861  cvrat4  39889  3atlem5  39933  2at0mat0  39971  psubclsetN  40382  4atex2  40523  isldil  40556  ltrnu  40567  ltrnid  40581  isdilN  40600  trlnid  40625  cdleme21k  40784  cdleme29b  40821  cdlemefrs29pre00  40841  cdlemefrs29bpre0  40842  cdlemefrs29cpre1  40844  cdleme32fva  40883  cdleme42b  40924  cdleme50ex  41005  cdleme  41006  cdlemg1a  41016  ltrniotaval  41027  cdlemeiota  41031  tendoid0  41271  cdlemksv2  41293  cdlemkuv2  41313  cdlemk36  41359  cdlemk42  41387  cdlemk  41420  tendoex  41421  cdleml3N  41424  cdleml5N  41426  tendospcanN  41469  cdlemm10N  41564  dihffval  41676  dihfval  41677  dihlsscpre  41680  islpolN  41929  mapdhval  42170  mapdheq  42174  hdmap1fval  42242  hdmap1val  42244  hdmap1eq  42247  hdmap1cbv  42248  hdmapval2lem  42277  hdmap11  42294  hdmap14lem2a  42313  hdmap14lem6  42319  hgmapval  42333  hlhillcs  42404  hlhilphllem  42405  aks4d1  42528  isprimroot  42532  mndmolinv  42534  linvh  42535  primrootsunit1  42536  primrootsunit  42537  primrootscoprmpow  42538  primrootscoprbij  42541  primrootlekpowne0  42544  primrootspoweq0  42545  ringexp0nn  42573  aks6d1c5lem1  42575  sticksstones8  42592  sticksstones9  42593  sticksstones10  42594  sticksstones11  42595  sticksstones12a  42596  sticksstones12  42597  sticksstones16  42601  sticksstones17  42602  sticksstones18  42603  sticksstones19  42604  aks6d1c6lem4  42612  aks6d1c6isolem3  42615  rhmqusspan  42624  grpods  42633  unitscyglem1  42634  unitscyglem2  42635  unitscyglem3  42636  unitscyglem5  42638  expeq1d  42756  zdivgd  42769  ef11d  42771  resubval  42799  renegadd  42804  resubeu  42809  resubadd  42811  sn-remul0ord  42840  sn-negex12  42849  addinvcom  42864  redivvald  42874  rediveud  42875  redivmuld  42877  sn-mul02  42897  mulgt0con1d  42915  mulgt0con2d  42916  fimgmcyclem  42978  fidomncyc  42980  fsuppind  43023  mhphflem  43029  prjspnfv01  43057  prjspner01  43058  prjspner1  43059  prjcrvval  43065  dffltz  43067  flt4lem7  43092  nna4b4nsq  43093  negexpidd  43114  mzpcompact2lem  43183  eldioph  43190  eldioph2lem1  43192  eldioph2lem2  43193  eldioph2  43194  eldioph2b  43195  eldioph3  43198  diophin  43204  diophun  43205  eq0rabdioph  43208  dvdsrabdioph  43238  eldioph4i  43240  diophren  43241  rabren3dioph  43243  fphpd  43244  pellexlem5  43261  pellexlem6  43262  pellex  43263  pell1qrval  43274  pell14qrval  43276  pell1234qrval  43278  pell1234qrreccl  43282  pell1234qrmulcl  43283  pell1234qrdich  43289  pell14qrdich  43297  pell1qr1  43299  pellqrexplicit  43305  rmxycomplete  43345  jm2.27  43436  rmydioph  43442  rmxdiophlem  43443  rmxdioph  43444  pw2f1ocnv  43465  pwssplit4  43517  elmnc  43564  dgraalem  43573  dgraaub  43576  dgraa0p  43577  mpaaeu  43578  mpaaval  43579  mpaalem  43580  aaitgo  43590  rngunsnply  43597  proot1ex  43624  cantnfresb  43752  tfsconcatfv  43769  tfsconcatb0  43772  tfsconcat0i  43773  tfsconcat0b  43774  tfsconcat00  43775  tfsconcatrev  43776  naddwordnexlem4  43829  sqrtcval  44068  relexpnul  44105  relexpxpnnidm  44130  relexpiidm  44131  trclfvdecomr  44155  rfovcnvf1od  44431  ntrkbimka  44465  ntrk0kbimka  44466  clsk3nimkb  44467  clsk1independent  44473  ntrclsfveq1  44487  ntrclsfveq2  44488  ntrclskb  44496  k0004val  44577  k0004val0  44581  mnringmulrcld  44655  expgrowth  44762  bcc0  44767  relpfrlem  45380  permac8prim  45441  disjinfi  45622  fsumf1of  46004  limsupmnflem  46148  liminfpnfuz  46244  climxlim2lem  46273  coseq0  46292  icccncfext  46315  dvnmptconst  46369  dvnprodlem1  46374  dvnprodlem2  46375  dvnprodlem3  46376  dvnprod  46377  stoweidlem15  46443  stoweidlem31  46459  stoweidlem35  46463  stoweidlem36  46464  stoweidlem37  46465  stoweidlem43  46471  stoweidlem44  46472  stoweidlem46  46474  stoweidlem55  46483  stoweidlem59  46487  dirkerval2  46522  dirkertrigeqlem1  46526  dirkeritg  46530  dirkercncf  46535  fourierdlem2  46537  fourierdlem3  46538  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem71  46605  fourierdlem112  46646  fourierdlem113  46647  elaa2lem  46661  etransclem11  46673  etransclem24  46686  etransclem26  46688  etransclem28  46690  etransclem35  46697  ioorrnopnxr  46735  salgenval  46749  intsaluni  46757  salgenn0  46759  salgencl  46760  sssalgen  46763  salgenss  46764  salgenuni  46765  issalgend  46766  dfsalgen2  46769  subsaliuncl  46786  sge0f1o  46810  sge0fodjrnlem  46844  ismea  46879  nnfoctbdjlem  46883  iundjiun  46888  isome  46922  caragenel  46923  ovn0lem  46993  ovnsubaddlem1  46998  smflimlem4  47202  smflim  47205  sigarcol  47292  chnsubseqwl  47309  nthrucw  47316  cfsetsnfsetf  47506  cfsetsnfsetfo  47508  fnbrafvb  47602  afv2fv0  47713  readdcnnred  47751  resubcnnred  47752  cndivrenred  47754  nnmul2  47778  ceilbi  47785  minusmodnep2tmod  47807  modmkpkne  47815  nndivides2  47832  fargshiftf1  47901  fargshiftfo  47902  ichexmpl2  47930  ichnreuop  47932  ichreuopeq  47933  elsprel  47935  prproropf1olem4  47966  reupr  47982  reuopreuprim  47986  goldbachthlem2  48009  fmtnoprmfac2lem1  48029  fmtnofac2lem  48031  prmdvdsfmtnof1lem2  48048  mod42tp1mod8  48065  lighneallem2  48069  lighneallem3  48070  lighneallem4  48073  proththd  48077  41prothprm  48082  requad01  48097  requad2  48099  dfeven2  48125  dfeven5  48142  dfodd7  48143  fpprel  48204  fppr2odd  48207  fpprwppr  48215  fpprwpprb  48216  nnsum3primesgbe  48268  isubgredg  48342  upgrimpths  48385  ushggricedg  48403  uhgrimisgrgric  48407  isubgr3stgrlem3  48444  isubgr3stgrlem4  48445  isubgr3stgrlem6  48447  grlimprclnbgr  48472  grlimgrtrilem2  48478  gpgedgvtx0  48537  gpgedgvtx1  48538  gpgvtxedg0  48539  gpgvtxedg1  48540  gpg3kgrtriexlem5  48563  gpgprismgr4cycllem3  48573  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  upwlksfval  48611  0nodd  48646  2nodd  48648  nnsgrpnmnd  48654  nn0mnd  48655  lidldomn1  48707  zlidlring  48710  uzlidlring  48711  2zrngamgm  48721  2zrngamnd  48723  2zrngagrp  48725  2zrngnmlid2  48733  ztprmneprm  48823  dmatALTbasel  48878  linindslinci  48924  lindslinindsimp1  48933  lindslinindimp2lem4  48937  lindslinindsimp2lem5  48938  linds0  48941  el0ldep  48942  lindsrng01  48944  snlindsntorlem  48946  snlindsntor  48947  ldepspr  48949  lincresunit3  48957  islindeps2  48959  isldepslvec2  48961  zlmodzxzldep  48980  blen1b  49064  dig2bits  49090  nn0sumshdiglem1  49097  0aryfvalelfv  49111  itcovalsuc  49143  prelrrx2b  49190  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  rrx2linest2  49220  elrrx2linest2  49221  spheres  49222  2sphere  49225  2sphere0  49226  line2ylem  49227  line2  49228  line2xlem  49229  line2x  49230  line2y  49231  itscnhlc0yqe  49235  itschlc0yqe  49236  itscnhlc0xyqsol  49241  itschlc0xyqsol1  49242  itsclc0xyqsolr  49245  itsclc0  49247  itsclc0b  49248  itsclinecirc0b  49250  itsclquadb  49252  itsclquadeu  49253  itscnhlinecirc02p  49261  resinsnALT  49348  sepnsepolem2  49398  sepnsepo  49399  sepfsepc  49403  iscnrm3rlem8  49422  iscnrm3r  49423  iscnrm3llem2  49425  iscnrm3l  49426  oppcendc  49493  isisod  49502  sectpropdlem  49511  ssccatid  49547  resccatlem  49548  imasubc  49626  uptrlem1  49685  oppcthinendcALT  49916  functhinclem2  49920  fullthinc2  49926  thincciso  49928  thinccisod  49929  termcpropd  49978  fulltermc2  49987  oduoppcciso  50041  discsnterm  50049  aacllem  50276