Theorem eqeq1d 2741

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 2732	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	biimpi 217	. . 3 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		bibi1 352	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	alimi 1818	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		albi 1825	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)) → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
7	1, 3, 5, 6	4syl 19	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
8		dfcleq 2732	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
9		dfcleq 2732	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
10	7, 8, 9	3bitr4g 315	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  eqeq1  2743  eqcomd  2745  eqeq2d  2750  eqeqan12d  2753  neeq1d  2993  csbconstg  3850  csbhypf  3859  csbiebt  3860  csbiebg  3863  sbceq2g  4347  csbie2df  4371  disjeq0  4384  disjssun  4396  mosneq  4773  preq12b  4781  preq12bg  4784  elpreqprlem  4797  disji2  5056  invdisjrab  5059  disjprg  5068  disjxun  5070  iin0  5291  opthg  5417  opeqsng  5444  propeqop  5448  wefrc  5612  xpcan  6127  xpcan2  6128  dmsnopg  6164  rnmpt0f  6194  reuop  6244  dfpo2  6247  sspred  6261  onfr  6349  unisucg  6390  nsuceq0  6395  iotaeq  6453  iotabi  6454  fneq1  6576  fnun  6599  fnresdisj  6605  fnimadisj  6617  fnimaeq0  6618  foeq1  6735  fveqeq2d  6835  fvun1  6918  fvmptdv2  6954  fndmdifeq0  6985  fneqeql  6987  dffo3  7043  dffo3f  7047  fnnfpeq0  7122  foeqcnvco  7244  f1eqcocnv  7245  isofrlem  7284  eqfunresadj  7304  ovanraleqv  7380  f1opr  7412  eloprabga  7465  ovmpodv2  7514  ov3  7519  ovelimab  7534  caovcang  7557  caovcan  7560  caovmo  7593  caofinvl  7652  caofid1  7655  caofid2  7656  caofidlcan  7658  caonncan  7664  tfisi  7799  mptcnfimad  7928  oteqimp  7950  br1steqg  7953  br2ndeqg  7954  eqop  7973  reldm  7986  mposn  8042  fparlem1  8051  fparlem2  8052  fsplit  8056  frxp  8066  xporderlem  8067  fnwelem  8071  xpord2lem  8082  xpord3lem  8089  poseq  8098  soseq  8099  fnsuppeq0  8132  suppssov1  8137  suppssov2  8138  suppofss1d  8144  suppofss2d  8145  tposfo2  8189  mpocurryd  8209  iinon  8270  onnseq  8274  tz7.49  8374  seqomlem2  8380  oe0m1  8446  om0r  8464  oe1m  8470  oawordeulem  8479  oawordeu  8480  oarec  8487  omord  8493  oneo  8506  omeu  8510  oeeui  8528  nnm0r  8536  nnmord  8558  nnawordex  8563  nnaordex2  8565  nnneo  8581  nneob  8582  omopth  8588  nnasmo  8589  ereq1  8641  eqerlem  8669  qsdisj  8731  erov  8751  eceqoveq  8759  mapsnd  8824  endisj  8992  pw2f1olem  9009  enfixsn  9014  disjenex  9063  domssex2  9065  xpf1o  9067  mapxpen  9071  unxpdomlem2  9157  enp1ilem  9178  fodomfib  9229  fodomfibOLD  9231  fipreima  9258  opthreg  9530  cantnfp1lem3  9592  ssttrcl  9627  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  frmin  9664  updjud  9849  pm54.43  9916  dfac5  10042  dfacacn  10055  kmlem9  10072  cfeq0  10169  cfss  10178  cfslb  10179  fin23lem22  10240  fin23lem12  10244  fin23lem19  10249  fin23lem30  10255  fin23lem33  10258  fin1a2lem6  10318  axcc2lem  10349  axdc3lem2  10364  axdc3lem3  10365  axdc3lem4  10366  axdc3  10367  axdc4lem  10368  zorn2lem7  10415  ttukeylem3  10424  ttukeylem6  10427  ttukey2g  10429  fodomb  10439  axacndlem5  10525  fpwwe2cbv  10544  fpwwe2lem2  10546  fpwwe2lem3  10547  fpwwe2lem11  10555  fpwwe2lem12  10556  fpwwe  10560  pwfseqlem2  10573  pwxpndom2  10579  addnidpi  10815  ltexpi  10816  recmulnq  10878  ltexnq  10889  halfnq  10890  archnq  10894  ltexpri  10957  recexpr  10965  addsrpr  10989  mulsrpr  10990  00sr  11013  negexsr  11016  recexsrlem  11017  recexsr  11021  axrnegex  11076  axrrecex  11077  00id  11312  mul02  11315  addrid  11317  cnegex  11318  cnegex2  11319  subval  11375  subadd  11387  subadd2  11388  subsub23  11389  addsubeq4  11399  subcan2  11410  negcon1  11437  subcan  11440  addrsub  11558  ltordlem  11666  ltord1  11667  recex  11773  mul0or  11781  muleqadd  11785  receu  11786  mulcan1g  11794  divval  11802  divmul  11803  rec11  11844  ldiv  11980  rdiv  11981  ind1a  12161  zdiv  12590  uzin  12815  xaddval  13166  xmulval  13168  xnn0xadd0  13190  xnegdi  13191  ioo0  13314  ico0  13335  ioc0  13336  icc0  13337  1fv  13592  fzon  13626  fvinim0ffz  13735  flbi  13766  mod0  13826  modmuladdnn0  13868  modirr  13895  addmodlteq  13899  uzrdgfni  13911  axdc4uzlem  13936  fsuppmapnn0fiubex  13945  mptnn0fsupp  13950  seqid  14000  seqz  14003  expval  14016  expeq0  14045  sqeqor  14169  nn0opth2  14225  hashdom  14332  elprchashprn2  14349  hashbc  14406  hashf1lem1  14408  hash2pwpr  14429  ccat0  14529  wrdl1s1  14568  ccatws1lenp1b  14575  pfxsuff1eqwrdeq  14652  swrdccatin2  14682  pfxccatin12lem2  14684  2cshwcshw  14778  scshwfzeqfzo  14779  cshimadifsn  14782  cshimadifsn0  14783  s2f1o  14869  wrdlen2i  14895  2swrd2eqwrdeq  14906  wwlktovf  14909  wwlktovf1  14910  wwlktovfo  14911  wrd2f1tovbij  14913  relexp0g  14975  relexpsucnnr  14978  dfrtrcl2  15015  mulre  15074  rennim  15192  cnpart  15193  01sqrex  15202  resqrex  15203  sqrmo  15204  resqrtcl  15206  resqrtthlem  15207  sqrtgt0  15211  sqrtneg  15220  sqrtsq2  15221  absmod0  15256  sqreulem  15313  sqreu  15314  sqrtthlem  15316  eqsqrtd  15321  reusq0  15418  fsum00  15752  telfsumo  15756  prodss  15903  fprodle  15952  tanaddlem  16124  absefib  16156  efieq1re  16157  divides  16214  dvdsval2  16215  nndivides  16222  dvds0lem  16226  dvds1lem  16227  dvds2lem  16228  negdvdsb  16232  muldvds1  16240  muldvds2  16241  dvdscmulr  16244  dvdsmulcr  16245  difmod0  16247  dvdstr  16254  dvdsabseq  16273  divconjdvds  16275  odd2np1lem  16300  odd2np1  16301  even2n  16302  oddm1even  16303  2tp1odd  16312  opeo  16325  omeo  16326  m1exp1  16336  divalglem4  16356  divalglem8  16360  divalgb  16364  bitsuz  16434  smupvallem  16443  gcdaddmlem  16484  gcdabs1  16489  bezoutlem3  16501  rplpwr  16518  rprpwr  16519  alginv  16535  algcvga  16539  algfx  16540  eucalgval2  16541  coprmdvds  16613  qredeq  16617  qredeu  16618  coprmprod  16621  coprmproddvdslem  16622  divgcdcoprm0  16625  divgcdcoprmex  16626  cncongr1  16627  rpexp  16683  rpexp12i  16685  cncongrprm  16690  qnumdenbi  16705  phival  16728  phicl2  16729  dfphi2  16735  phiprmpw  16737  phimullem  16740  eulerthlem1  16742  eulerthlem2  16743  eulerth  16744  fermltl  16745  hashgcdlem  16749  phisum  16752  odzval  16753  odzdvds  16757  reumodprminv  16766  modprm0  16767  nnnn0modprm0  16768  modprmn0modprm0  16769  coprimeprodsq  16770  coprimeprodsq2  16771  pythagtriplem2  16779  pythagtrip  16796  pcval  16806  pceulem  16807  pcqmul  16815  pcqcl  16818  pcabs  16837  pcgcd1  16839  pc2dvds  16841  pcaddlem  16850  pcadd  16851  pcmpt  16854  prmpwdvds  16866  pockthi  16869  unbenlem  16870  4sqlem12  16918  ramz  16987  ramcl  16991  cshwrepswhash1  17064  imasval  17466  fvprif  17516  iscat  17629  iscatd  17630  catidex  17631  catideu  17632  cidfval  17633  cidval  17634  catidd  17637  catlid  17640  catrid  17641  catpropd  17666  cidpropd  17667  issect  17711  dfiso2  17730  invcoisoid  17750  isocoinvid  17751  setcepi  18046  latleeqj2  18409  latleeqm2  18425  oduclatb  18464  mgmidmo  18619  grpidval  18620  grpidpropd  18621  ismgmid  18624  ismgmid2  18627  mgmidsssn0  18631  grpinvalem  18632  grprida  18634  gsumvalx  18635  gsumpropd  18637  gsumpropd2lem  18638  gsumress  18641  gsumval2  18645  ismnddef  18695  sgrpidmnd  18698  ismndd  18715  mndpropd  18718  mndinvmod  18723  mnd1  18738  ismhm  18744  gsumvallem2  18793  frmdgsum  18821  frmdup3  18826  efmndmnd  18848  smndex1mnd  18872  sgrp2rid2  18888  sgrp2rid2ex  18889  pwmnd  18899  grpinvex  18910  isgrpd2  18923  isgrpd  18925  dfgrp2  18929  grpinveu  18941  grpinvval  18947  grplinv  18956  isgrpinv  18960  grplrinv  18963  grpidinv2  18964  grpidinv  18965  grplmulf1o  18980  grpraddf1o  18981  grpsubeq0  18993  grpsubadd  18995  dfgrp3lem  19005  dfgrp3  19006  grp1  19014  imasgrp2  19022  qusgrp2  19025  mhmmnd  19031  ghmgrp  19033  mulgval  19038  mulgaddcom  19065  eqg0el  19149  cycsubmel  19166  ghmeqker  19209  ghmf1  19212  conjnmzb  19219  ghmqusker  19253  isga  19257  subgga  19266  gaorb  19273  gaorber  19274  gastacl  19275  gastacos  19276  orbsta  19279  symgfix2  19382  gsmsymgrfixlem1  19393  gsmsymgrfix  19394  gsmsymgreq  19398  symgfixelq  19399  f1omvdconj  19412  pmtrdifwrdel2  19452  psgnunilem1  19459  psgnunilem2  19461  psgnunilem3  19462  psgnunilem4  19463  odval  19500  odid  19504  odlem2  19505  oddvdsnn0  19510  odnncl  19511  oddvds  19513  odcong  19515  odeq  19516  odmulgid  19520  odmulgeq  19523  gexval  19544  gexid  19547  gexlem2  19548  gexdvdsi  19549  gexdvds  19550  subgpgp  19563  sylow1lem1  19564  sylow1lem4  19567  sylow2alem1  19583  sylow2alem2  19584  sylow2blem2  19587  sylow3lem6  19598  lsmdisj3a  19655  lsmdisj3b  19656  pj1val  19661  pj1eq  19666  efgredlemd  19710  efgredlem  19713  efgred  19714  efgrelexlema  19715  frgpup3  19744  ablsubadd  19775  ablsubsub23  19790  iscyggen  19846  cyggenod  19850  gsumval3lem2  19872  gsumval3  19873  gsummptnn0fz  19952  dmdprd  19966  dprddisj  19977  dprdfeq0  19990  dprdf11  19991  dmdprdpr  20017  dpjeq  20027  ablfacrp  20034  pgpfac1lem2  20043  pgpfac1lem3  20045  pgpfac1lem5  20047  pgpfac1  20048  pgpfaclem1  20049  pgpfaclem2  20050  pgpfaclem3  20051  ablfaclem2  20054  ablfaclem3  20055  ablfac2  20057  rngmneg1  20139  rngmneg2  20140  ringurd  20157  srgrz  20179  srglz  20180  srgisid  20181  srg1zr  20187  ringid  20246  qusring2  20305  opprring  20318  dvdsrval  20332  dvdsrmul  20335  dvdsr01  20342  dvdsr02  20343  crngunit  20349  ringunitnzdiv  20369  dvreq1  20382  dvdsrpropd  20387  irredn0  20394  irredrmul  20398  irredmul  20400  rngisomring  20438  rhmdvdsr  20480  lringuplu  20516  subrg1  20554  subrgdvds  20558  isrrg  20670  rrgeq0i  20671  rrgeq0  20672  domneq0  20680  isdomn4  20688  domnlcanb  20692  domnrcanb  20694  drngid2  20724  drngmul0orOLD  20733  isdrngd  20737  isdrngdOLD  20739  fidomndrnglem  20744  isabv  20783  issrngd  20827  islmod  20854  islmodd  20856  lmodprop2d  20914  mptscmfsupp0  20917  lss1d  20953  lspextmo  21046  lvecvs0or  21101  lvecvscan  21104  lvecvscan2  21105  lbsacsbs  21149  rngqiprngimf1lem  21287  rng2idl1cntr  21298  prmirredlem  21447  pzriprnglem7  21462  pzriprnglem13  21468  chrdvds  21501  chrnzr  21505  domnchr  21507  znval  21510  zncyg  21523  znfld  21535  znunit  21538  znrrg  21540  frgpcyg  21548  psgndiflemB  21575  psgndiflemA  21576  ipeq0  21613  ip2eq  21628  elocv  21643  ocvi  21644  obsne0  21700  dsmmacl  21716  dsmmlss  21719  frlmphl  21756  frlmup4  21776  islindf4  21813  islindf5  21814  mplsubrglem  21978  mplmon2  22037  evlslem1  22058  evlseu  22059  evlsval  22062  evlsval2  22063  evlsval3  22065  ismhp3  22130  mhpsclcl  22135  mhpvarcl  22136  mhpmulcl  22137  psdmul  22154  psdmvr  22157  cply1coe0bi  22288  gsummoncoe1  22294  evl1vsd  22330  dmatel  22476  dmatelnd  22479  dmatmulcl  22483  scmateALT  22495  mdetdiaglem  22581  mdetunilem1  22595  mdetunilem3  22597  mdetunilem4  22598  mdetunilem9  22603  symgmatr01lem  22636  symgmatr01  22637  gsummatr01lem1  22638  gsummatr01lem4  22641  gsummatr01  22642  smadiadetlem3  22651  cramerlem3  22672  pmatcoe1fsupp  22684  cpmatel  22694  1elcpmat  22698  cpmatmcllem  22701  cpmatmcl  22702  d1mat2pmat  22722  m2cpminvid2lem  22737  m2cpminvid2  22738  decpmatmulsumfsupp  22756  pmatcollpw2lem  22760  pmatcollpwscmatlem1  22772  mp2pm2mplem4  22792  pm2mpmhmlem1  22801  chpscmat  22825  cpmidpmatlem3  22855  cayleyhamilton0  22872  cayleyhamiltonALT  22874  cayleyhamilton1  22875  0ntr  23054  ntreq0  23060  cldlp  23133  pnrmopn  23326  hausnei2  23336  cnhaus  23337  nrmsep  23340  isnrm2  23341  regsep2  23359  dishaus  23365  ordthauslem  23366  iscmp  23371  cmpsublem  23382  cmpsub  23383  tgcmp  23384  sscmp  23388  hauscmplem  23389  cmpfi  23391  bwth  23393  connsuba  23403  nconnsubb  23406  isref  23492  islocfin  23500  elpt  23555  elptr  23556  pthaus  23621  txcmp  23626  hausdiag  23628  txhaus  23630  txkgen  23635  xkohaus  23636  xkococnlem  23642  regr1lem  23722  fbasrn  23867  fmfnfmlem3  23939  flimtopon  23953  fclstopon  23995  alexsubb  24029  symgtgp  24089  qustgpopn  24103  qustgphaus  24106  ustuqtop  24229  isusp  24244  ispsmet  24287  psmet0  24291  ismet  24306  isxmet  24307  xmeteq0  24321  metn0  24343  xmetres2  24344  imasf1oxmet  24358  xblss2ps  24384  xblss2  24385  xmseq0  24447  comet  24496  stdbdxmet  24498  methaus  24503  dscmet  24555  nrmmetd  24557  nmeq0  24601  tngngp  24637  tngngp3  24639  nlmmul0or  24666  cnmet  24754  xrsxmet  24793  metnrmlem3  24845  icopnfcnv  24927  iccpnfcnv  24929  ishtpy  24957  isphtpy  24966  phtpyi  24969  om1elbas  25017  elpi1i  25031  pi1grplem  25034  isclmp  25082  cphsqrtcl2  25171  tcphcph  25222  bcth3  25316  rrxcph  25377  rrxmet  25393  ivth2  25440  iundisj2  25534  dyaddisj  25581  volivth  25592  mbfinf  25650  i1f1lem  25674  i1fmullem  25679  i1fmulclem  25687  i1fres  25690  itg1climres  25699  mbfi1fseqlem4  25703  dvnres  25916  dvcobr  25931  rolle  25975  cmvth  25976  deg1leb  26078  ismon1p  26126  q1peqb  26139  dvdsr1p  26147  ply1remlem  26148  fta1glem2  26152  idomrootle  26156  elply2  26179  ne0p  26190  coeeu  26208  coelem  26209  coeeq  26210  dgrle  26226  coeaddlem  26232  plymul0or  26265  ofmulrt  26266  plydivlem3  26279  plydivlem4  26280  plydivex  26281  plydiveu  26282  plydivalg  26283  quotlem  26284  plyremlem  26288  quotcan  26293  plyexmo  26297  elqaalem3  26305  qaa  26307  iaa  26309  aareccl  26310  aacjcl  26311  aannenlem2  26313  reeff1o  26430  sineq0  26506  coseq1  26507  efeq1  26510  recosf1o  26517  logeftb  26565  cosarg0d  26591  logtayl  26642  cxpval  26646  cxpeq0  26660  root1eq1  26737  cxpeq  26739  logbgcd1irr  26776  angrtmuld  26790  affineequiv  26805  affineequiv3  26807  angpieqvdlem2  26811  quad2  26821  dcubic1lem  26825  dcubic2  26826  dcubic  26828  mcubic  26829  cubic2  26830  dquartlem1  26833  dquart  26835  quart  26843  atandm2  26859  atandm4  26861  atantan  26905  wilthlem2  27050  wilthlem3  27051  muval2  27115  isnsqf  27116  mumullem2  27161  sqff1o  27163  muinv  27174  mpodvdsmulf1o  27175  dvdsmulf1o  27177  dchrelbas2  27218  dchrmullid  27233  dchrfi  27236  lgsval  27282  lgsdir  27313  lgsne0  27316  lgsprme0  27320  lgsdirnn0  27325  lgsqrlem1  27327  lgsqr  27332  gausslemma2dlem0c  27339  gausslemma2dlem0i  27345  gausslemma2dlem7  27354  gausslemma2d  27355  lgseisenlem2  27357  lgsquadlem1  27361  lgsquadlem2  27362  lgsquad2lem2  27366  lgsquad3  27368  m1lgs  27369  2lgs  27388  2sqlem7  27405  2sqlem8  27407  2sqlem9  27408  2sqlem11  27410  2sq  27411  2sq2  27414  2sqmo  27418  addsq2reu  27421  addsqn2reu  27422  addsqrexnreu  27423  addsqnreup  27424  addsq2nreurex  27425  2sqreulem1  27427  2sqreultlem  27428  2sqreunnlem1  27430  2sqreunnltlem  27431  2sqreulem4  27435  2sqreuop  27443  2sqreuopnn  27444  2sqreuoplt  27445  2sqreuopltb  27446  2sqreuopnnlt  27447  2sqreuopnnltb  27448  2sqreuopb  27449  dchrisumlem1  27470  dchrvmaeq0  27485  dchrisum0re  27494  ostth3  27619  ltsval  27629  nosepssdm  27668  nosupprefixmo  27682  noinfprefixmo  27683  nosupcbv  27684  nosupdm  27686  nosupfv  27688  nosupres  27689  nosupbnd1lem1  27690  nosupbnd1lem3  27692  nosupbnd1lem5  27694  noinfcbv  27699  noinfdm  27701  noinffv  27703  noinfres  27704  noinfbnd1lem3  27707  noinfbnd1lem5  27709  eqcuts  27795  cutbdaylt  27808  made0  27873  madecut  27893  negsid  28051  negsex  28053  subadds  28080  divsmo  28194  muls0ord  28195  divsval  28199  norecdiv  28200  recsne0  28202  divmulsw  28203  divs1  28214  precsexlem8  28224  precsexlem9  28225  precsexlem11  28227  precsex  28228  recsex  28229  abssor  28256  elons  28263  noseqrdgfn  28316  bdayn0sf1o  28380  eucliddivs  28386  zsoring  28419  n0seo  28431  zseo  28432  nohalf  28434  expsne0  28446  pw2recs  28448  halfcut  28468  z12negscl  28488  z12zsodd  28492  z12sge0  28493  renegscl  28508  istrkg3ld  28547  axtgcgrid  28549  axtgsegcon  28550  axtg5seg  28551  axtgupdim2  28557  tgjustc1  28561  tgjustc2  28562  iscgrg  28598  isismt  28620  legov  28671  legov2  28672  hlcgreu  28704  mirreu3  28740  mircgr  28743  mirbtwn  28744  ismir  28745  mireq  28751  ismidb  28864  lmiopp  28888  dfcgra2  28916  inaghl  28931  f1otrg  28957  ttgval  28961  ttgelitv  28969  brbtwn  28986  brcgr  28987  colinearalglem2  28994  colinearalg  28997  axsegconlem1  29004  axsegcon  29014  ax5seglem4  29019  ax5seglem5  29020  axpaschlem  29027  axpasch  29028  axlowdimlem16  29044  axeuclidlem  29049  axeuclid  29050  axcontlem2  29052  axcontlem4  29054  axcontlem5  29055  edglnl  29230  usgredg2ALT  29280  usgredgprvALT  29282  usgrnloopvALT  29288  ushgredgedgloop  29318  edg0usgr  29340  nb3grpr  29469  cplgr1v  29517  cusgrsize  29541  vtxdgfval  29554  vtxdeqd  29564  vtxdun  29568  vtxd0nedgb  29575  vtxdusgr0edgnelALT  29583  1loopgrvd2  29590  usgruvtxvdb  29616  usgrvd0nedg  29620  vtxdginducedm1  29630  rusgrpropedg  29671  wksfval  29696  wlklenvclwlk  29740  iswlkon  29742  ispth  29807  dfpth2  29815  upgrwlkdvdelem  29822  crctcshwlkn0lem6  29901  wwlknon  29943  wwlksm1edg  29967  wwlksnextbi  29980  wwlksnextfun  29984  wwlksnextinj  29985  wwlksnextsurj  29986  wwlksnextbij  29988  wlksnwwlknvbij  29994  wwlksnextproplem3  29997  wwlksnextprop  29998  wspn0  30010  umgr2adedgwlkonALT  30033  umgr2adedgspth  30034  umgr2wlkon  30036  rusgrnumwwlkslem  30058  rusgrnumwwlkb0  30060  rusgrnumwwlks  30063  clwlkclwwlklem2a4  30085  clwlknf1oclwwlknlem2  30170  clwlknf1oclwwlkn  30172  isclwwlknon  30179  clwwlknon1loop  30186  s2elclwwlknon2  30192  clwwlknonwwlknonb  30194  clwwlkvbij  30201  uhgr3cyclex  30270  fusgreg2wsplem  30421  fusgr2wsp2nb  30422  fusgreghash2wsp  30426  frrusgrord0  30428  2clwwlkel  30437  extwwlkfab  30440  extwwlkfabel  30441  clwwlknonclwlknonf1o  30450  dlwwlknondlwlknonf1o  30453  wlkl0  30455  numclwwlk2lem1  30464  numclwlk2lem2f  30465  numclwlk2lem2f1o  30467  numclwwlk5  30476  ex-opab  30520  isgrpo  30586  isgrpoi  30587  grpoidinvlem3  30595  grpoideu  30598  gidval  30601  grpoidinv2  30604  grpoinveu  30608  grpoinvval  30612  grpoinv  30614  vciOLD  30650  isvclem  30666  cnidOLD  30671  isnvlem  30699  nvmul0or  30739  imsmetlem  30779  diporthcom  30805  ipz  30808  nmlno0  30884  ajfval  30898  hmoval  30899  isphg  30906  isph  30911  ip2eqi  30945  ajval  30950  hvmul0or  31114  hvsubeq0  31157  hvaddeq0  31158  hvaddcan  31159  hvmulcan  31161  hvmulcan2  31162  hvsubadd  31166  his6  31188  hial0  31191  hial02  31192  hi2eq  31194  orthcom  31197  normlem7tALT  31208  normsub0  31225  normpyth  31234  hilid  31250  hhssnv  31353  ocel  31370  ocsh  31372  ocorth  31380  ocin  31385  occllem  31392  choc0  31415  pjpreeq  31487  omlsi  31493  pjoc1  31523  pjoml  31525  pjoc2  31528  chm0  31580  chocin  31584  chlejb1  31601  chlejb2  31602  chjo  31604  h1deoi  31638  h1de2i  31642  pjoml6i  31678  pjoml2  31700  pjoml3  31701  pjch  31783  hodsi  31864  hodid  31881  eigorth  31927  elunop  31961  adjeu  31978  adjval  31979  eigvecval  31985  unopf1o  32005  adj1  32022  adjeq  32024  hmdmadj  32029  lnopeq0i  32096  lnopeqi  32097  lnopeq  32098  lnfn0  32136  riesz4i  32152  riesz4  32153  riesz1  32154  cnlnadjlem3  32158  cnlnadjlem5  32160  cnlnadjeu  32167  cnlnssadj  32169  nmopadjlei  32177  opsqrlem1  32229  hmopidmpji  32241  pjimai  32265  isst  32302  ishst  32303  hstel2  32308  stadd3i  32337  stri  32346  largei  32356  golem2  32361  superpos  32443  sumdmdii  32504  mddmdin0i  32520  opreu2reuALT  32564  difeq  32606  elim2if  32632  disji2f  32666  disjif2  32670  disjxpin  32677  iundisj2f  32679  disjunsn  32683  fmptco1f1o  32725  ofpreima  32757  fnpreimac  32762  ressupprn  32782  curry2ima  32801  preiman0  32802  receqid  32836  xrofsup  32859  iundisj2fi  32889  f1ocnt  32892  fzo0opth  32895  elq2  32904  fprodex01  32917  sgn0bi  32932  prodindf  32941  xdivval  32997  xrecex  32998  xreceu  33000  xdivmul  33003  rexdiv  33004  wrdt2ind  33032  mndlrinvb  33104  mndlactfo  33106  mndractfo  33108  mndlactf1o  33109  mndractf1o  33110  gsummpt2d  33130  gsumwun  33157  fzo0pmtrlast  33173  cyc3genpm  33233  cycpmconjslem2  33236  fxpval  33246  fxpgaeq  33250  cntrval2  33252  isslmd  33283  slmdlema  33284  urpropd  33312  elrgspnlem4  33326  elrgspnsubrunlem2  33329  erlcl1  33341  erlcl2  33342  erldi  33343  erlbrd  33344  erler  33346  rloccring  33351  domnprodeq0  33357  domnlcanOLD  33361  isdrng4  33379  fracerl  33390  fracfld  33392  resv1r  33422  islinds5  33450  linds2eq  33464  dvdsruassoi  33467  dvdsruasso  33468  dvdsruasso2  33469  quslsm  33488  rhmimaidl  33515  qsidomlem2  33536  ssdifidllem  33539  ssdifidl  33540  ssdifidlprm  33541  opprqus0g  33573  qsdrngilem  33577  unitmulrprm  33611  1arithidom  33620  1arithufdlem3  33629  1arithufdlem4  33630  ply1dg1rt  33663  r1pid2OLD  33692  extvfvv  33718  extvfvcl  33720  evlextv  33726  esplysply  33755  esplyind  33759  lbsdiflsp0  33810  fedgmullem1  33813  fedgmullem2  33814  irngss  33871  irngnzply1lem  33874  extdgfialglem2  33877  ply1annidllem  33885  ply1annnr  33887  minplymindeg  33892  minplyann  33893  minplyirredlem  33894  minplyirred  33895  irngnminplynz  33896  minplyelirng  33899  irredminply  33900  algextdeglem6  33906  algextdeglem7  33907  rtelextdg2lem  33910  fldext2chn  33912  constrsuc  33922  constrsslem  33925  constrconj  33929  constrextdg2lem  33932  constrextdg2  33933  constrlccllem  33937  constrcccllem  33938  constrcbvlem  33939  constrext2chn  33943  constrcon  33958  1smat1  33988  iscref  34028  metidval  34074  metidv  34076  metider  34078  pstmxmet  34081  xrmulc1cn  34114  esumfsup  34254  esumpcvgval  34262  esumcvg  34270  inelsros  34362  diffiunisros  34363  ismeas  34383  isrnmeas  34384  brae  34425  braew  34426  dya2iocuni  34467  elcarsg  34489  eulerpartleme  34547  eulerpartlemv  34548  eulerpartlemb  34552  eulerpartgbij  34556  eulerpartlemr  34558  eulerpartlemgvv  34560  eulerpartlemgh  34562  eulerpartlemn  34565  elprob  34593  ballotlemi  34685  ballotlemi1  34687  ballotlemii  34688  ballotlemsima  34700  ballotlemfrcn0  34714  signsw0g  34740  signswmnd  34741  signstfvc  34758  prodfzo03  34787  reprval  34794  reprsum  34797  reprsuc  34799  reprpmtf1o  34810  axtgupdim2ALTV  34852  brafs  34856  bnj125  35054  bnj154  35060  bnj526  35070  bnj609  35099  bnj893  35110  bnj1321  35209  bnj1491  35239  nummin  35274  fineqvnttrclselem2  35303  fineqvnttrclselem3  35304  fineqvnttrclse  35305  noinfepfnregs  35313  subgrwlk  35360  loop1cycl  35365  subfacp1lem3  35410  subfacp1lem5  35412  subfacp1lem6  35413  cnpconn  35458  txpconn  35460  ptpconn  35461  indispconn  35462  connpconn  35463  cvxpconn  35470  cvmscbv  35486  cvmsi  35493  cvmsval  35494  cvmsdisj  35498  cvmsss2  35502  cvmliftmo  35512  cvmliftlem14  35525  cvmliftiota  35529  cvmlift2lem12  35542  cvmlift2lem13  35543  cvmlift2  35544  cvmliftphtlem  35545  cvmlift3lem2  35548  cvmlift3lem4  35550  cvmlift3lem6  35552  cvmlift3lem7  35553  cvmlift3lem9  35555  cvmlift3  35556  snmlval  35559  satffunlem  35629  prv1n  35659  mrsub0  35744  mrsubcn  35747  ismfs  35777  sinccvglem  35900  br6  35985  brbigcup  36124  imageval  36156  funpartlem  36170  dfrdg4  36179  altopthsn  36189  brsegle  36336  rankeq1o  36399  cbviotadavw  36497  subtr  36542  opnbnd  36553  cldbnd  36554  isfne  36567  topfneec  36583  neibastop3  36590  dfttc4lem1  36756  dfttc4lem2  36757  dfttc4  36758  elttcirr  36759  cnndvlem2  36844  bj-imdirval2  37543  bj-imdirid  37546  bj-imdirco  37550  bj-inftyexpiinj  37569  bj-isrvecd  37658  bj-isrvec2  37660  bj-bary1lem1  37671  bj-bary1  37672  qdiff  37687  finxp00  37764  nlpfvineqsn  37771  pibp19  37776  pibt2  37779  unccur  37970  matunitlindflem2  37984  ptrecube  37987  poimirlem4  37991  poimirlem19  38006  poimirlem23  38010  poimirlem25  38012  poimirlem27  38014  poimirlem28  38015  poimirlem31  38018  poimirlem32  38019  broucube  38021  mblfinlem2  38025  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  mbfresfi  38033  itg2addnclem  38038  itg2addnclem3  38040  itg2addnc  38041  ftc2nc  38069  cover2  38082  sdclem2  38109  fdc  38112  metf1o  38122  istotbnd3  38138  0totbnd  38140  sstotbnd2  38141  equivtotbnd  38145  totbndbnd  38156  prdstotbnd  38161  heibor1  38177  rrnmet  38196  isexid  38214  ismgmOLD  38217  opidonOLD  38219  exidu1  38223  cmpidelt  38226  exidreslem  38244  exidres  38245  exidresid  38246  grpoeqdivid  38248  elghomlem1OLD  38252  grpokerinj  38260  isrngo  38264  isrngod  38265  rngoideu  38270  isgrpda  38322  isdrngo2  38325  isdrngo3  38326  isrngohom  38332  divrngidl  38395  dmnnzd  38442  dmncan1  38443  disjeccnvep  38657  disjressuc2  38778  mopre  38838  qsdisjALTV  39066  dmqseqeq1  39094  unidmqseq  39107  disjdmqseq  39275  eldisjlem19  39280  riotasvd  39448  toycom  39465  islshpsm  39472  lshpnel2N  39477  lsatfixedN  39501  islshpat  39509  lcvexchlem4  39529  l1cvpat  39546  lkr0f  39586  lkrsc  39589  lshpkrlem1  39602  lkreqN  39662  isopos  39672  oposlem  39674  opcon2b  39689  cmtbr3N  39746  cvlcvrp  39832  hlrelat5N  39893  cvrval5  39907  cvrat4  39935  3atlem5  39979  2at0mat0  40017  psubclsetN  40428  4atex2  40569  isldil  40602  ltrnu  40613  ltrnid  40627  isdilN  40646  trlnid  40671  cdleme21k  40830  cdleme29b  40867  cdlemefrs29pre00  40887  cdlemefrs29bpre0  40888  cdlemefrs29cpre1  40890  cdleme32fva  40929  cdleme42b  40970  cdleme50ex  41051  cdleme  41052  cdlemg1a  41062  ltrniotaval  41073  cdlemeiota  41077  tendoid0  41317  cdlemksv2  41339  cdlemkuv2  41359  cdlemk36  41405  cdlemk42  41433  cdlemk  41466  tendoex  41467  cdleml3N  41470  cdleml5N  41472  tendospcanN  41515  cdlemm10N  41610  dihffval  41722  dihfval  41723  dihlsscpre  41726  islpolN  41975  mapdhval  42216  mapdheq  42220  hdmap1fval  42288  hdmap1val  42290  hdmap1eq  42293  hdmap1cbv  42294  hdmapval2lem  42323  hdmap11  42340  hdmap14lem2a  42359  hdmap14lem6  42365  hgmapval  42379  hlhillcs  42450  hlhilphllem  42451  aks4d1  42574  isprimroot  42578  mndmolinv  42580  linvh  42581  primrootsunit1  42582  primrootsunit  42583  primrootscoprmpow  42584  primrootscoprbij  42587  primrootlekpowne0  42590  primrootspoweq0  42591  ringexp0nn  42619  aks6d1c5lem1  42621  sticksstones8  42638  sticksstones9  42639  sticksstones10  42640  sticksstones11  42641  sticksstones12a  42642  sticksstones12  42643  sticksstones16  42647  sticksstones17  42648  sticksstones18  42649  sticksstones19  42650  aks6d1c6lem4  42658  aks6d1c6isolem3  42661  rhmqusspan  42670  grpods  42679  unitscyglem1  42680  unitscyglem2  42681  unitscyglem3  42682  unitscyglem5  42684  expeq1d  42801  zdivgd  42814  ef11d  42816  resubval  42844  renegadd  42849  resubeu  42854  resubadd  42856  sn-remul0ord  42885  sn-negex12  42894  addinvcom  42909  redivvald  42919  rediveud  42920  redivmuld  42922  sn-mul02  42942  mulgt0con1d  42960  mulgt0con2d  42961  fimgmcyclem  43019  fidomncyc  43021  fsuppind  43040  mhphflem  43046  prjspnfv01  43074  prjspner01  43075  prjspner1  43076  prjcrvval  43082  dffltz  43084  flt4lem7  43109  nna4b4nsq  43110  negexpidd  43131  mzpcompact2lem  43200  eldioph  43207  eldioph2lem1  43209  eldioph2lem2  43210  eldioph2  43211  eldioph2b  43212  eldioph3  43215  diophin  43221  diophun  43222  eq0rabdioph  43225  dvdsrabdioph  43255  eldioph4i  43257  diophren  43258  rabren3dioph  43260  fphpd  43261  pellexlem5  43278  pellexlem6  43279  pellex  43280  pell1qrval  43291  pell14qrval  43293  pell1234qrval  43295  pell1234qrreccl  43299  pell1234qrmulcl  43300  pell1234qrdich  43306  pell14qrdich  43314  pell1qr1  43316  pellqrexplicit  43322  rmxycomplete  43362  jm2.27  43453  rmydioph  43459  rmxdiophlem  43460  rmxdioph  43461  pw2f1ocnv  43482  pwssplit4  43534  elmnc  43581  dgraalem  43590  dgraaub  43593  dgraa0p  43594  mpaaeu  43595  mpaaval  43596  mpaalem  43597  aaitgo  43607  rngunsnply  43614  proot1ex  43641  cantnfresb  43769  tfsconcatfv  43786  tfsconcatb0  43789  tfsconcat0i  43790  tfsconcat0b  43791  tfsconcat00  43792  tfsconcatrev  43793  naddwordnexlem4  43846  sqrtcval  44085  relexpnul  44122  relexpxpnnidm  44147  relexpiidm  44148  trclfvdecomr  44172  rfovcnvf1od  44448  ntrkbimka  44482  ntrk0kbimka  44483  clsk3nimkb  44484  clsk1independent  44490  ntrclsfveq1  44504  ntrclsfveq2  44505  ntrclskb  44513  k0004val  44594  k0004val0  44598  mnringmulrcld  44672  expgrowth  44779  bcc0  44784  relpfrlem  45397  permac8prim  45458  disjinfi  45639  fsumf1of  46019  limsupmnflem  46163  liminfpnfuz  46259  climxlim2lem  46288  coseq0  46307  icccncfext  46330  dvnmptconst  46384  dvnprodlem1  46389  dvnprodlem2  46390  dvnprodlem3  46391  dvnprod  46392  stoweidlem15  46458  stoweidlem31  46474  stoweidlem35  46478  stoweidlem36  46479  stoweidlem37  46480  stoweidlem43  46486  stoweidlem44  46487  stoweidlem46  46489  stoweidlem55  46498  stoweidlem59  46502  dirkerval2  46537  dirkertrigeqlem1  46541  dirkeritg  46545  dirkercncf  46550  fourierdlem2  46552  fourierdlem3  46553  fourierdlem42  46592  fourierdlem48  46597  fourierdlem49  46598  fourierdlem71  46620  fourierdlem112  46661  fourierdlem113  46662  elaa2lem  46676  etransclem11  46688  etransclem24  46701  etransclem26  46703  etransclem28  46705  etransclem35  46712  ioorrnopnxr  46750  salgenval  46764  intsaluni  46772  salgenn0  46774  salgencl  46775  sssalgen  46778  salgenss  46779  salgenuni  46780  issalgend  46781  dfsalgen2  46784  subsaliuncl  46801  sge0f1o  46825  sge0fodjrnlem  46859  ismea  46894  nnfoctbdjlem  46898  iundjiun  46903  isome  46937  caragenel  46938  ovn0lem  47008  ovnsubaddlem1  47013  smflimlem4  47217  smflim  47220  sigarcol  47307  chnsubseqwl  47324  nthrucw  47331  cfsetsnfsetf  47521  cfsetsnfsetfo  47523  fnbrafvb  47617  afv2fv0  47728  readdcnnred  47766  resubcnnred  47767  cndivrenred  47769  nnmul2  47793  ceilbi  47800  minusmodnep2tmod  47822  modmkpkne  47830  nndivides2  47847  fargshiftf1  47916  fargshiftfo  47917  ichexmpl2  47945  ichnreuop  47947  ichreuopeq  47948  elsprel  47950  prproropf1olem4  47981  reupr  47997  reuopreuprim  48001  goldbachthlem2  48024  fmtnoprmfac2lem1  48044  fmtnofac2lem  48046  prmdvdsfmtnof1lem2  48063  mod42tp1mod8  48080  lighneallem2  48084  lighneallem3  48085  lighneallem4  48088  proththd  48092  41prothprm  48097  requad01  48112  requad2  48114  dfeven2  48140  dfeven5  48157  dfodd7  48158  fpprel  48219  fppr2odd  48222  fpprwppr  48230  fpprwpprb  48231  nnsum3primesgbe  48283  isubgredg  48357  upgrimpths  48400  ushggricedg  48418  uhgrimisgrgric  48422  isubgr3stgrlem3  48459  isubgr3stgrlem4  48460  isubgr3stgrlem6  48462  grlimprclnbgr  48487  grlimgrtrilem2  48493  gpgedgvtx0  48552  gpgedgvtx1  48553  gpgvtxedg0  48554  gpgvtxedg1  48555  gpg3kgrtriexlem5  48578  gpgprismgr4cycllem3  48588  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  upwlksfval  48626  0nodd  48661  2nodd  48663  nnsgrpnmnd  48669  nn0mnd  48670  lidldomn1  48722  zlidlring  48725  uzlidlring  48726  2zrngamgm  48736  2zrngamnd  48738  2zrngagrp  48740  2zrngnmlid2  48748  ztprmneprm  48838  dmatALTbasel  48893  linindslinci  48939  lindslinindsimp1  48948  lindslinindimp2lem4  48952  lindslinindsimp2lem5  48953  linds0  48956  el0ldep  48957  lindsrng01  48959  snlindsntorlem  48961  snlindsntor  48962  ldepspr  48964  lincresunit3  48972  islindeps2  48974  isldepslvec2  48976  zlmodzxzldep  48995  blen1b  49079  dig2bits  49105  nn0sumshdiglem1  49112  0aryfvalelfv  49126  itcovalsuc  49158  prelrrx2b  49205  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229  rrx2linest2  49235  elrrx2linest2  49236  spheres  49237  2sphere  49240  2sphere0  49241  line2ylem  49242  line2  49243  line2xlem  49244  line2x  49245  line2y  49246  itscnhlc0yqe  49250  itschlc0yqe  49251  itscnhlc0xyqsol  49256  itschlc0xyqsol1  49257  itsclc0xyqsolr  49260  itsclc0  49262  itsclc0b  49263  itsclinecirc0b  49265  itsclquadb  49267  itsclquadeu  49268  itscnhlinecirc02p  49276  resinsnALT  49363  sepnsepolem2  49413  sepnsepo  49414  sepfsepc  49418  iscnrm3rlem8  49437  iscnrm3r  49438  iscnrm3llem2  49440  iscnrm3l  49441  oppcendc  49508  isisod  49517  sectpropdlem  49526  ssccatid  49562  resccatlem  49563  imasubc  49641  uptrlem1  49700  oppcthinendcALT  49931  functhinclem2  49935  fullthinc2  49941  thincciso  49943  thinccisod  49944  termcpropd  49993  fulltermc2  50002  oduoppcciso  50056  discsnterm  50064  aacllem  50291