Theorem eqeq1d 2739

Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)

Hypothesis

Ref	Expression
eqeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eqeq1d	⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Proof of Theorem eqeq1d

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		dfcleq 2730	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	biimpi 216	. . 3 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		bibi1 351	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	alimi 1813	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		albi 1820	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)) → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
7	1, 3, 5, 6	4syl 19	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
8		dfcleq 2730	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
9		dfcleq 2730	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
10	7, 8, 9	3bitr4g 314	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 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 2709

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

This theorem is referenced by:  eqeq1  2741  eqcomd  2743  eqeq2d  2748  eqeqan12d  2751  neeq1d  2992  csbconstg  3857  csbhypf  3866  csbiebt  3867  csbiebg  3870  sbceq2g  4360  csbie2df  4384  disjeq0  4397  disjssun  4409  mosneq  4786  preq12b  4794  preq12bg  4797  elpreqprlem  4810  disji2  5070  invdisjrab  5073  disjprg  5082  disjxun  5084  iin0  5300  opthg  5426  opeqsng  5452  propeqop  5456  wefrc  5619  xpcan  6135  xpcan2  6136  dmsnopg  6172  rnmpt0f  6202  reuop  6252  dfpo2  6255  sspred  6269  onfr  6357  unisucg  6398  nsuceq0  6403  iotaeq  6461  iotabi  6462  fneq1  6584  fnun  6607  fnresdisj  6613  fnimadisj  6625  fnimaeq0  6626  foeq1  6743  fveqeq2d  6843  fvun1  6926  fvmptdv2  6961  fndmdifeq0  6991  fneqeql  6993  dffo3  7049  dffo3f  7053  fnnfpeq0  7127  foeqcnvco  7249  f1eqcocnv  7250  isofrlem  7289  eqfunresadj  7309  ovanraleqv  7385  f1opr  7417  eloprabga  7470  ovmpodv2  7519  ov3  7524  ovelimab  7539  caovcang  7562  caovcan  7565  caovmo  7598  caofinvl  7657  caofid1  7660  caofid2  7661  caofidlcan  7663  caonncan  7669  tfisi  7804  mptcnfimad  7933  oteqimp  7955  br1steqg  7958  br2ndeqg  7959  eqop  7978  reldm  7991  mposn  8047  fparlem1  8056  fparlem2  8057  fsplit  8061  frxp  8070  xporderlem  8071  fnwelem  8075  xpord2lem  8086  xpord3lem  8093  poseq  8102  soseq  8103  fnsuppeq0  8136  suppssov1  8141  suppssov2  8142  suppofss1d  8148  suppofss2d  8149  tposfo2  8193  mpocurryd  8213  iinon  8274  onnseq  8278  tz7.49  8378  seqomlem2  8384  oe0m1  8450  om0r  8468  oe1m  8474  oawordeulem  8483  oawordeu  8484  oarec  8491  omord  8497  oneo  8510  omeu  8514  oeeui  8532  nnm0r  8540  nnmord  8562  nnawordex  8567  nnaordex2  8569  nnneo  8585  nneob  8586  omopth  8592  nnasmo  8593  ereq1  8645  eqerlem  8673  qsdisj  8735  erov  8755  eceqoveq  8763  mapsnd  8828  endisj  8996  pw2f1olem  9013  enfixsn  9018  disjenex  9067  domssex2  9069  xpf1o  9071  mapxpen  9075  unxpdomlem2  9161  enp1ilem  9182  fodomfib  9233  fodomfibOLD  9235  fipreima  9262  opthreg  9533  cantnfp1lem3  9595  ssttrcl  9630  ttrcltr  9631  ttrclss  9635  ttrclselem2  9641  frmin  9667  updjud  9852  pm54.43  9919  dfac5  10045  dfacacn  10058  kmlem9  10075  cfeq0  10172  cfss  10181  cfslb  10182  fin23lem22  10243  fin23lem12  10247  fin23lem19  10252  fin23lem30  10258  fin23lem33  10261  fin1a2lem6  10321  axcc2lem  10352  axdc3lem2  10367  axdc3lem3  10368  axdc3lem4  10369  axdc3  10370  axdc4lem  10371  zorn2lem7  10418  ttukeylem3  10427  ttukeylem6  10430  ttukey2g  10432  fodomb  10442  axacndlem5  10528  fpwwe2cbv  10547  fpwwe2lem2  10549  fpwwe2lem3  10550  fpwwe2lem11  10558  fpwwe2lem12  10559  fpwwe  10563  pwfseqlem2  10576  pwxpndom2  10582  addnidpi  10818  ltexpi  10819  recmulnq  10881  ltexnq  10892  halfnq  10893  archnq  10897  ltexpri  10960  recexpr  10968  addsrpr  10992  mulsrpr  10993  00sr  11016  negexsr  11019  recexsrlem  11020  recexsr  11024  axrnegex  11079  axrrecex  11080  00id  11315  mul02  11318  addrid  11320  cnegex  11321  cnegex2  11322  subval  11378  subadd  11390  subadd2  11391  subsub23  11392  addsubeq4  11402  subcan2  11413  negcon1  11440  subcan  11443  addrsub  11561  ltordlem  11669  ltord1  11670  recex  11776  mul0or  11784  muleqadd  11788  receu  11789  mulcan1g  11797  divval  11805  divmul  11806  rec11  11847  ldiv  11983  rdiv  11984  ind1a  12164  zdiv  12593  uzin  12818  xaddval  13169  xmulval  13171  xnn0xadd0  13193  xnegdi  13194  ioo0  13317  ico0  13338  ioc0  13339  icc0  13340  1fv  13595  fzon  13629  fvinim0ffz  13738  flbi  13769  mod0  13829  modmuladdnn0  13871  modirr  13898  addmodlteq  13902  uzrdgfni  13914  axdc4uzlem  13939  fsuppmapnn0fiubex  13948  mptnn0fsupp  13953  seqid  14003  seqz  14006  expval  14019  expeq0  14048  sqeqor  14172  nn0opth2  14228  hashdom  14335  elprchashprn2  14352  hashbc  14409  hashf1lem1  14411  hash2pwpr  14432  ccat0  14532  wrdl1s1  14571  ccatws1lenp1b  14578  pfxsuff1eqwrdeq  14655  swrdccatin2  14685  pfxccatin12lem2  14687  2cshwcshw  14781  scshwfzeqfzo  14782  cshimadifsn  14785  cshimadifsn0  14786  s2f1o  14872  wrdlen2i  14898  2swrd2eqwrdeq  14909  wwlktovf  14912  wwlktovf1  14913  wwlktovfo  14914  wrd2f1tovbij  14916  relexp0g  14978  relexpsucnnr  14981  dfrtrcl2  15018  mulre  15077  rennim  15195  cnpart  15196  01sqrex  15205  resqrex  15206  sqrmo  15207  resqrtcl  15209  resqrtthlem  15210  sqrtgt0  15214  sqrtneg  15223  sqrtsq2  15224  absmod0  15259  sqreulem  15316  sqreu  15317  sqrtthlem  15319  eqsqrtd  15324  reusq0  15421  fsum00  15755  telfsumo  15759  prodss  15906  fprodle  15955  tanaddlem  16127  absefib  16159  efieq1re  16160  divides  16217  dvdsval2  16218  nndivides  16225  dvds0lem  16229  dvds1lem  16230  dvds2lem  16231  negdvdsb  16235  muldvds1  16243  muldvds2  16244  dvdscmulr  16247  dvdsmulcr  16248  difmod0  16250  dvdstr  16257  dvdsabseq  16276  divconjdvds  16278  odd2np1lem  16303  odd2np1  16304  even2n  16305  oddm1even  16306  2tp1odd  16315  opeo  16328  omeo  16329  m1exp1  16339  divalglem4  16359  divalglem8  16363  divalgb  16367  bitsuz  16437  smupvallem  16446  gcdaddmlem  16487  gcdabs1  16492  bezoutlem3  16504  rplpwr  16521  rprpwr  16522  alginv  16538  algcvga  16542  algfx  16543  eucalgval2  16544  coprmdvds  16616  qredeq  16620  qredeu  16621  coprmprod  16624  coprmproddvdslem  16625  divgcdcoprm0  16628  divgcdcoprmex  16629  cncongr1  16630  rpexp  16686  rpexp12i  16688  cncongrprm  16693  qnumdenbi  16708  phival  16731  phicl2  16732  dfphi2  16738  phiprmpw  16740  phimullem  16743  eulerthlem1  16745  eulerthlem2  16746  eulerth  16747  fermltl  16748  hashgcdlem  16752  phisum  16755  odzval  16756  odzdvds  16760  reumodprminv  16769  modprm0  16770  nnnn0modprm0  16771  modprmn0modprm0  16772  coprimeprodsq  16773  coprimeprodsq2  16774  pythagtriplem2  16782  pythagtrip  16799  pcval  16809  pceulem  16810  pcqmul  16818  pcqcl  16821  pcabs  16840  pcgcd1  16842  pc2dvds  16844  pcaddlem  16853  pcadd  16854  pcmpt  16857  prmpwdvds  16869  pockthi  16872  unbenlem  16873  4sqlem12  16921  ramz  16990  ramcl  16994  cshwrepswhash1  17067  imasval  17469  fvprif  17519  iscat  17632  iscatd  17633  catidex  17634  catideu  17635  cidfval  17636  cidval  17637  catidd  17640  catlid  17643  catrid  17644  catpropd  17669  cidpropd  17670  issect  17714  dfiso2  17733  invcoisoid  17753  isocoinvid  17754  setcepi  18049  latleeqj2  18412  latleeqm2  18428  oduclatb  18467  mgmidmo  18622  grpidval  18623  grpidpropd  18624  ismgmid  18627  ismgmid2  18630  mgmidsssn0  18634  grpinvalem  18635  grprida  18637  gsumvalx  18638  gsumpropd  18640  gsumpropd2lem  18641  gsumress  18644  gsumval2  18648  ismnddef  18698  sgrpidmnd  18701  ismndd  18718  mndpropd  18721  mndinvmod  18726  mnd1  18741  ismhm  18747  gsumvallem2  18796  frmdgsum  18824  frmdup3  18829  efmndmnd  18851  smndex1mnd  18875  sgrp2rid2  18891  sgrp2rid2ex  18892  pwmnd  18902  grpinvex  18913  isgrpd2  18926  isgrpd  18928  dfgrp2  18932  grpinveu  18944  grpinvval  18950  grplinv  18959  isgrpinv  18963  grplrinv  18966  grpidinv2  18967  grpidinv  18968  grplmulf1o  18983  grpraddf1o  18984  grpsubeq0  18996  grpsubadd  18998  dfgrp3lem  19008  dfgrp3  19009  grp1  19017  imasgrp2  19025  qusgrp2  19028  mhmmnd  19034  ghmgrp  19036  mulgval  19041  mulgaddcom  19068  eqg0el  19152  cycsubmel  19169  ghmeqker  19212  ghmf1  19215  conjnmzb  19222  ghmqusker  19256  isga  19260  subgga  19269  gaorb  19276  gaorber  19277  gastacl  19278  gastacos  19279  orbsta  19282  symgfix2  19385  gsmsymgrfixlem1  19396  gsmsymgrfix  19397  gsmsymgreq  19401  symgfixelq  19402  f1omvdconj  19415  pmtrdifwrdel2  19455  psgnunilem1  19462  psgnunilem2  19464  psgnunilem3  19465  psgnunilem4  19466  odval  19503  odid  19507  odlem2  19508  oddvdsnn0  19513  odnncl  19514  oddvds  19516  odcong  19518  odeq  19519  odmulgid  19523  odmulgeq  19526  gexval  19547  gexid  19550  gexlem2  19551  gexdvdsi  19552  gexdvds  19553  subgpgp  19566  sylow1lem1  19567  sylow1lem4  19570  sylow2alem1  19586  sylow2alem2  19587  sylow2blem2  19590  sylow3lem6  19601  lsmdisj3a  19658  lsmdisj3b  19659  pj1val  19664  pj1eq  19669  efgredlemd  19713  efgredlem  19716  efgred  19717  efgrelexlema  19718  frgpup3  19747  ablsubadd  19778  ablsubsub23  19793  iscyggen  19849  cyggenod  19853  gsumval3lem2  19875  gsumval3  19876  gsummptnn0fz  19955  dmdprd  19969  dprddisj  19980  dprdfeq0  19993  dprdf11  19994  dmdprdpr  20020  dpjeq  20030  ablfacrp  20037  pgpfac1lem2  20046  pgpfac1lem3  20048  pgpfac1lem5  20050  pgpfac1  20051  pgpfaclem1  20052  pgpfaclem2  20053  pgpfaclem3  20054  ablfaclem2  20057  ablfaclem3  20058  ablfac2  20060  rngmneg1  20142  rngmneg2  20143  ringurd  20160  srgrz  20182  srglz  20183  srgisid  20184  srg1zr  20190  ringid  20249  qusring2  20308  opprring  20321  dvdsrval  20335  dvdsrmul  20338  dvdsr01  20345  dvdsr02  20346  crngunit  20352  ringunitnzdiv  20372  dvreq1  20385  dvdsrpropd  20390  irredn0  20397  irredrmul  20401  irredmul  20403  rngisomring  20441  rhmdvdsr  20479  lringuplu  20515  subrg1  20553  subrgdvds  20557  isrrg  20669  rrgeq0i  20670  rrgeq0  20671  domneq0  20679  isdomn4  20687  domnlcanb  20691  domnrcanb  20693  drngid2  20723  drngmul0orOLD  20732  isdrngd  20736  isdrngdOLD  20738  fidomndrnglem  20743  isabv  20782  issrngd  20826  islmod  20853  islmodd  20855  lmodprop2d  20913  mptscmfsupp0  20916  lss1d  20952  lspextmo  21046  lvecvs0or  21101  lvecvscan  21104  lvecvscan2  21105  lbsacsbs  21149  rngqiprngimf1lem  21287  rng2idl1cntr  21298  prmirredlem  21465  pzriprnglem7  21480  pzriprnglem13  21486  chrdvds  21519  chrnzr  21523  domnchr  21525  znval  21528  zncyg  21541  znfld  21553  znunit  21556  znrrg  21558  frgpcyg  21566  psgndiflemB  21593  psgndiflemA  21594  ipeq0  21631  ip2eq  21646  elocv  21661  ocvi  21662  obsne0  21718  dsmmacl  21734  dsmmlss  21737  frlmphl  21774  frlmup4  21794  islindf4  21831  islindf5  21832  mplsubrglem  21995  mplmon2  22052  evlslem1  22073  evlseu  22074  evlsval  22077  evlsval2  22078  evlsval3  22080  ismhp3  22121  mhpsclcl  22126  mhpvarcl  22127  mhpmulcl  22128  psdmul  22145  psdmvr  22148  cply1coe0bi  22280  gsummoncoe1  22286  evl1vsd  22322  dmatel  22471  dmatelnd  22474  dmatmulcl  22478  scmateALT  22490  mdetdiaglem  22576  mdetunilem1  22590  mdetunilem3  22592  mdetunilem4  22593  mdetunilem9  22598  symgmatr01lem  22631  symgmatr01  22632  gsummatr01lem1  22633  gsummatr01lem4  22636  gsummatr01  22637  smadiadetlem3  22646  cramerlem3  22667  pmatcoe1fsupp  22679  cpmatel  22689  1elcpmat  22693  cpmatmcllem  22696  cpmatmcl  22697  d1mat2pmat  22717  m2cpminvid2lem  22732  m2cpminvid2  22733  decpmatmulsumfsupp  22751  pmatcollpw2lem  22755  pmatcollpwscmatlem1  22767  mp2pm2mplem4  22787  pm2mpmhmlem1  22796  chpscmat  22820  cpmidpmatlem3  22850  cayleyhamilton0  22867  cayleyhamiltonALT  22869  cayleyhamilton1  22870  0ntr  23049  ntreq0  23055  cldlp  23128  pnrmopn  23321  hausnei2  23331  cnhaus  23332  nrmsep  23335  isnrm2  23336  regsep2  23354  dishaus  23360  ordthauslem  23361  iscmp  23366  cmpsublem  23377  cmpsub  23378  tgcmp  23379  sscmp  23383  hauscmplem  23384  cmpfi  23386  bwth  23388  connsuba  23398  nconnsubb  23401  isref  23487  islocfin  23495  elpt  23550  elptr  23551  pthaus  23616  txcmp  23621  hausdiag  23623  txhaus  23625  txkgen  23630  xkohaus  23631  xkococnlem  23637  regr1lem  23717  fbasrn  23862  fmfnfmlem3  23934  flimtopon  23948  fclstopon  23990  alexsubb  24024  symgtgp  24084  qustgpopn  24098  qustgphaus  24101  ustuqtop  24224  isusp  24239  ispsmet  24282  psmet0  24286  ismet  24301  isxmet  24302  xmeteq0  24316  metn0  24338  xmetres2  24339  imasf1oxmet  24353  xblss2ps  24379  xblss2  24380  xmseq0  24442  comet  24491  stdbdxmet  24493  methaus  24498  dscmet  24550  nrmmetd  24552  nmeq0  24596  tngngp  24632  tngngp3  24634  nlmmul0or  24661  cnmet  24749  xrsxmet  24788  metnrmlem3  24840  icopnfcnv  24922  iccpnfcnv  24924  ishtpy  24952  isphtpy  24961  phtpyi  24964  om1elbas  25012  elpi1i  25026  pi1grplem  25029  isclmp  25077  cphsqrtcl2  25166  tcphcph  25217  bcth3  25311  rrxcph  25372  rrxmet  25388  ivth2  25435  iundisj2  25529  dyaddisj  25576  volivth  25587  mbfinf  25645  i1f1lem  25669  i1fmullem  25674  i1fmulclem  25682  i1fres  25685  itg1climres  25694  mbfi1fseqlem4  25698  dvnres  25911  dvcobr  25926  rolle  25970  cmvth  25971  deg1leb  26073  ismon1p  26121  q1peqb  26134  dvdsr1p  26142  ply1remlem  26143  fta1glem2  26147  idomrootle  26151  elply2  26174  ne0p  26185  coeeu  26203  coelem  26204  coeeq  26205  dgrle  26221  coeaddlem  26227  plymul0or  26260  ofmulrt  26261  plydivlem3  26275  plydivlem4  26276  plydivex  26277  plydiveu  26278  plydivalg  26279  quotlem  26280  plyremlem  26284  quotcan  26289  plyexmo  26293  elqaalem3  26301  qaa  26303  iaa  26305  aareccl  26306  aacjcl  26307  aannenlem2  26309  reeff1o  26428  sineq0  26504  coseq1  26505  efeq1  26508  recosf1o  26515  logeftb  26563  cosarg0d  26589  logtayl  26640  cxpval  26644  cxpeq0  26658  root1eq1  26735  cxpeq  26737  logbgcd1irr  26774  angrtmuld  26788  affineequiv  26803  affineequiv3  26805  angpieqvdlem2  26809  quad2  26819  dcubic1lem  26823  dcubic2  26824  dcubic  26826  mcubic  26827  cubic2  26828  dquartlem1  26831  dquart  26833  quart  26841  atandm2  26857  atandm4  26859  atantan  26903  wilthlem2  27049  wilthlem3  27050  muval2  27114  isnsqf  27115  mumullem2  27160  sqff1o  27162  muinv  27173  mpodvdsmulf1o  27174  dvdsmulf1o  27176  dchrelbas2  27217  dchrmullid  27232  dchrfi  27235  lgsval  27281  lgsdir  27312  lgsne0  27315  lgsprme0  27319  lgsdirnn0  27324  lgsqrlem1  27326  lgsqr  27331  gausslemma2dlem0c  27338  gausslemma2dlem0i  27344  gausslemma2dlem7  27353  gausslemma2d  27354  lgseisenlem2  27356  lgsquadlem1  27360  lgsquadlem2  27361  lgsquad2lem2  27365  lgsquad3  27367  m1lgs  27368  2lgs  27387  2sqlem7  27404  2sqlem8  27406  2sqlem9  27407  2sqlem11  27409  2sq  27410  2sq2  27413  2sqmo  27417  addsq2reu  27420  addsqn2reu  27421  addsqrexnreu  27422  addsqnreup  27423  addsq2nreurex  27424  2sqreulem1  27426  2sqreultlem  27427  2sqreunnlem1  27429  2sqreunnltlem  27430  2sqreulem4  27434  2sqreuop  27442  2sqreuopnn  27443  2sqreuoplt  27444  2sqreuopltb  27445  2sqreuopnnlt  27446  2sqreuopnnltb  27447  2sqreuopb  27448  dchrisumlem1  27469  dchrvmaeq0  27484  dchrisum0re  27493  ostth3  27618  ltsval  27628  nosepssdm  27667  nosupprefixmo  27681  noinfprefixmo  27682  nosupcbv  27683  nosupdm  27685  nosupfv  27687  nosupres  27688  nosupbnd1lem1  27689  nosupbnd1lem3  27691  nosupbnd1lem5  27693  noinfcbv  27698  noinfdm  27700  noinffv  27702  noinfres  27703  noinfbnd1lem3  27706  noinfbnd1lem5  27708  eqcuts  27794  cutbdaylt  27807  made0  27872  madecut  27892  negsid  28050  negsex  28052  subadds  28079  divsmo  28193  muls0ord  28194  divsval  28198  norecdiv  28199  recsne0  28201  divmulsw  28202  divs1  28213  precsexlem8  28223  precsexlem9  28224  precsexlem11  28226  precsex  28227  recsex  28228  abssor  28255  elons  28262  noseqrdgfn  28315  bdayn0sf1o  28379  eucliddivs  28385  zsoring  28418  n0seo  28430  zseo  28431  nohalf  28433  expsne0  28445  pw2recs  28447  halfcut  28467  z12negscl  28487  z12zsodd  28491  z12sge0  28492  renegscl  28507  istrkg3ld  28546  axtgcgrid  28548  axtgsegcon  28549  axtg5seg  28550  axtgupdim2  28556  tgjustc1  28560  tgjustc2  28561  iscgrg  28597  isismt  28619  legov  28670  legov2  28671  hlcgreu  28703  mirreu3  28739  mircgr  28742  mirbtwn  28743  ismir  28744  mireq  28750  ismidb  28863  lmiopp  28887  dfcgra2  28915  inaghl  28930  f1otrg  28956  ttgval  28960  ttgelitv  28968  brbtwn  28985  brcgr  28986  colinearalglem2  28993  colinearalg  28996  axsegconlem1  29003  axsegcon  29013  ax5seglem4  29018  ax5seglem5  29019  axpaschlem  29026  axpasch  29027  axlowdimlem16  29043  axeuclidlem  29048  axeuclid  29049  axcontlem2  29051  axcontlem4  29053  axcontlem5  29054  edglnl  29229  usgredg2ALT  29279  usgredgprvALT  29281  usgrnloopvALT  29287  ushgredgedgloop  29317  edg0usgr  29339  nb3grpr  29468  cplgr1v  29516  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  32665  disjif2  32669  disjxpin  32676  iundisj2f  32678  disjunsn  32682  fmptco1f1o  32724  ofpreima  32756  fnpreimac  32761  ressupprn  32781  curry2ima  32800  preiman0  32801  receqid  32835  xrofsup  32858  iundisj2fi  32888  f1ocnt  32891  fzo0opth  32894  elq2  32903  fprodex01  32916  sgn0bi  32931  prodindf  32940  xdivval  32996  xrecex  32997  xreceu  32999  xdivmul  33002  rexdiv  33003  wrdt2ind  33031  mndlrinvb  33103  mndlactfo  33105  mndractfo  33107  mndlactf1o  33108  mndractf1o  33109  gsummpt2d  33128  gsumwun  33155  fzo0pmtrlast  33171  cyc3genpm  33231  cycpmconjslem2  33234  fxpval  33244  fxpgaeq  33248  cntrval2  33250  isslmd  33281  slmdlema  33282  urpropd  33310  elrgspnlem4  33324  elrgspnsubrunlem2  33327  erlcl1  33339  erlcl2  33340  erldi  33341  erlbrd  33342  erler  33344  rloccring  33349  domnprodeq0  33355  domnlcanOLD  33359  isdrng4  33374  fracerl  33385  fracfld  33387  resv1r  33417  islinds5  33445  linds2eq  33459  dvdsruassoi  33462  dvdsruasso  33463  dvdsruasso2  33464  quslsm  33483  rhmimaidl  33510  qsidomlem2  33531  ssdifidllem  33534  ssdifidl  33535  ssdifidlprm  33536  opprqus0g  33568  qsdrngilem  33572  unitmulrprm  33606  1arithidom  33615  1arithufdlem3  33624  1arithufdlem4  33625  ply1dg1rt  33658  r1pid2OLD  33687  extvfvv  33696  extvfvcl  33698  evlextv  33704  esplysply  33733  esplyind  33737  lbsdiflsp0  33789  fedgmullem1  33792  fedgmullem2  33793  irngss  33850  irngnzply1lem  33853  extdgfialglem2  33856  ply1annidllem  33864  ply1annnr  33866  minplymindeg  33871  minplyann  33872  minplyirredlem  33873  minplyirred  33874  irngnminplynz  33875  minplyelirng  33878  irredminply  33879  algextdeglem6  33885  algextdeglem7  33886  rtelextdg2lem  33889  fldext2chn  33891  constrsuc  33901  constrsslem  33904  constrconj  33908  constrextdg2lem  33911  constrextdg2  33912  constrlccllem  33916  constrcccllem  33917  constrcbvlem  33918  constrext2chn  33922  constrcon  33937  1smat1  33967  iscref  34007  metidval  34053  metidv  34055  metider  34057  pstmxmet  34060  xrmulc1cn  34093  esumfsup  34233  esumpcvgval  34241  esumcvg  34249  inelsros  34341  diffiunisros  34342  ismeas  34362  isrnmeas  34363  brae  34404  braew  34405  dya2iocuni  34446  elcarsg  34468  eulerpartleme  34526  eulerpartlemv  34527  eulerpartlemb  34531  eulerpartgbij  34535  eulerpartlemr  34537  eulerpartlemgvv  34539  eulerpartlemgh  34541  eulerpartlemn  34544  elprob  34572  ballotlemi  34664  ballotlemi1  34666  ballotlemii  34667  ballotlemsima  34679  ballotlemfrcn0  34693  signsw0g  34719  signswmnd  34720  signstfvc  34737  prodfzo03  34766  reprval  34773  reprsum  34776  reprsuc  34778  reprpmtf1o  34789  axtgupdim2ALTV  34831  brafs  34835  bnj125  35033  bnj154  35039  bnj526  35049  bnj609  35078  bnj893  35089  bnj1321  35188  bnj1491  35218  nummin  35255  fineqvnttrclselem2  35285  fineqvnttrclselem3  35286  fineqvnttrclse  35287  noinfepfnregs  35295  subgrwlk  35333  loop1cycl  35338  subfacp1lem3  35383  subfacp1lem5  35385  subfacp1lem6  35386  cnpconn  35431  txpconn  35433  ptpconn  35434  indispconn  35435  connpconn  35436  cvxpconn  35443  cvmscbv  35459  cvmsi  35466  cvmsval  35467  cvmsdisj  35471  cvmsss2  35475  cvmliftmo  35485  cvmliftlem14  35498  cvmliftiota  35502  cvmlift2lem12  35515  cvmlift2lem13  35516  cvmlift2  35517  cvmliftphtlem  35518  cvmlift3lem2  35521  cvmlift3lem4  35523  cvmlift3lem6  35525  cvmlift3lem7  35526  cvmlift3lem9  35528  cvmlift3  35529  snmlval  35532  satffunlem  35602  prv1n  35632  mrsub0  35717  mrsubcn  35720  ismfs  35750  sinccvglem  35873  br6  35958  brbigcup  36097  imageval  36129  funpartlem  36143  dfrdg4  36152  altopthsn  36162  brsegle  36309  rankeq1o  36372  cbviotadavw  36470  subtr  36515  opnbnd  36526  cldbnd  36527  isfne  36540  topfneec  36556  neibastop3  36563  dfttc4lem1  36729  dfttc4lem2  36730  dfttc4  36731  elttcirr  36732  cnndvlem2  36817  bj-imdirval2  37516  bj-imdirid  37519  bj-imdirco  37523  bj-inftyexpiinj  37542  bj-isrvecd  37631  bj-isrvec2  37633  bj-bary1lem1  37644  bj-bary1  37645  finxp00  37735  nlpfvineqsn  37742  pibp19  37747  pibt2  37750  unccur  37941  matunitlindflem2  37955  ptrecube  37958  poimirlem4  37962  poimirlem19  37977  poimirlem23  37981  poimirlem25  37983  poimirlem27  37985  poimirlem28  37986  poimirlem31  37989  poimirlem32  37990  broucube  37992  mblfinlem2  37996  ovoliunnfl  38000  voliunnfl  38002  volsupnfl  38003  mbfresfi  38004  itg2addnclem  38009  itg2addnclem3  38011  itg2addnc  38012  ftc2nc  38040  cover2  38053  sdclem2  38080  fdc  38083  metf1o  38093  istotbnd3  38109  0totbnd  38111  sstotbnd2  38112  equivtotbnd  38116  totbndbnd  38127  prdstotbnd  38132  heibor1  38148  rrnmet  38167  isexid  38185  ismgmOLD  38188  opidonOLD  38190  exidu1  38194  cmpidelt  38197  exidreslem  38215  exidres  38216  exidresid  38217  grpoeqdivid  38219  elghomlem1OLD  38223  grpokerinj  38231  isrngo  38235  isrngod  38236  rngoideu  38241  isgrpda  38293  isdrngo2  38296  isdrngo3  38297  isrngohom  38303  divrngidl  38366  dmnnzd  38413  dmncan1  38414  disjeccnvep  38628  disjressuc2  38749  mopre  38809  qsdisjALTV  39037  dmqseqeq1  39065  unidmqseq  39078  disjdmqseq  39246  eldisjlem19  39251  riotasvd  39419  toycom  39436  islshpsm  39443  lshpnel2N  39448  lsatfixedN  39472  islshpat  39480  lcvexchlem4  39500  l1cvpat  39517  lkr0f  39557  lkrsc  39560  lshpkrlem1  39573  lkreqN  39633  isopos  39643  oposlem  39645  opcon2b  39660  cmtbr3N  39717  cvlcvrp  39803  hlrelat5N  39864  cvrval5  39878  cvrat4  39906  3atlem5  39950  2at0mat0  39988  psubclsetN  40399  4atex2  40540  isldil  40573  ltrnu  40584  ltrnid  40598  isdilN  40617  trlnid  40642  cdleme21k  40801  cdleme29b  40838  cdlemefrs29pre00  40858  cdlemefrs29bpre0  40859  cdlemefrs29cpre1  40861  cdleme32fva  40900  cdleme42b  40941  cdleme50ex  41022  cdleme  41023  cdlemg1a  41033  ltrniotaval  41044  cdlemeiota  41048  tendoid0  41288  cdlemksv2  41310  cdlemkuv2  41330  cdlemk36  41376  cdlemk42  41404  cdlemk  41437  tendoex  41438  cdleml3N  41441  cdleml5N  41443  tendospcanN  41486  cdlemm10N  41581  dihffval  41693  dihfval  41694  dihlsscpre  41697  islpolN  41946  mapdhval  42187  mapdheq  42191  hdmap1fval  42259  hdmap1val  42261  hdmap1eq  42264  hdmap1cbv  42265  hdmapval2lem  42294  hdmap11  42311  hdmap14lem2a  42330  hdmap14lem6  42336  hgmapval  42350  hlhillcs  42421  hlhilphllem  42422  aks4d1  42545  isprimroot  42549  mndmolinv  42551  linvh  42552  primrootsunit1  42553  primrootsunit  42554  primrootscoprmpow  42555  primrootscoprbij  42558  primrootlekpowne0  42561  primrootspoweq0  42562  ringexp0nn  42590  aks6d1c5lem1  42592  sticksstones8  42609  sticksstones9  42610  sticksstones10  42611  sticksstones11  42612  sticksstones12a  42613  sticksstones12  42614  sticksstones16  42618  sticksstones17  42619  sticksstones18  42620  sticksstones19  42621  aks6d1c6lem4  42629  aks6d1c6isolem3  42632  rhmqusspan  42641  grpods  42650  unitscyglem1  42651  unitscyglem2  42652  unitscyglem3  42653  unitscyglem5  42655  expeq1d  42773  zdivgd  42786  ef11d  42788  resubval  42816  renegadd  42821  resubeu  42826  resubadd  42828  sn-remul0ord  42857  sn-negex12  42866  addinvcom  42881  redivvald  42891  rediveud  42892  redivmuld  42894  sn-mul02  42914  mulgt0con1d  42932  mulgt0con2d  42933  fimgmcyclem  42995  fidomncyc  42997  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  43259  eldioph4i  43261  diophren  43262  rabren3dioph  43264  fphpd  43265  pellexlem5  43282  pellexlem6  43283  pellex  43284  pell1qrval  43295  pell14qrval  43297  pell1234qrval  43299  pell1234qrreccl  43303  pell1234qrmulcl  43304  pell1234qrdich  43310  pell14qrdich  43318  pell1qr1  43320  pellqrexplicit  43326  rmxycomplete  43366  jm2.27  43457  rmydioph  43463  rmxdiophlem  43464  rmxdioph  43465  pw2f1ocnv  43486  pwssplit4  43538  elmnc  43585  dgraalem  43594  dgraaub  43597  dgraa0p  43598  mpaaeu  43599  mpaaval  43600  mpaalem  43601  aaitgo  43611  rngunsnply  43618  proot1ex  43645  cantnfresb  43773  tfsconcatfv  43790  tfsconcatb0  43793  tfsconcat0i  43794  tfsconcat0b  43795  tfsconcat00  43796  tfsconcatrev  43797  naddwordnexlem4  43850  sqrtcval  44089  relexpnul  44126  relexpxpnnidm  44151  relexpiidm  44152  trclfvdecomr  44176  rfovcnvf1od  44452  ntrkbimka  44486  ntrk0kbimka  44487  clsk3nimkb  44488  clsk1independent  44494  ntrclsfveq1  44508  ntrclsfveq2  44509  ntrclskb  44517  k0004val  44598  k0004val0  44602  mnringmulrcld  44676  expgrowth  44783  bcc0  44788  relpfrlem  45401  permac8prim  45462  disjinfi  45643  fsumf1of  46025  limsupmnflem  46169  liminfpnfuz  46265  climxlim2lem  46294  coseq0  46313  icccncfext  46336  dvnmptconst  46390  dvnprodlem1  46395  dvnprodlem2  46396  dvnprodlem3  46397  dvnprod  46398  stoweidlem15  46464  stoweidlem31  46480  stoweidlem35  46484  stoweidlem36  46485  stoweidlem37  46486  stoweidlem43  46492  stoweidlem44  46493  stoweidlem46  46495  stoweidlem55  46504  stoweidlem59  46508  dirkerval2  46543  dirkertrigeqlem1  46547  dirkeritg  46551  dirkercncf  46556  fourierdlem2  46558  fourierdlem3  46559  fourierdlem42  46598  fourierdlem48  46603  fourierdlem49  46604  fourierdlem71  46626  fourierdlem112  46667  fourierdlem113  46668  elaa2lem  46682  etransclem11  46694  etransclem24  46707  etransclem26  46709  etransclem28  46711  etransclem35  46718  ioorrnopnxr  46756  salgenval  46770  intsaluni  46778  salgenn0  46780  salgencl  46781  sssalgen  46784  salgenss  46785  salgenuni  46786  issalgend  46787  dfsalgen2  46790  subsaliuncl  46807  sge0f1o  46831  sge0fodjrnlem  46865  ismea  46900  nnfoctbdjlem  46904  iundjiun  46909  isome  46943  caragenel  46944  ovn0lem  47014  ovnsubaddlem1  47019  smflimlem4  47223  smflim  47226  sigarcol  47313  chnsubseqwl  47328  nthrucw  47335  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