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  rspcedeq1vd  3585  csbconstg  3870  csbhypf  3879  csbiebt  3880  csbiebg  3883  sbceq2g  4373  csbie2df  4397  disjeq0  4410  disjssun  4422  mosneq  4800  preq12b  4808  preq12bg  4811  elpreqprlem  4824  disji2  5084  invdisjrab  5087  disjprg  5096  disjxun  5098  iin0  5309  opthg  5433  opeqsng  5459  propeqop  5463  wefrc  5626  xpcan  6142  xpcan2  6143  dmsnopg  6179  rnmpt0f  6209  reuop  6259  dfpo2  6262  sspred  6276  onfr  6364  unisucg  6405  nsuceq0  6410  iotaeq  6468  iotabi  6469  fneq1  6591  fnun  6614  fnresdisj  6620  fnimadisj  6632  fnimaeq0  6633  foeq1  6750  fveqeq2d  6850  fvun1  6933  fvmptdv2  6968  fndmdifeq0  6998  fneqeql  7000  dffo3  7056  dffo3f  7060  fnnfpeq0  7134  foeqcnvco  7256  f1eqcocnv  7257  isofrlem  7296  eqfunresadj  7316  ovanraleqv  7392  f1opr  7424  eloprabga  7477  ovmpodv2  7526  ov3  7531  ovelimab  7546  caovcang  7569  caovcan  7572  caovmo  7605  caofinvl  7664  caofid1  7667  caofid2  7668  caofidlcan  7670  caonncan  7676  tfisi  7811  mptcnfimad  7940  oteqimp  7962  br1steqg  7965  br2ndeqg  7966  eqop  7985  reldm  7998  mposn  8055  fparlem1  8064  fparlem2  8065  fsplit  8069  frxp  8078  xporderlem  8079  fnwelem  8083  xpord2lem  8094  xpord3lem  8101  poseq  8110  soseq  8111  fnsuppeq0  8144  suppssov1  8149  suppssov2  8150  suppofss1d  8156  suppofss2d  8157  tposfo2  8201  mpocurryd  8221  iinon  8282  onnseq  8286  tz7.49  8386  seqomlem2  8392  oe0m1  8458  om0r  8476  oe1m  8482  oawordeulem  8491  oawordeu  8492  oarec  8499  omord  8505  oneo  8518  omeu  8522  oeeui  8540  nnm0r  8548  nnmord  8570  nnawordex  8575  nnaordex2  8577  nnneo  8593  nneob  8594  omopth  8600  nnasmo  8601  ereq1  8653  eqerlem  8681  qsdisj  8743  erov  8763  eceqoveq  8771  mapsnd  8836  endisj  9004  pw2f1olem  9021  enfixsn  9026  disjenex  9075  domssex2  9077  xpf1o  9079  mapxpen  9083  unxpdomlem2  9169  enp1ilem  9190  fodomfib  9241  fodomfibOLD  9243  fipreima  9270  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  11320  mul02  11323  addrid  11325  cnegex  11326  cnegex2  11327  subval  11383  subadd  11395  subadd2  11396  subsub23  11397  addsubeq4  11407  subcan2  11418  negcon1  11445  subcan  11448  addrsub  11566  ltordlem  11674  ltord1  11675  recex  11781  mul0or  11789  muleqadd  11793  receu  11794  mulcan1g  11802  divval  11810  divmul  11811  rec11  11851  ldiv  11987  rdiv  11988  zdiv  12574  uzin  12799  xaddval  13150  xmulval  13152  xnn0xadd0  13174  xnegdi  13175  ioo0  13298  ico0  13319  ioc0  13320  icc0  13321  1fv  13575  fzon  13608  fvinim0ffz  13717  flbi  13748  mod0  13808  modmuladdnn0  13850  modirr  13877  addmodlteq  13881  uzrdgfni  13893  axdc4uzlem  13918  fsuppmapnn0fiubex  13927  mptnn0fsupp  13932  seqid  13982  seqz  13985  expval  13998  expeq0  14027  sqeqor  14151  nn0opth2  14207  hashdom  14314  elprchashprn2  14331  hashbc  14388  hashf1lem1  14390  hash2pwpr  14411  ccat0  14511  wrdl1s1  14550  ccatws1lenp1b  14557  pfxsuff1eqwrdeq  14634  swrdccatin2  14664  pfxccatin12lem2  14666  2cshwcshw  14760  scshwfzeqfzo  14761  cshimadifsn  14764  cshimadifsn0  14765  s2f1o  14851  wrdlen2i  14877  2swrd2eqwrdeq  14888  wwlktovf  14891  wwlktovf1  14892  wwlktovfo  14893  wrd2f1tovbij  14895  relexp0g  14957  relexpsucnnr  14960  dfrtrcl2  14997  mulre  15056  rennim  15174  cnpart  15175  01sqrex  15184  resqrex  15185  sqrmo  15186  resqrtcl  15188  resqrtthlem  15189  sqrtgt0  15193  sqrtneg  15202  sqrtsq2  15203  absmod0  15238  sqreulem  15295  sqreu  15296  sqrtthlem  15298  eqsqrtd  15303  reusq0  15400  fsum00  15733  telfsumo  15737  prodss  15882  fprodle  15931  tanaddlem  16103  absefib  16135  efieq1re  16136  divides  16193  dvdsval2  16194  nndivides  16201  dvds0lem  16205  dvds1lem  16206  dvds2lem  16207  negdvdsb  16211  muldvds1  16219  muldvds2  16220  dvdscmulr  16223  dvdsmulcr  16224  difmod0  16226  dvdstr  16233  dvdsabseq  16252  divconjdvds  16254  odd2np1lem  16279  odd2np1  16280  even2n  16281  oddm1even  16282  2tp1odd  16291  opeo  16304  omeo  16305  m1exp1  16315  divalglem4  16335  divalglem8  16339  divalgb  16343  bitsuz  16413  smupvallem  16422  gcdaddmlem  16463  gcdabs1  16468  bezoutlem3  16480  rplpwr  16497  rprpwr  16498  alginv  16514  algcvga  16518  algfx  16519  eucalgval2  16520  coprmdvds  16592  qredeq  16596  qredeu  16597  coprmprod  16600  coprmproddvdslem  16601  divgcdcoprm0  16604  divgcdcoprmex  16605  cncongr1  16606  rpexp  16661  rpexp12i  16663  cncongrprm  16668  qnumdenbi  16683  phival  16706  phicl2  16707  dfphi2  16713  phiprmpw  16715  phimullem  16718  eulerthlem1  16720  eulerthlem2  16721  eulerth  16722  fermltl  16723  hashgcdlem  16727  phisum  16730  odzval  16731  odzdvds  16735  reumodprminv  16744  modprm0  16745  nnnn0modprm0  16746  modprmn0modprm0  16747  coprimeprodsq  16748  coprimeprodsq2  16749  pythagtriplem2  16757  pythagtrip  16774  pcval  16784  pceulem  16785  pcqmul  16793  pcqcl  16796  pcabs  16815  pcgcd1  16817  pc2dvds  16819  pcaddlem  16828  pcadd  16829  pcmpt  16832  prmpwdvds  16844  pockthi  16847  unbenlem  16848  4sqlem12  16896  ramz  16965  ramcl  16969  cshwrepswhash1  17042  imasval  17444  fvprif  17494  iscat  17607  iscatd  17608  catidex  17609  catideu  17610  cidfval  17611  cidval  17612  catidd  17615  catlid  17618  catrid  17619  catpropd  17644  cidpropd  17645  issect  17689  dfiso2  17708  invcoisoid  17728  isocoinvid  17729  setcepi  18024  latleeqj2  18387  latleeqm2  18403  oduclatb  18442  mgmidmo  18597  grpidval  18598  grpidpropd  18599  ismgmid  18602  ismgmid2  18605  mgmidsssn0  18609  grpinvalem  18610  grprida  18612  gsumvalx  18613  gsumpropd  18615  gsumpropd2lem  18616  gsumress  18619  gsumval2  18623  ismnddef  18673  sgrpidmnd  18676  ismndd  18693  mndpropd  18696  mndinvmod  18701  mnd1  18716  ismhm  18722  gsumvallem2  18771  frmdgsum  18799  frmdup3  18804  efmndmnd  18826  smndex1mnd  18847  sgrp2rid2  18863  sgrp2rid2ex  18864  pwmnd  18874  grpinvex  18885  isgrpd2  18898  isgrpd  18900  dfgrp2  18904  grpinveu  18916  grpinvval  18922  grplinv  18931  isgrpinv  18935  grplrinv  18938  grpidinv2  18939  grpidinv  18940  grplmulf1o  18955  grpraddf1o  18956  grpsubeq0  18968  grpsubadd  18970  dfgrp3lem  18980  dfgrp3  18981  grp1  18989  imasgrp2  18997  qusgrp2  19000  mhmmnd  19006  ghmgrp  19008  mulgval  19013  mulgaddcom  19040  eqg0el  19124  cycsubmel  19141  ghmeqker  19184  ghmf1  19187  conjnmzb  19194  ghmqusker  19228  isga  19232  subgga  19241  gaorb  19248  gaorber  19249  gastacl  19250  gastacos  19251  orbsta  19254  symgfix2  19357  gsmsymgrfixlem1  19368  gsmsymgrfix  19369  gsmsymgreq  19373  symgfixelq  19374  f1omvdconj  19387  pmtrdifwrdel2  19427  psgnunilem1  19434  psgnunilem2  19436  psgnunilem3  19437  psgnunilem4  19438  odval  19475  odid  19479  odlem2  19480  oddvdsnn0  19485  odnncl  19486  oddvds  19488  odcong  19490  odeq  19491  odmulgid  19495  odmulgeq  19498  gexval  19519  gexid  19522  gexlem2  19523  gexdvdsi  19524  gexdvds  19525  subgpgp  19538  sylow1lem1  19539  sylow1lem4  19542  sylow2alem1  19558  sylow2alem2  19559  sylow2blem2  19562  sylow3lem6  19573  lsmdisj3a  19630  lsmdisj3b  19631  pj1val  19636  pj1eq  19641  efgredlemd  19685  efgredlem  19688  efgred  19689  efgrelexlema  19690  frgpup3  19719  ablsubadd  19750  ablsubsub23  19765  iscyggen  19821  cyggenod  19825  gsumval3lem2  19847  gsumval3  19848  gsummptnn0fz  19927  dmdprd  19941  dprddisj  19952  dprdfeq0  19965  dprdf11  19966  dmdprdpr  19992  dpjeq  20002  ablfacrp  20009  pgpfac1lem2  20018  pgpfac1lem3  20020  pgpfac1lem5  20022  pgpfac1  20023  pgpfaclem1  20024  pgpfaclem2  20025  pgpfaclem3  20026  ablfaclem2  20029  ablfaclem3  20030  ablfac2  20032  rngmneg1  20114  rngmneg2  20115  ringurd  20132  srgrz  20154  srglz  20155  srgisid  20156  srg1zr  20162  ringid  20221  qusring2  20282  opprring  20295  dvdsrval  20309  dvdsrmul  20312  dvdsr01  20319  dvdsr02  20320  crngunit  20326  ringunitnzdiv  20346  dvreq1  20359  dvdsrpropd  20364  irredn0  20371  irredrmul  20375  irredmul  20377  rngisomring  20415  rhmdvdsr  20453  lringuplu  20489  subrg1  20527  subrgdvds  20531  isrrg  20643  rrgeq0i  20644  rrgeq0  20645  domneq0  20653  isdomn4  20661  domnlcanb  20665  domnrcanb  20667  drngid2  20697  drngmul0orOLD  20706  isdrngd  20710  isdrngdOLD  20712  fidomndrnglem  20717  isabv  20756  issrngd  20800  islmod  20827  islmodd  20829  lmodprop2d  20887  mptscmfsupp0  20890  lss1d  20926  lspextmo  21020  lvecvs0or  21075  lvecvscan  21078  lvecvscan2  21079  lbsacsbs  21123  rngqiprngimf1lem  21261  rng2idl1cntr  21272  prmirredlem  21439  pzriprnglem7  21454  pzriprnglem13  21460  chrdvds  21493  chrnzr  21497  domnchr  21499  znval  21502  zncyg  21515  znfld  21527  znunit  21530  znrrg  21532  frgpcyg  21540  psgndiflemB  21567  psgndiflemA  21568  ipeq0  21605  ip2eq  21620  elocv  21635  ocvi  21636  obsne0  21692  dsmmacl  21708  dsmmlss  21711  frlmphl  21748  frlmup4  21768  islindf4  21805  islindf5  21806  mplsubrglem  21971  mplmon2  22028  evlslem1  22049  evlseu  22050  evlsval  22053  evlsval2  22054  evlsval3  22056  ismhp3  22097  mhpsclcl  22102  mhpvarcl  22103  mhpmulcl  22104  psdmul  22121  psdmvr  22124  cply1coe0bi  22258  gsummoncoe1  22264  evl1vsd  22300  dmatel  22449  dmatelnd  22452  dmatmulcl  22456  scmateALT  22468  mdetdiaglem  22554  mdetunilem1  22568  mdetunilem3  22570  mdetunilem4  22571  mdetunilem9  22576  symgmatr01lem  22609  symgmatr01  22610  gsummatr01lem1  22611  gsummatr01lem4  22614  gsummatr01  22615  smadiadetlem3  22624  cramerlem3  22645  pmatcoe1fsupp  22657  cpmatel  22667  1elcpmat  22671  cpmatmcllem  22674  cpmatmcl  22675  d1mat2pmat  22695  m2cpminvid2lem  22710  m2cpminvid2  22711  decpmatmulsumfsupp  22729  pmatcollpw2lem  22733  pmatcollpwscmatlem1  22745  mp2pm2mplem4  22765  pm2mpmhmlem1  22774  chpscmat  22798  cpmidpmatlem3  22828  cayleyhamilton0  22845  cayleyhamiltonALT  22847  cayleyhamilton1  22848  0ntr  23027  ntreq0  23033  cldlp  23106  pnrmopn  23299  hausnei2  23309  cnhaus  23310  nrmsep  23313  isnrm2  23314  regsep2  23332  dishaus  23338  ordthauslem  23339  iscmp  23344  cmpsublem  23355  cmpsub  23356  tgcmp  23357  sscmp  23361  hauscmplem  23362  cmpfi  23364  bwth  23366  connsuba  23376  nconnsubb  23379  isref  23465  islocfin  23473  elpt  23528  elptr  23529  pthaus  23594  txcmp  23599  hausdiag  23601  txhaus  23603  txkgen  23608  xkohaus  23609  xkococnlem  23615  regr1lem  23695  fbasrn  23840  fmfnfmlem3  23912  flimtopon  23926  fclstopon  23968  alexsubb  24002  symgtgp  24062  qustgpopn  24076  qustgphaus  24079  ustuqtop  24202  isusp  24217  ispsmet  24260  psmet0  24264  ismet  24279  isxmet  24280  xmeteq0  24294  metn0  24316  xmetres2  24317  imasf1oxmet  24331  xblss2ps  24357  xblss2  24358  xmseq0  24420  comet  24469  stdbdxmet  24471  methaus  24476  dscmet  24528  nrmmetd  24530  nmeq0  24574  tngngp  24610  tngngp3  24612  nlmmul0or  24639  cnmet  24727  xrsxmet  24766  metnrmlem3  24818  icopnfcnv  24908  iccpnfcnv  24910  ishtpy  24939  isphtpy  24948  phtpyi  24951  om1elbas  25000  elpi1i  25014  pi1grplem  25017  isclmp  25065  cphsqrtcl2  25154  tcphcph  25205  bcth3  25299  rrxcph  25360  rrxmet  25376  ivth2  25424  iundisj2  25518  dyaddisj  25565  volivth  25576  mbfinf  25634  i1f1lem  25658  i1fmullem  25663  i1fmulclem  25671  i1fres  25674  itg1climres  25683  mbfi1fseqlem4  25687  dvnres  25901  dvcobr  25917  dvcobrOLD  25918  rolle  25962  cmvth  25963  cmvthOLD  25964  deg1leb  26068  ismon1p  26116  q1peqb  26129  dvdsr1p  26137  ply1remlem  26138  fta1glem2  26142  idomrootle  26146  elply2  26169  ne0p  26180  coeeu  26198  coelem  26199  coeeq  26200  dgrle  26216  coeaddlem  26222  plymul0or  26256  ofmulrt  26257  plydivlem3  26271  plydivlem4  26272  plydivex  26273  plydiveu  26274  plydivalg  26275  quotlem  26276  plyremlem  26280  quotcan  26285  plyexmo  26289  elqaalem3  26297  qaa  26299  iaa  26301  aareccl  26302  aacjcl  26303  aannenlem2  26305  reeff1o  26425  sineq0  26501  coseq1  26502  efeq1  26505  recosf1o  26512  logeftb  26560  cosarg0d  26586  logtayl  26637  cxpval  26641  cxpeq0  26655  root1eq1  26733  cxpeq  26735  logbgcd1irr  26772  angrtmuld  26786  affineequiv  26801  affineequiv3  26803  angpieqvdlem2  26807  quad2  26817  dcubic1lem  26821  dcubic2  26822  dcubic  26824  mcubic  26825  cubic2  26826  dquartlem1  26829  dquart  26831  quart  26839  atandm2  26855  atandm4  26857  atantan  26901  wilthlem2  27047  wilthlem3  27048  muval2  27112  isnsqf  27113  mumullem2  27158  sqff1o  27160  muinv  27171  mpodvdsmulf1o  27172  dvdsmulf1o  27174  dchrelbas2  27216  dchrmullid  27231  dchrfi  27234  lgsval  27280  lgsdir  27311  lgsne0  27314  lgsprme0  27318  lgsdirnn0  27323  lgsqrlem1  27325  lgsqr  27330  gausslemma2dlem0c  27337  gausslemma2dlem0i  27343  gausslemma2dlem7  27352  gausslemma2d  27353  lgseisenlem2  27355  lgsquadlem1  27359  lgsquadlem2  27360  lgsquad2lem2  27364  lgsquad3  27366  m1lgs  27367  2lgs  27386  2sqlem7  27403  2sqlem8  27405  2sqlem9  27406  2sqlem11  27408  2sq  27409  2sq2  27412  2sqmo  27416  addsq2reu  27419  addsqn2reu  27420  addsqrexnreu  27421  addsqnreup  27422  addsq2nreurex  27423  2sqreulem1  27425  2sqreultlem  27426  2sqreunnlem1  27428  2sqreunnltlem  27429  2sqreulem4  27433  2sqreuop  27441  2sqreuopnn  27442  2sqreuoplt  27443  2sqreuopltb  27444  2sqreuopnnlt  27445  2sqreuopnnltb  27446  2sqreuopb  27447  dchrisumlem1  27468  dchrvmaeq0  27483  dchrisum0re  27492  ostth3  27617  ltsval  27627  nosepssdm  27666  nosupprefixmo  27680  noinfprefixmo  27681  nosupcbv  27682  nosupdm  27684  nosupfv  27686  nosupres  27687  nosupbnd1lem1  27688  nosupbnd1lem3  27690  nosupbnd1lem5  27692  noinfcbv  27697  noinfdm  27699  noinffv  27701  noinfres  27702  noinfbnd1lem3  27705  noinfbnd1lem5  27707  eqcuts  27793  cutbdaylt  27806  made0  27871  madecut  27891  negsid  28049  negsex  28051  subadds  28078  divsmo  28192  muls0ord  28193  divsval  28197  norecdiv  28198  recsne0  28200  divmulsw  28201  divs1  28212  precsexlem8  28222  precsexlem9  28223  precsexlem11  28225  precsex  28226  recsex  28227  abssor  28254  elons  28261  noseqrdgfn  28314  bdayn0sf1o  28378  eucliddivs  28384  zsoring  28417  n0seo  28429  zseo  28430  nohalf  28432  expsne0  28444  pw2recs  28446  halfcut  28466  z12negscl  28486  z12zsodd  28490  z12sge0  28491  renegscl  28506  istrkg3ld  28545  axtgcgrid  28547  axtgsegcon  28548  axtg5seg  28549  axtgupdim2  28555  tgjustc1  28559  tgjustc2  28560  iscgrg  28596  isismt  28618  legov  28669  legov2  28670  hlcgreu  28702  mirreu3  28738  mircgr  28741  mirbtwn  28742  ismir  28743  mireq  28749  ismidb  28862  lmiopp  28886  dfcgra2  28914  inaghl  28929  f1otrg  28955  ttgval  28959  ttgelitv  28967  brbtwn  28984  brcgr  28985  colinearalglem2  28992  colinearalg  28995  axsegconlem1  29002  axsegcon  29012  ax5seglem4  29017  ax5seglem5  29018  axpaschlem  29025  axpasch  29026  axlowdimlem16  29042  axeuclidlem  29047  axeuclid  29048  axcontlem2  29050  axcontlem4  29052  axcontlem5  29053  edglnl  29228  usgredg2ALT  29278  usgredgprvALT  29280  usgrnloopvALT  29286  ushgredgedgloop  29316  edg0usgr  29338  nb3grpr  29467  cplgr1v  29515  cusgrsize  29540  vtxdgfval  29553  vtxdeqd  29563  vtxdun  29567  vtxd0nedgb  29574  vtxdusgr0edgnelALT  29582  1loopgrvd2  29589  usgruvtxvdb  29615  usgrvd0nedg  29619  vtxdginducedm1  29629  rusgrpropedg  29670  wksfval  29695  wlklenvclwlk  29739  iswlkon  29741  ispth  29806  dfpth2  29814  upgrwlkdvdelem  29821  crctcshwlkn0lem6  29900  wwlknon  29942  wwlksm1edg  29966  wwlksnextbi  29979  wwlksnextfun  29983  wwlksnextinj  29984  wwlksnextsurj  29985  wwlksnextbij  29987  wlksnwwlknvbij  29993  wwlksnextproplem3  29996  wwlksnextprop  29997  wspn0  30009  umgr2adedgwlkonALT  30032  umgr2adedgspth  30033  umgr2wlkon  30035  rusgrnumwwlkslem  30057  rusgrnumwwlkb0  30059  rusgrnumwwlks  30062  clwlkclwwlklem2a4  30084  clwlknf1oclwwlknlem2  30169  clwlknf1oclwwlkn  30171  isclwwlknon  30178  clwwlknon1loop  30185  s2elclwwlknon2  30191  clwwlknonwwlknonb  30193  clwwlkvbij  30200  uhgr3cyclex  30269  fusgreg2wsplem  30420  fusgr2wsp2nb  30421  fusgreghash2wsp  30425  frrusgrord0  30427  2clwwlkel  30436  extwwlkfab  30439  extwwlkfabel  30440  clwwlknonclwlknonf1o  30449  dlwwlknondlwlknonf1o  30452  wlkl0  30454  numclwwlk2lem1  30463  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  numclwwlk5  30475  ex-opab  30519  isgrpo  30585  isgrpoi  30586  grpoidinvlem3  30594  grpoideu  30597  gidval  30600  grpoidinv2  30603  grpoinveu  30607  grpoinvval  30611  grpoinv  30613  vciOLD  30649  isvclem  30665  cnidOLD  30670  isnvlem  30698  nvmul0or  30738  imsmetlem  30778  diporthcom  30804  ipz  30807  nmlno0  30883  ajfval  30897  hmoval  30898  isphg  30905  isph  30910  ip2eqi  30944  ajval  30949  hvmul0or  31113  hvsubeq0  31156  hvaddeq0  31157  hvaddcan  31158  hvmulcan  31160  hvmulcan2  31161  hvsubadd  31165  his6  31187  hial0  31190  hial02  31191  hi2eq  31193  orthcom  31196  normlem7tALT  31207  normsub0  31224  normpyth  31233  hilid  31249  hhssnv  31352  ocel  31369  ocsh  31371  ocorth  31379  ocin  31384  occllem  31391  choc0  31414  pjpreeq  31486  omlsi  31492  pjoc1  31522  pjoml  31524  pjoc2  31527  chm0  31579  chocin  31583  chlejb1  31600  chlejb2  31601  chjo  31603  h1deoi  31637  h1de2i  31641  pjoml6i  31677  pjoml2  31699  pjoml3  31700  pjch  31782  hodsi  31863  hodid  31880  eigorth  31926  elunop  31960  adjeu  31977  adjval  31978  eigvecval  31984  unopf1o  32004  adj1  32021  adjeq  32023  hmdmadj  32028  lnopeq0i  32095  lnopeqi  32096  lnopeq  32097  lnfn0  32135  riesz4i  32151  riesz4  32152  riesz1  32153  cnlnadjlem3  32157  cnlnadjlem5  32159  cnlnadjeu  32166  cnlnssadj  32168  nmopadjlei  32176  opsqrlem1  32228  hmopidmpji  32240  pjimai  32264  isst  32301  ishst  32302  hstel2  32307  stadd3i  32336  stri  32345  largei  32355  golem2  32360  superpos  32442  sumdmdii  32503  mddmdin0i  32519  opreu2reuALT  32563  difeq  32605  elim2if  32631  disji2f  32664  disjif2  32668  disjxpin  32675  iundisj2f  32677  disjunsn  32681  fmptco1f1o  32723  ofpreima  32755  fnpreimac  32760  ressupprn  32780  curry2ima  32799  preiman0  32800  receqid  32835  xrofsup  32858  iundisj2fi  32888  f1ocnt  32891  fzo0opth  32894  elq2  32903  fprodex01  32917  sgn0bi  32932  ind1a  32949  prodindf  32955  xdivval  33011  xrecex  33012  xreceu  33014  xdivmul  33017  rexdiv  33018  wrdt2ind  33046  mndlrinvb  33118  mndlactfo  33120  mndractfo  33122  mndlactf1o  33123  mndractf1o  33124  gsummpt2d  33143  gsumwun  33170  fzo0pmtrlast  33186  cyc3genpm  33246  cycpmconjslem2  33249  fxpval  33259  fxpgaeq  33263  cntrval2  33265  isslmd  33296  slmdlema  33297  urpropd  33325  elrgspnlem4  33339  elrgspnsubrunlem2  33342  erlcl1  33354  erlcl2  33355  erldi  33356  erlbrd  33357  erler  33359  rloccring  33364  domnprodeq0  33370  domnlcanOLD  33374  isdrng4  33389  fracerl  33400  fracfld  33402  resv1r  33432  islinds5  33460  linds2eq  33474  dvdsruassoi  33477  dvdsruasso  33478  dvdsruasso2  33479  quslsm  33498  rhmimaidl  33525  qsidomlem2  33546  ssdifidllem  33549  ssdifidl  33550  ssdifidlprm  33551  opprqus0g  33583  qsdrngilem  33587  unitmulrprm  33621  1arithidom  33630  1arithufdlem3  33639  1arithufdlem4  33640  ply1dg1rt  33673  r1pid2OLD  33702  extvfvv  33711  extvfvcl  33713  evlextv  33719  esplysply  33748  esplyind  33752  lbsdiflsp0  33804  fedgmullem1  33807  fedgmullem2  33808  irngss  33865  irngnzply1lem  33868  extdgfialglem2  33871  ply1annidllem  33879  ply1annnr  33881  minplymindeg  33886  minplyann  33887  minplyirredlem  33888  minplyirred  33889  irngnminplynz  33890  minplyelirng  33893  irredminply  33894  algextdeglem6  33900  algextdeglem7  33901  rtelextdg2lem  33904  fldext2chn  33906  constrsuc  33916  constrsslem  33919  constrconj  33923  constrextdg2lem  33926  constrextdg2  33927  constrlccllem  33931  constrcccllem  33932  constrcbvlem  33933  constrext2chn  33937  constrcon  33952  1smat1  33982  iscref  34022  metidval  34068  metidv  34070  metider  34072  pstmxmet  34075  xrmulc1cn  34108  esumfsup  34248  esumpcvgval  34256  esumcvg  34264  inelsros  34356  diffiunisros  34357  ismeas  34377  isrnmeas  34378  brae  34419  braew  34420  dya2iocuni  34461  elcarsg  34483  eulerpartleme  34541  eulerpartlemv  34542  eulerpartlemb  34546  eulerpartgbij  34550  eulerpartlemr  34552  eulerpartlemgvv  34554  eulerpartlemgh  34556  eulerpartlemn  34559  elprob  34587  ballotlemi  34679  ballotlemi1  34681  ballotlemii  34682  ballotlemsima  34694  ballotlemfrcn0  34708  signsw0g  34734  signswmnd  34735  signstfvc  34752  prodfzo03  34781  reprval  34788  reprsum  34791  reprsuc  34793  reprpmtf1o  34804  axtgupdim2ALTV  34846  brafs  34850  bnj125  35048  bnj154  35054  bnj526  35064  bnj609  35093  bnj893  35104  bnj1321  35203  bnj1491  35233  nummin  35270  fineqvnttrclselem2  35300  fineqvnttrclselem3  35301  fineqvnttrclse  35302  noinfepfnregs  35310  subgrwlk  35348  loop1cycl  35353  subfacp1lem3  35398  subfacp1lem5  35400  subfacp1lem6  35401  cnpconn  35446  txpconn  35448  ptpconn  35449  indispconn  35450  connpconn  35451  cvxpconn  35458  cvmscbv  35474  cvmsi  35481  cvmsval  35482  cvmsdisj  35486  cvmsss2  35490  cvmliftmo  35500  cvmliftlem14  35513  cvmliftiota  35517  cvmlift2lem12  35530  cvmlift2lem13  35531  cvmlift2  35532  cvmliftphtlem  35533  cvmlift3lem2  35536  cvmlift3lem4  35538  cvmlift3lem6  35540  cvmlift3lem7  35541  cvmlift3lem9  35543  cvmlift3  35544  snmlval  35547  satffunlem  35617  prv1n  35647  mrsub0  35732  mrsubcn  35735  ismfs  35765  sinccvglem  35888  br6  35973  brbigcup  36112  imageval  36144  funpartlem  36158  dfrdg4  36167  altopthsn  36177  brsegle  36324  rankeq1o  36387  cbviotadavw  36485  subtr  36530  opnbnd  36541  cldbnd  36542  isfne  36555  topfneec  36571  neibastop3  36578  cnndvlem2  36760  bj-imdirval2  37438  bj-imdirid  37441  bj-imdirco  37445  bj-inftyexpiinj  37464  bj-isrvecd  37553  bj-isrvec2  37555  bj-bary1lem1  37566  bj-bary1  37567  finxp00  37657  nlpfvineqsn  37664  pibp19  37669  pibt2  37672  unccur  37854  matunitlindflem2  37868  ptrecube  37871  poimirlem4  37875  poimirlem19  37890  poimirlem23  37894  poimirlem25  37896  poimirlem27  37898  poimirlem28  37899  poimirlem31  37902  poimirlem32  37903  broucube  37905  mblfinlem2  37909  ovoliunnfl  37913  voliunnfl  37915  volsupnfl  37916  mbfresfi  37917  itg2addnclem  37922  itg2addnclem3  37924  itg2addnc  37925  ftc2nc  37953  cover2  37966  sdclem2  37993  fdc  37996  metf1o  38006  istotbnd3  38022  0totbnd  38024  sstotbnd2  38025  equivtotbnd  38029  totbndbnd  38040  prdstotbnd  38045  heibor1  38061  rrnmet  38080  isexid  38098  ismgmOLD  38101  opidonOLD  38103  exidu1  38107  cmpidelt  38110  exidreslem  38128  exidres  38129  exidresid  38130  grpoeqdivid  38132  elghomlem1OLD  38136  grpokerinj  38144  isrngo  38148  isrngod  38149  rngoideu  38154  isgrpda  38206  isdrngo2  38209  isdrngo3  38210  isrngohom  38216  divrngidl  38279  dmnnzd  38326  dmncan1  38327  disjeccnvep  38541  disjressuc2  38662  mopre  38722  qsdisjALTV  38950  dmqseqeq1  38978  unidmqseq  38991  disjdmqseq  39159  eldisjlem19  39164  riotasvd  39332  toycom  39349  islshpsm  39356  lshpnel2N  39361  lsatfixedN  39385  islshpat  39393  lcvexchlem4  39413  l1cvpat  39430  lkr0f  39470  lkrsc  39473  lshpkrlem1  39486  lkreqN  39546  isopos  39556  oposlem  39558  opcon2b  39573  cmtbr3N  39630  cvlcvrp  39716  hlrelat5N  39777  cvrval5  39791  cvrat4  39819  3atlem5  39863  2at0mat0  39901  psubclsetN  40312  4atex2  40453  isldil  40486  ltrnu  40497  ltrnid  40511  isdilN  40530  trlnid  40555  cdleme21k  40714  cdleme29b  40751  cdlemefrs29pre00  40771  cdlemefrs29bpre0  40772  cdlemefrs29cpre1  40774  cdleme32fva  40813  cdleme42b  40854  cdleme50ex  40935  cdleme  40936  cdlemg1a  40946  ltrniotaval  40957  cdlemeiota  40961  tendoid0  41201  cdlemksv2  41223  cdlemkuv2  41243  cdlemk36  41289  cdlemk42  41317  cdlemk  41350  tendoex  41351  cdleml3N  41354  cdleml5N  41356  tendospcanN  41399  cdlemm10N  41494  dihffval  41606  dihfval  41607  dihlsscpre  41610  islpolN  41859  mapdhval  42100  mapdheq  42104  hdmap1fval  42172  hdmap1val  42174  hdmap1eq  42177  hdmap1cbv  42178  hdmapval2lem  42207  hdmap11  42224  hdmap14lem2a  42243  hdmap14lem6  42249  hgmapval  42263  hlhillcs  42334  hlhilphllem  42335  aks4d1  42459  isprimroot  42463  mndmolinv  42465  linvh  42466  primrootsunit1  42467  primrootsunit  42468  primrootscoprmpow  42469  primrootscoprbij  42472  primrootlekpowne0  42475  primrootspoweq0  42476  ringexp0nn  42504  aks6d1c5lem1  42506  sticksstones8  42523  sticksstones9  42524  sticksstones10  42525  sticksstones11  42526  sticksstones12a  42527  sticksstones12  42528  sticksstones16  42532  sticksstones17  42533  sticksstones18  42534  sticksstones19  42535  aks6d1c6lem4  42543  aks6d1c6isolem3  42546  rhmqusspan  42555  grpods  42564  unitscyglem1  42565  unitscyglem2  42566  unitscyglem3  42567  unitscyglem5  42569  expeq1d  42694  zdivgd  42707  ef11d  42709  resubval  42737  renegadd  42742  resubeu  42747  resubadd  42749  sn-remul0ord  42778  sn-negex12  42787  addinvcom  42802  redivvald  42812  rediveud  42813  redivmuld  42815  sn-mul02  42822  mulgt0con1d  42840  mulgt0con2d  42841  fimgmcyclem  42903  fidomncyc  42905  fsuppind  42948  mhphflem  42954  prjspnfv01  42982  prjspner01  42983  prjspner1  42984  prjcrvval  42990  dffltz  42992  flt4lem7  43017  nna4b4nsq  43018  negexpidd  43039  mzpcompact2lem  43108  eldioph  43115  eldioph2lem1  43117  eldioph2lem2  43118  eldioph2  43119  eldioph2b  43120  eldioph3  43123  diophin  43129  diophun  43130  eq0rabdioph  43133  dvdsrabdioph  43167  eldioph4i  43169  diophren  43170  rabren3dioph  43172  fphpd  43173  pellexlem5  43190  pellexlem6  43191  pellex  43192  pell1qrval  43203  pell14qrval  43205  pell1234qrval  43207  pell1234qrreccl  43211  pell1234qrmulcl  43212  pell1234qrdich  43218  pell14qrdich  43226  pell1qr1  43228  pellqrexplicit  43234  rmxycomplete  43274  jm2.27  43365  rmydioph  43371  rmxdiophlem  43372  rmxdioph  43373  pw2f1ocnv  43394  pwssplit4  43446  elmnc  43493  dgraalem  43502  dgraaub  43505  dgraa0p  43506  mpaaeu  43507  mpaaval  43508  mpaalem  43509  aaitgo  43519  rngunsnply  43526  proot1ex  43553  cantnfresb  43681  tfsconcatfv  43698  tfsconcatb0  43701  tfsconcat0i  43702  tfsconcat0b  43703  tfsconcat00  43704  tfsconcatrev  43705  naddwordnexlem4  43758  sqrtcval  43997  relexpnul  44034  relexpxpnnidm  44059  relexpiidm  44060  trclfvdecomr  44084  rfovcnvf1od  44360  ntrkbimka  44394  ntrk0kbimka  44395  clsk3nimkb  44396  clsk1independent  44402  ntrclsfveq1  44416  ntrclsfveq2  44417  ntrclskb  44425  k0004val  44506  k0004val0  44510  mnringmulrcld  44584  expgrowth  44691  bcc0  44696  relpfrlem  45309  permac8prim  45370  disjinfi  45551  fsumf1of  45934  limsupmnflem  46078  liminfpnfuz  46174  climxlim2lem  46203  coseq0  46222  icccncfext  46245  dvnmptconst  46299  dvnprodlem1  46304  dvnprodlem2  46305  dvnprodlem3  46306  dvnprod  46307  stoweidlem15  46373  stoweidlem31  46389  stoweidlem35  46393  stoweidlem36  46394  stoweidlem37  46395  stoweidlem43  46401  stoweidlem44  46402  stoweidlem46  46404  stoweidlem55  46413  stoweidlem59  46417  dirkerval2  46452  dirkertrigeqlem1  46456  dirkeritg  46460  dirkercncf  46465  fourierdlem2  46467  fourierdlem3  46468  fourierdlem42  46507  fourierdlem48  46512  fourierdlem49  46513  fourierdlem71  46535  fourierdlem112  46576  fourierdlem113  46577  elaa2lem  46591  etransclem11  46603  etransclem24  46616  etransclem26  46618  etransclem28  46620  etransclem35  46627  ioorrnopnxr  46665  salgenval  46679  intsaluni  46687  salgenn0  46689  salgencl  46690  sssalgen  46693  salgenss  46694  salgenuni  46695  issalgend  46696  dfsalgen2  46699  subsaliuncl  46716  sge0f1o  46740  sge0fodjrnlem  46774  ismea  46809  nnfoctbdjlem  46813  iundjiun  46818  isome  46852  caragenel  46853  ovn0lem  46923  ovnsubaddlem1  46928  smflimlem4  47132  smflim  47135  sigarcol  47222  chnsubseqwl  47237  nthrucw  47244  cfsetsnfsetf  47418  cfsetsnfsetfo  47420  fnbrafvb  47514  afv2fv0  47625  readdcnnred  47663  resubcnnred  47664  cndivrenred  47666  ceilbi  47693  minusmodnep2tmod  47713  modmkpkne  47721  fargshiftf1  47801  fargshiftfo  47802  ichexmpl2  47830  ichnreuop  47832  ichreuopeq  47833  elsprel  47835  prproropf1olem4  47866  reupr  47882  reuopreuprim  47886  goldbachthlem2  47906  fmtnoprmfac2lem1  47926  fmtnofac2lem  47928  prmdvdsfmtnof1lem2  47945  mod42tp1mod8  47962  lighneallem2  47966  lighneallem3  47967  lighneallem4  47970  proththd  47974  41prothprm  47979  requad01  47981  requad2  47983  dfeven2  48009  dfeven5  48026  dfodd7  48027  fpprel  48088  fppr2odd  48091  fpprwppr  48099  fpprwpprb  48100  nnsum3primesgbe  48152  isubgredg  48226  upgrimpths  48269  ushggricedg  48287  uhgrimisgrgric  48291  isubgr3stgrlem3  48328  isubgr3stgrlem4  48329  isubgr3stgrlem6  48331  grlimprclnbgr  48356  grlimgrtrilem2  48362  gpgedgvtx0  48421  gpgedgvtx1  48422  gpgvtxedg0  48423  gpgvtxedg1  48424  gpg3kgrtriexlem5  48447  gpgprismgr4cycllem3  48457  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  pgnbgreunbgrlem2lem3  48476  upwlksfval  48495  0nodd  48530  2nodd  48532  nnsgrpnmnd  48538  nn0mnd  48539  lidldomn1  48591  zlidlring  48594  uzlidlring  48595  2zrngamgm  48605  2zrngamnd  48607  2zrngagrp  48609  2zrngnmlid2  48617  ztprmneprm  48707  dmatALTbasel  48762  linindslinci  48808  lindslinindsimp1  48817  lindslinindimp2lem4  48821  lindslinindsimp2lem5  48822  linds0  48825  el0ldep  48826  lindsrng01  48828  snlindsntorlem  48830  snlindsntor  48831  ldepspr  48833  lincresunit3  48841  islindeps2  48843  isldepslvec2  48845  zlmodzxzldep  48864  blen1b  48948  dig2bits  48974  nn0sumshdiglem1  48981  0aryfvalelfv  48995  itcovalsuc  49027  prelrrx2b  49074  eenglngeehlnmlem1  49097  eenglngeehlnmlem2  49098  rrx2linest2  49104  elrrx2linest2  49105  spheres  49106  2sphere  49109  2sphere0  49110  line2ylem  49111  line2  49112  line2xlem  49113  line2x  49114  line2y  49115  itscnhlc0yqe  49119  itschlc0yqe  49120  itscnhlc0xyqsol  49125  itschlc0xyqsol1  49126  itsclc0xyqsolr  49129  itsclc0  49131  itsclc0b  49132  itsclinecirc0b  49134  itsclquadb  49136  itsclquadeu  49137  itscnhlinecirc02p  49145  resinsnALT  49232  sepnsepolem2  49282  sepnsepo  49283  sepfsepc  49287  iscnrm3rlem8  49306  iscnrm3r  49307  iscnrm3llem2  49309  iscnrm3l  49310  oppcendc  49377  isisod  49386  sectpropdlem  49395  ssccatid  49431  resccatlem  49432  imasubc  49510  uptrlem1  49569  oppcthinendcALT  49800  functhinclem2  49804  fullthinc2  49810  thincciso  49812  thinccisod  49813  termcpropd  49862  fulltermc2  49871  oduoppcciso  49925  discsnterm  49933  aacllem  50160