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

Theorem eqeq1 2289
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 2277 . . . . . 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 1794 . . . 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 1611 . 2  |-  ( A  =  B  ->  ( A. x ( x  e.  A  <->  x  e.  C
)  <->  A. x ( x  e.  B  <->  x  e.  C ) ) )
6 dfcleq 2277 . 2  |-  ( A  =  C  <->  A. x
( x  e.  A  <->  x  e.  C ) )
7 dfcleq 2277 . 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 1527    = wceq 1623    e. wcel 1684
This theorem is referenced by:  eqeq1i  2290  eqeq1d  2291  eqeq2  2292  eqeq12  2295  eqtr  2300  eqsb3lem  2383  clelab  2403  neeq1  2454  pm13.18  2518  issetf  2793  sbhypf  2833  vtoclgft  2834  eqvincf  2896  pm13.183  2908  eueq  2937  mob  2947  euind  2952  reu6  2954  reu7  2960  reuind  2968  eqsbc3  3030  csbhypf  3116  uniiunlem  3260  snjust  3645  elprg  3657  elsncg  3662  sneqrg  3782  preq12bg  3791  intab  3892  uniintsn  3899  dfiin2g  3936  disji2  4010  disjprg  4019  disjxun  4021  opthg  4246  copsexg  4252  euotd  4267  elopab  4272  solin  4337  snnex  4524  uniuni  4527  eusv1  4528  reusv2lem2  4536  reusv3  4542  reusv6OLD  4545  orduninsuc  4634  elxpi  4705  opbrop  4767  relop  4834  ideqg  4835  elrnmpt  4926  elrnmpt1  4928  elrnmptg  4929  somin1  5079  cnveqb  5129  relcoi1  5201  funopg  5286  funcnvuni  5317  fun11iun  5493  fvelrnb  5570  fvmptg  5600  fndmin  5632  foelrn  5679  foco2  5680  fmptco  5691  eufnfv  5752  elabrex  5765  abrexco  5766  dff13f  5784  f1fveq  5786  isosolem  5844  f1oiso  5848  f1oweALT  5851  oprabid  5882  mpt2fun  5946  elrnmpt2g  5956  elrnmpt2  5957  ralrnmpt2  5958  ov3  5984  ov6g  5985  ovelrn  5996  caovcang  6021  caovcan  6024  eloprabi  6186  frxp  6225  dftpos4  6253  opiota  6290  eusvobj2  6337  riotasvd  6347  riotasvdOLD  6348  tz7.44-2  6420  tz7.44-3  6421  oev  6513  oalimcl  6558  omlimcl  6576  odi  6577  omeu  6583  oeeui  6600  nneob  6650  omopth  6656  elqsg  6711  qsdisj  6736  qsel  6738  brecop  6751  eroveu  6753  erovlem  6754  th3qlem1  6764  th3q  6767  elixpsn  6855  ixpsnf1o  6856  boxcutc  6859  2dom  6933  fundmen  6934  xpf1o  7023  nneneq  7044  fofinf1o  7137  elfi  7167  elfiun  7183  dffi3  7184  brwdom  7281  brwdom3  7296  unwdomg  7298  xpwdomg  7299  noinfep  7360  cantnfp1lem1  7380  cantnfp1lem3  7382  cantnfp1  7383  cantnflem1  7391  scott0  7556  carden2a  7599  cardiun  7615  pm54.43lem  7632  alephval3  7737  dfac5lem3  7752  dfac5lem4  7753  dfac2  7757  kmlem9  7784  kmlem12  7787  cardcf  7878  cfeq0  7882  cfsuc  7883  cff1  7884  cflim2  7889  cfss  7891  isfin5  7925  fin1a2lem11  8036  fin1a2lem13  8038  brdom7disj  8156  brdom6disj  8157  canthp1lem2  8275  canthp1  8276  tskuni  8405  gruina  8440  genpv  8623  genpelv  8624  ltsosr  8716  ltresr  8762  axcnre  8786  axpre-lttri  8787  ltordlem  9298  ltord1  9299  fimaxre3  9703  supmul1  9719  supmullem1  9720  supmullem2  9721  supmul  9722  creur  9740  creui  9741  nn1m1nn  9766  elz  10026  nn0ind-raph  10112  xnegeq  10534  xmullem2  10585  xmulasslem  10605  fseqsupubi  11040  sqeqor  11217  nn0opth2  11287  ccatco  11490  shftfval  11565  sqrlem6  11733  cbvsum  12168  summo  12190  fsum  12193  fsumtscopo  12260  infcvgaux1i  12315  infcvgaux2i  12316  mertenslem1  12340  mertenslem2  12341  mertens  12342  ruclem12  12519  divalg  12602  ndvdssub  12606  bitsinvp1  12640  sadcp1  12646  smupp1  12671  gcdval  12687  bezoutlem1  12717  bezoutlem3  12719  bezoutlem4  12720  bezout  12721  dvdsprime  12771  nprm  12772  dvdsprm  12778  coprm  12779  qnumval  12808  qdenval  12809  pcval  12897  pceu  12899  pczpre  12900  pcdiv  12905  4sqlem2  12996  4sqlem4  12999  4sqlem12  13003  4sq  13011  vdwapval  13020  vdwapun  13021  vdwlem6  13033  acsfn  13561  posi  14084  gsumval2a  14459  ghmf1  14711  conjnmzb  14717  orbsta  14767  odval  14849  dfod2  14877  submod  14880  isslw  14919  sylow2alem1  14928  sylow3lem2  14939  lsmelvalm  14962  lsmdisj2  14991  efgrelexlemb  15059  frgpup3lem  15086  cyggeninv  15170  cygabl  15177  gsumval3eu  15190  gsumval3  15191  dprddisj2  15274  dpjrid  15297  pgpfac1lem3  15312  abveq0  15591  abvtrivd  15605  lss1d  15720  lspsn  15759  lspsnel  15760  lspprel  15847  rrgeq0i  16030  domneq0  16038  psrlidm  16148  psrridm  16149  mvrval2  16167  mvrf1  16170  mplmonmul  16208  coe1tm  16349  coe1tmfv2  16351  xrsdsreval  16416  prmirredlem  16446  znf1o  16505  znfld  16514  znunit  16517  cygznlem3  16523  ipeq0  16542  obsip  16621  eltopspOLD  16656  istpsOLD  16658  istopon  16663  fctop  16741  cctop  16743  ppttop  16744  pptbas  16745  epttop  16746  t0sep  17052  t1sep2  17097  cmpsublem  17126  cmpsub  17127  txuni2  17260  elpt  17267  ptbasfi  17276  xkoopn  17284  ptpjopn  17306  ptclsg  17309  dfac14lem  17311  ptcnp  17316  ptrescn  17333  tx1stc  17344  qtopeu  17407  kqt0lem  17427  isr0  17428  hauspwpwf1  17682  xmeteq0  17903  imasf1oxmet  17939  comet  18059  stdbdxmet  18061  met2ndci  18068  prdsxmslem2  18075  nrmmetd  18097  tngngp  18170  xrsxmet  18315  iccpnfcnv  18442  iccpnfhmeo  18443  oprpiece1res2  18450  cnheibor  18453  phtpycc  18489  elovolm  18834  ovolgelb  18839  ovolicc1  18875  ovolicc  18882  ioorval  18929  uniioombllem6  18943  dyadmax  18953  dyadmbllem  18954  dyadmbl  18955  opnmbllem  18956  i1fadd  19050  i1fmul  19051  itg1addlem3  19053  i1fmulc  19058  itg2l  19084  itg2leub  19089  limcmpt  19233  limcco  19243  dvcobr  19295  evlslem3  19398  deg1ldg  19478  ig1pval  19558  elply  19577  elply2  19578  coeval  19605  coe1termlem  19639  coe1term  19640  quotval  19672  plydivlem4  19676  plydivex  19677  vieta1  19692  aannenlem2  19709  aalioulem2  19713  abelthlem9  19816  logtayllem  20006  logtayl  20007  isosctrlem2  20119  atantayl2  20234  leibpilem2  20237  rlimcnp2  20261  efrlim  20264  dvdsmulf1o  20434  perfectlem2  20469  lgsfval  20540  lgsval2lem  20545  lgsdchrval  20586  2sqlem2  20603  2sqlem8  20611  2sqlem9  20612  2sqlem11  20614  dchrisum0flblem1  20657  padicval  20766  padicabv  20779  ostth1  20782  gxval  20925  gxdi  20963  ismgm  20987  nvz  21235  nmosetn0  21343  nmoolb  21349  nmoubi  21350  nmlno0lem  21371  nmlno0i  21372  hvsubeq0  21647  hvaddcan  21649  normsub0  21715  norm1exi  21829  pjhval  21976  omlsii  21982  omlsi  21983  pjoml  22015  h1de2ci  22135  spansneleq  22149  h1datomi  22160  h1datom  22161  spansncv  22232  5oalem6  22238  pj11  22293  nmopsetn0  22445  nmfnsetn0  22458  nmoplb  22487  nmopub  22488  nmfnlb  22504  nmfnleub  22505  nmlnop0iALT  22575  nmlnop0  22578  lnopeq  22589  nmopun  22594  nmcexi  22606  branmfn  22685  pjnmopi  22728  pj3i  22788  atss  22926  atom1d  22933  chirred  22975  cdj3lem2  23015  elabreximd  23039  difeq  23128  fmptcof2  23229  xrge0iifcnv  23315  xrge0iifcv  23316  xrge0iifhom  23319  xrge0tmdALT  23327  xrge0tmd  23328  disji2f  23354  disjif2  23358  esumc  23430  esumpcvgval  23446  dya2iocseg  23579  probun  23622  sconpi1  23770  cvmlift3lem2  23851  ghomf1olem  24001  relexp0  24025  relexpsucr  24026  relexpsucl  24028  rtrclreclem.trans  24043  br8  24113  br6  24114  br4  24115  rdgprc0  24150  dfrdg2  24152  sltval2  24310  sltintdifex  24317  sltres  24318  dfbigcup2  24439  elfuns  24454  elsingles  24457  dfiota3  24462  brimageg  24466  brdomaing  24474  brrangeg  24475  funpartfun  24481  dfrdg4  24488  tfrqfree  24489  elaltxp  24509  axpaschlem  24568  axlowdimlem15  24584  axlowdim  24589  funtransport  24654  fvtransport  24655  brsegle  24731  funray  24763  fvray  24764  funline  24765  fvline  24767  ellines  24775  linethru  24776  rankeq1o  24801  copsexgb  24966  elo  25041  eloi  25086  repcpwti  25161  cbcpcp  25162  ismxl2  25267  prodeq1  25306  grpodrcan  25375  intopcoaconlem3b  25538  intopcoaconlem3  25539  fisub  25554  iint  25612  trnij  25615  ismonb2  25812  cmpmon  25815  isepib2  25822  vtarsuelt  25895  isconc1  26006  isconc2  26007  isconc3  26008  cndpv  26049  pgapspf  26052  sgplpte21b  26134  pdiveql  26168  bhp2a  26176  subtr  26224  subtr2  26225  nn0prpw  26239  unirep  26349  f1opr  26391  sdclem2  26452  sdclem1  26453  sdc  26454  fdc  26455  isbnd  26504  heibor1lem  26533  heiborlem4  26538  heiborlem6  26540  heiborlem10  26544  maxidlmax  26668  prnc  26692  isfldidl  26693  dmnnzd  26700  elrfi  26769  nacsfg  26780  mzpcompact2lem  26829  eldioph2b  26842  eldioph3  26845  eldiophss  26854  diophrex  26855  elnn0rabdioph  26884  rencldnfilem  26903  elpell1qr  26932  elpell14qr  26934  elpell1234qr  26936  divalgmodcl  27080  jm2.27  27101  rmydioph  27107  expdiophlem2  27115  wepwsolem  27138  aomclem6  27156  uvcvval  27235  ellspd  27254  lnr2i  27320  lpirlnr  27321  hbtlem2  27328  hbtlem4  27330  hbtlem5  27332  rngunsnply  27378  flcidc  27379  psgneu  27429  psgnval  27430  psgnvali  27431  psgnvalii  27432  pm13.192  27610  refsum2cnlem1  27708  stoweidlem46  27795  afv0fv0  28012  afvfv0bi  28015  afvelrnb  28025  afvelrnb0  28026  frgra3vlem1  28178  3vfriswmgralem  28182  sgnval  28245  equncomVD  28644  csbingVD  28660  csbsngVD  28669  csbfv12gALTVD  28675  relopabVD  28677  bnj1468  28878  lshpdisj  29177  lsat0cv  29223  lcvexchlem4  29227  lcvexchlem5  29228  lshpkrlem1  29300  lshpkrlem2  29301  lshpkrlem3  29302  lshpkrcl  29306  islshpkrN  29310  atnle  29507  glbconxN  29567  isline  29928  ispointN  29931  pmapglbx  29958  ispsubcl2N  30136  lhp2atnle  30222  cdleme43fsv1snlem  30609  cdleme40v  30658  cdlemkid5  31124  cdlemkid  31125  dvhb1dimN  31175  dib1dim  31355  dicopelval  31367  dicelval1sta  31377  diclspsn  31384  dihvalcqpre  31425  dihglblem2aN  31483  dihglblem2N  31484  dih1dimatlem  31519  dihpN  31526  dochfl1  31666  lcfl7N  31691  lcf1o  31741  hvmapvalvalN  31951  hdmapval2lem  32024
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator