MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeq1 Unicode version

Theorem eqeq1 2302
Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eqeq1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )

Proof of Theorem eqeq1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2290 . . . . . 6  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
21biimpi 186 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1806 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
43bibi1d 310 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  <->  x  e.  C )  <->  ( x  e.  B  <->  x  e.  C
) ) )
54albidv 1615 . 2  |-  ( A  =  B  ->  ( A. x ( x  e.  A  <->  x  e.  C
)  <->  A. x ( x  e.  B  <->  x  e.  C ) ) )
6 dfcleq 2290 . 2  |-  ( A  =  C  <->  A. x
( x  e.  A  <->  x  e.  C ) )
7 dfcleq 2290 . 2  |-  ( B  =  C  <->  A. x
( x  e.  B  <->  x  e.  C ) )
85, 6, 73bitr4g 279 1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530    = wceq 1632    e. wcel 1696
This theorem is referenced by:  eqeq1i  2303  eqeq1d  2304  eqeq2  2305  eqeq12  2308  eqtr  2313  eqsb3lem  2396  clelab  2416  neeq1  2467  pm13.18  2531  issetf  2806  sbhypf  2846  vtoclgft  2847  eqvincf  2909  pm13.183  2921  eueq  2950  mob  2960  euind  2965  reu6  2967  reu7  2973  reuind  2981  eqsbc3  3043  csbhypf  3129  uniiunlem  3273  snjust  3658  elprg  3670  elsncg  3675  sneqrg  3798  preq12bg  3807  intab  3908  uniintsn  3915  dfiin2g  3952  disji2  4026  disjprg  4035  disjxun  4037  opthg  4262  copsexg  4268  euotd  4283  elopab  4288  solin  4353  snnex  4540  uniuni  4543  eusv1  4544  reusv2lem2  4552  reusv3  4558  reusv6OLD  4561  orduninsuc  4650  elxpi  4721  opbrop  4783  relop  4850  ideqg  4851  elrnmpt  4942  elrnmpt1  4944  elrnmptg  4945  somin1  5095  cnveqb  5145  relcoi1  5217  funopg  5302  funcnvuni  5333  fun11iun  5509  fvelrnb  5586  fvmptg  5616  fndmin  5648  foelrn  5695  foco2  5696  fmptco  5707  eufnfv  5768  elabrex  5781  abrexco  5782  dff13f  5800  f1fveq  5802  isosolem  5860  f1oiso  5864  f1oweALT  5867  oprabid  5898  mpt2fun  5962  elrnmpt2g  5972  elrnmpt2  5973  ralrnmpt2  5974  ov3  6000  ov6g  6001  ovelrn  6012  caovcang  6037  caovcan  6040  eloprabi  6202  frxp  6241  dftpos4  6269  opiota  6306  eusvobj2  6353  riotasvd  6363  riotasvdOLD  6364  tz7.44-2  6436  tz7.44-3  6437  oev  6529  oalimcl  6574  omlimcl  6592  odi  6593  omeu  6599  oeeui  6616  nneob  6666  omopth  6672  elqsg  6727  qsdisj  6752  qsel  6754  brecop  6767  eroveu  6769  erovlem  6770  th3qlem1  6780  th3q  6783  elixpsn  6871  ixpsnf1o  6872  boxcutc  6875  2dom  6949  fundmen  6950  xpf1o  7039  nneneq  7060  fofinf1o  7153  elfi  7183  elfiun  7199  dffi3  7200  brwdom  7297  brwdom3  7312  unwdomg  7314  xpwdomg  7315  noinfep  7376  cantnfp1lem1  7396  cantnfp1lem3  7398  cantnfp1  7399  cantnflem1  7407  scott0  7572  carden2a  7615  cardiun  7631  pm54.43lem  7648  alephval3  7753  dfac5lem3  7768  dfac5lem4  7769  dfac2  7773  kmlem9  7800  kmlem12  7803  cardcf  7894  cfeq0  7898  cfsuc  7899  cff1  7900  cflim2  7905  cfss  7907  isfin5  7941  fin1a2lem11  8052  fin1a2lem13  8054  brdom7disj  8172  brdom6disj  8173  canthp1lem2  8291  canthp1  8292  tskuni  8421  gruina  8456  genpv  8639  genpelv  8640  ltsosr  8732  ltresr  8778  axcnre  8802  axpre-lttri  8803  ltordlem  9314  ltord1  9315  fimaxre3  9719  supmul1  9735  supmullem1  9736  supmullem2  9737  supmul  9738  creur  9756  creui  9757  nn1m1nn  9782  elz  10042  nn0ind-raph  10128  xnegeq  10550  xmullem2  10601  xmulasslem  10621  fseqsupubi  11056  sqeqor  11233  nn0opth2  11303  ccatco  11506  shftfval  11581  sqrlem6  11749  cbvsum  12184  summo  12206  fsum  12209  fsumtscopo  12276  infcvgaux1i  12331  infcvgaux2i  12332  mertenslem1  12356  mertenslem2  12357  mertens  12358  ruclem12  12535  divalg  12618  ndvdssub  12622  bitsinvp1  12656  sadcp1  12662  smupp1  12687  gcdval  12703  bezoutlem1  12733  bezoutlem3  12735  bezoutlem4  12736  bezout  12737  dvdsprime  12787  nprm  12788  dvdsprm  12794  coprm  12795  qnumval  12824  qdenval  12825  pcval  12913  pceu  12915  pczpre  12916  pcdiv  12921  4sqlem2  13012  4sqlem4  13015  4sqlem12  13019  4sq  13027  vdwapval  13036  vdwapun  13037  vdwlem6  13049  acsfn  13577  posi  14100  gsumval2a  14475  ghmf1  14727  conjnmzb  14733  orbsta  14783  odval  14865  dfod2  14893  submod  14896  isslw  14935  sylow2alem1  14944  sylow3lem2  14955  lsmelvalm  14978  lsmdisj2  15007  efgrelexlemb  15075  frgpup3lem  15102  cyggeninv  15186  cygabl  15193  gsumval3eu  15206  gsumval3  15207  dprddisj2  15290  dpjrid  15313  pgpfac1lem3  15328  abveq0  15607  abvtrivd  15621  lss1d  15736  lspsn  15775  lspsnel  15776  lspprel  15863  rrgeq0i  16046  domneq0  16054  psrlidm  16164  psrridm  16165  mvrval2  16183  mvrf1  16186  mplmonmul  16224  coe1tm  16365  coe1tmfv2  16367  xrsdsreval  16432  prmirredlem  16462  znf1o  16521  znfld  16530  znunit  16533  cygznlem3  16539  ipeq0  16558  obsip  16637  eltopspOLD  16672  istpsOLD  16674  istopon  16679  fctop  16757  cctop  16759  ppttop  16760  pptbas  16761  epttop  16762  t0sep  17068  t1sep2  17113  cmpsublem  17142  cmpsub  17143  txuni2  17276  elpt  17283  ptbasfi  17292  xkoopn  17300  ptpjopn  17322  ptclsg  17325  dfac14lem  17327  ptcnp  17332  ptrescn  17349  tx1stc  17360  qtopeu  17423  kqt0lem  17443  isr0  17444  hauspwpwf1  17698  xmeteq0  17919  imasf1oxmet  17955  comet  18075  stdbdxmet  18077  met2ndci  18084  prdsxmslem2  18091  nrmmetd  18113  tngngp  18186  xrsxmet  18331  iccpnfcnv  18458  iccpnfhmeo  18459  oprpiece1res2  18466  cnheibor  18469  phtpycc  18505  elovolm  18850  ovolgelb  18855  ovolicc1  18891  ovolicc  18898  ioorval  18945  uniioombllem6  18959  dyadmax  18969  dyadmbllem  18970  dyadmbl  18971  opnmbllem  18972  i1fadd  19066  i1fmul  19067  itg1addlem3  19069  i1fmulc  19074  itg2l  19100  itg2leub  19105  limcmpt  19249  limcco  19259  dvcobr  19311  evlslem3  19414  deg1ldg  19494  ig1pval  19574  elply  19593  elply2  19594  coeval  19621  coe1termlem  19655  coe1term  19656  quotval  19688  plydivlem4  19692  plydivex  19693  vieta1  19708  aannenlem2  19725  aalioulem2  19729  abelthlem9  19832  logtayllem  20022  logtayl  20023  isosctrlem2  20135  atantayl2  20250  leibpilem2  20253  rlimcnp2  20277  efrlim  20280  dvdsmulf1o  20450  perfectlem2  20485  lgsfval  20556  lgsval2lem  20561  lgsdchrval  20602  2sqlem2  20619  2sqlem8  20627  2sqlem9  20628  2sqlem11  20630  dchrisum0flblem1  20673  padicval  20782  padicabv  20795  ostth1  20798  gxval  20941  gxdi  20979  ismgm  21003  nvz  21251  nmosetn0  21359  nmoolb  21365  nmoubi  21366  nmlno0lem  21387  nmlno0i  21388  hvsubeq0  21663  hvaddcan  21665  normsub0  21731  norm1exi  21845  pjhval  21992  omlsii  21998  omlsi  21999  pjoml  22031  h1de2ci  22151  spansneleq  22165  h1datomi  22176  h1datom  22177  spansncv  22248  5oalem6  22254  pj11  22309  nmopsetn0  22461  nmfnsetn0  22474  nmoplb  22503  nmopub  22504  nmfnlb  22520  nmfnleub  22521  nmlnop0iALT  22591  nmlnop0  22594  lnopeq  22605  nmopun  22610  nmcexi  22622  branmfn  22701  pjnmopi  22744  pj3i  22804  atss  22942  atom1d  22949  chirred  22991  cdj3lem2  23031  elabreximd  23055  difeq  23144  fmptcof2  23244  xrge0iifcnv  23330  xrge0iifcv  23331  xrge0iifhom  23334  xrge0tmdALT  23342  xrge0tmd  23343  disji2f  23369  disjif2  23373  esumc  23445  esumpcvgval  23461  dya2iocseg  23594  probun  23637  sconpi1  23785  cvmlift3lem2  23866  ghomf1olem  24016  relexp0  24040  relexpsucr  24041  relexpsucl  24043  rtrclreclem.trans  24058  prodmo  24159  fprod  24164  br8  24184  br6  24185  br4  24186  rdgprc0  24221  dfrdg2  24223  sltval2  24381  sltintdifex  24388  sltres  24389  dfbigcup2  24510  elfuns  24525  elsingles  24528  dfiota3  24533  brimageg  24537  brdomaing  24545  brrangeg  24546  dfrdg4  24560  tfrqfree  24561  elaltxp  24581  axpaschlem  24640  axlowdimlem15  24656  axlowdim  24661  funtransport  24726  fvtransport  24727  brsegle  24803  funray  24835  fvray  24836  funline  24837  fvline  24839  ellines  24847  linethru  24848  rankeq1o  24873  supaddc  24995  supadd  24996  itg2addnclem  25003  itg2addnc  25005  copsexgb  25069  elo  25144  eloi  25189  repcpwti  25264  cbcpcp  25265  ismxl2  25370  prodeq1  25409  grpodrcan  25478  intopcoaconlem3b  25641  intopcoaconlem3  25642  fisub  25657  iint  25715  trnij  25718  ismonb2  25915  cmpmon  25918  isepib2  25925  vtarsuelt  25998  isconc1  26109  isconc2  26110  isconc3  26111  cndpv  26152  pgapspf  26155  sgplpte21b  26237  pdiveql  26271  bhp2a  26279  subtr  26327  subtr2  26328  nn0prpw  26342  unirep  26452  f1opr  26494  sdclem2  26555  sdclem1  26556  sdc  26557  fdc  26558  isbnd  26607  heibor1lem  26636  heiborlem4  26641  heiborlem6  26643  heiborlem10  26647  maxidlmax  26771  prnc  26795  isfldidl  26796  dmnnzd  26803  elrfi  26872  nacsfg  26883  mzpcompact2lem  26932  eldioph2b  26945  eldioph3  26948  eldiophss  26957  diophrex  26958  elnn0rabdioph  26987  rencldnfilem  27006  elpell1qr  27035  elpell14qr  27037  elpell1234qr  27039  divalgmodcl  27183  jm2.27  27204  rmydioph  27210  expdiophlem2  27218  wepwsolem  27241  aomclem6  27259  uvcvval  27338  ellspd  27357  lnr2i  27423  lpirlnr  27424  hbtlem2  27431  hbtlem4  27433  hbtlem5  27435  rngunsnply  27481  flcidc  27482  psgneu  27532  psgnval  27533  psgnvali  27534  psgnvalii  27535  pm13.192  27713  refsum2cnlem1  27811  stoweidlem46  27898  afv0fv0  28117  afvfv0bi  28120  afvelrnb  28131  afvelrnb0  28132  f1veqaeq  28188  wlkntrllem5  28349  fargshiftf1  28382  fargshiftfo  28383  constr3trllem2  28397  frgra3vlem1  28424  3vfriswmgralem  28428  sgnval  28499  equncomVD  28960  csbingVD  28976  csbsngVD  28985  csbfv12gALTVD  28991  relopabVD  28993  bnj1468  29194  lshpdisj  29799  lsat0cv  29845  lcvexchlem4  29849  lcvexchlem5  29850  lshpkrlem1  29922  lshpkrlem2  29923  lshpkrlem3  29924  lshpkrcl  29928  islshpkrN  29932  atnle  30129  glbconxN  30189  isline  30550  ispointN  30553  pmapglbx  30580  ispsubcl2N  30758  lhp2atnle  30844  cdleme43fsv1snlem  31231  cdleme40v  31280  cdlemkid5  31746  cdlemkid  31747  dvhb1dimN  31797  dib1dim  31977  dicopelval  31989  dicelval1sta  31999  diclspsn  32006  dihvalcqpre  32047  dihglblem2aN  32105  dihglblem2N  32106  dih1dimatlem  32141  dihpN  32148  dochfl1  32288  lcfl7N  32313  lcf1o  32363  hvmapvalvalN  32573  hdmapval2lem  32646
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator