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

Theorem eqeq1 2444
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 2432 . . . . . 6  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
21biimpi 188 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1775 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
43bibi1d 312 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  <->  x  e.  C )  <->  ( x  e.  B  <->  x  e.  C
) ) )
54albidv 1636 . 2  |-  ( A  =  B  ->  ( A. x ( x  e.  A  <->  x  e.  C
)  <->  A. x ( x  e.  B  <->  x  e.  C ) ) )
6 dfcleq 2432 . 2  |-  ( A  =  C  <->  A. x
( x  e.  A  <->  x  e.  C ) )
7 dfcleq 2432 . 2  |-  ( B  =  C  <->  A. x
( x  e.  B  <->  x  e.  C ) )
85, 6, 73bitr4g 281 1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wal 1550    = wceq 1653    e. wcel 1726
This theorem is referenced by:  eqeq1i  2445  eqeq1d  2446  eqeq2  2447  eqeq12  2450  eqtr  2455  eqsb3lem  2538  clelab  2558  neeq1  2611  pm13.18  2678  issetf  2963  sbhypf  3003  vtoclgft  3004  eqvincf  3066  pm13.183  3078  eueq  3108  mob  3118  euind  3123  reuind  3139  eqsbc3  3202  csbhypf  3288  uniiunlem  3433  snjust  3821  elprg  3833  elsncg  3838  rabrsn  3876  sneqrg  3970  preq12bg  3979  intab  4082  uniintsn  4089  dfiin2g  4126  disji2  4201  disjprg  4210  opthg  4438  copsexg  4444  euotd  4459  elopab  4464  solin  4528  snnex  4715  uniuni  4718  eusv1  4719  reusv2lem2  4727  reusv3  4733  reusv6OLD  4736  orduninsuc  4825  elxpi  4896  opbrop  4957  relop  5025  ideqg  5026  elrnmpt  5119  elrnmpt1  5121  elrnmptg  5122  somin1  5272  cnveqb  5328  relcoi1  5400  funopg  5487  funcnvuni  5520  fun11iun  5697  fvelrnb  5776  fvmptg  5806  fndmin  5839  eldmrexrn  5878  foelrn  5890  foco2  5891  fmptco  5903  eufnfv  5974  elabrex  5987  abrexco  5988  f1veqaeq  6007  isosolem  6069  f1oiso  6073  f1oweALT  6076  oprabid  6107  mpt2fun  6174  elrnmpt2g  6184  elrnmpt2  6185  ralrnmpt2  6186  ov3  6212  ov6g  6213  ovelrn  6224  caovcang  6250  caovcan  6253  eloprabi  6415  frxp  6458  dftpos4  6500  opiota  6537  eusvobj2  6584  riotasvd  6594  riotasvdOLD  6595  tz7.44-2  6667  tz7.44-3  6668  oev  6760  oalimcl  6805  omlimcl  6823  odi  6824  omeu  6830  oeeui  6847  nneob  6897  omopth  6903  elqsg  6958  qsdisj  6983  qsel  6985  brecop  6999  eroveu  7001  erovlem  7002  th3qlem1  7012  th3q  7015  elixpsn  7103  ixpsnf1o  7104  boxcutc  7107  2dom  7181  fundmen  7182  xpf1o  7271  nneneq  7292  fofinf1o  7389  elfi  7420  elfiun  7437  dffi3  7438  brwdom  7537  brwdom3  7552  unwdomg  7554  xpwdomg  7555  noinfep  7616  cantnfp1lem1  7636  cantnfp1lem3  7638  cantnfp1  7639  cantnflem1  7647  scott0  7812  carden2a  7855  cardiun  7871  pm54.43lem  7888  alephval3  7993  dfac5lem3  8008  dfac5lem4  8009  dfac2  8013  kmlem9  8040  kmlem12  8043  cardcf  8134  cfeq0  8138  cfsuc  8139  cff1  8140  cflim2  8145  cfss  8147  isfin5  8181  fin1a2lem11  8292  fin1a2lem13  8294  brdom7disj  8411  brdom6disj  8412  canthp1lem2  8530  canthp1  8531  tskuni  8660  gruina  8695  genpv  8878  genpelv  8879  ltsosr  8971  ltresr  9017  axcnre  9041  axpre-lttri  9042  ltordlem  9554  ltord1  9555  fimaxre3  9959  supmul1  9975  supmullem1  9976  supmullem2  9977  supmul  9978  creur  9996  creui  9997  nn1m1nn  10022  elz  10286  nn0ind-raph  10372  xnegeq  10795  xmullem2  10846  xmulasslem  10866  fseqsupubi  11319  sqeqor  11497  nn0opth2  11567  hash1snb  11683  hash2prde  11690  brfi1uzind  11717  ccatco  11806  shftfval  11887  sqrlem6  12055  summo  12513  fsum  12516  fsumtscopo  12583  infcvgaux1i  12638  infcvgaux2i  12639  mertenslem1  12663  mertenslem2  12664  mertens  12665  ruclem12  12842  divalg  12925  ndvdssub  12929  bitsinvp1  12963  sadcp1  12969  smupp1  12994  gcdval  13010  bezoutlem1  13040  bezoutlem3  13042  bezoutlem4  13043  bezout  13044  dvdsprime  13094  nprm  13095  dvdsprm  13101  coprm  13102  qnumval  13131  qdenval  13132  pcval  13220  pceu  13222  pczpre  13223  pcdiv  13228  4sqlem2  13319  4sqlem4  13322  4sqlem12  13326  4sq  13334  vdwapval  13343  vdwapun  13344  vdwlem6  13356  acsfn  13886  posi  14409  gsumval2a  14784  ghmf1  15036  conjnmzb  15042  orbsta  15092  odval  15174  dfod2  15202  submod  15205  isslw  15244  sylow2alem1  15253  sylow3lem2  15264  lsmelvalm  15287  lsmdisj2  15316  efgrelexlemb  15384  frgpup3lem  15411  cyggeninv  15495  cygabl  15502  gsumval3eu  15515  gsumval3  15516  dprddisj2  15599  dpjrid  15622  pgpfac1lem3  15637  abveq0  15916  abvtrivd  15930  lss1d  16041  lspsn  16080  lspsnel  16081  lspprel  16168  rrgeq0i  16351  domneq0  16359  psrlidm  16469  psrridm  16470  mvrval2  16488  mvrf1  16491  mplmonmul  16529  coe1tm  16667  coe1tmfv2  16669  xrsdsreval  16745  prmirredlem  16775  znf1o  16834  znfld  16843  znunit  16846  cygznlem3  16852  ipeq0  16871  obsip  16950  eltopspOLD  16985  istpsOLD  16987  istopon  16992  fctop  17070  cctop  17072  ppttop  17073  pptbas  17074  epttop  17075  t0sep  17390  t1sep2  17435  cmpsublem  17464  cmpsub  17465  txuni2  17599  elpt  17606  ptbasfi  17615  xkoopn  17623  ptpjopn  17646  ptclsg  17649  dfac14lem  17651  ptcnp  17656  ptrescn  17673  tx1stc  17684  qtopeu  17750  kqt0lem  17770  isr0  17771  hauspwpwf1  18021  xmeteq0  18370  imasf1oxmet  18407  comet  18545  stdbdxmet  18547  met2ndci  18554  prdsxmslem2  18561  nrmmetd  18624  tngngp  18697  xrsxmet  18842  iccpnfcnv  18971  iccpnfhmeo  18972  oprpiece1res2  18979  cnheibor  18982  phtpycc  19018  elovolm  19373  ovolgelb  19378  ovolicc1  19414  ovolicc  19421  ioorval  19468  uniioombllem6  19482  dyadmax  19492  dyadmbl  19494  i1fadd  19589  i1fmul  19590  itg1addlem3  19592  i1fmulc  19597  itg2l  19623  itg2leub  19628  limcmpt  19772  limcco  19782  dvcobr  19834  evlslem3  19937  deg1ldg  20017  ig1pval  20097  elply  20116  elply2  20117  coeval  20144  coe1termlem  20178  coe1term  20179  quotval  20211  plydivlem4  20215  plydivex  20216  vieta1  20231  aannenlem2  20248  aalioulem2  20252  abelthlem9  20358  logtayllem  20552  logtayl  20553  isosctrlem2  20665  atantayl2  20780  leibpilem2  20783  rlimcnp2  20807  efrlim  20810  dvdsmulf1o  20981  perfectlem2  21016  lgsfval  21087  lgsval2lem  21092  lgsdchrval  21133  2sqlem2  21150  2sqlem8  21158  2sqlem9  21159  2sqlem11  21161  dchrisum0flblem1  21204  padicval  21313  padicabv  21326  ostth1  21329  cusgrafilem2  21491  cusgrafi  21493  wlkntrllem3  21563  fargshiftf1  21626  fargshiftfo  21627  constr3trllem2  21640  vdusgraval  21680  gxval  21848  gxdi  21886  ismgm  21910  nvz  22160  nmosetn0  22268  nmoolb  22274  nmoubi  22275  nmlno0lem  22296  nmlno0i  22297  hvsubeq0  22572  hvaddcan  22574  normsub0  22640  norm1exi  22754  pjhval  22901  omlsii  22907  omlsi  22908  pjoml  22940  h1de2ci  23060  spansneleq  23074  h1datomi  23085  h1datom  23086  spansncv  23157  5oalem6  23163  pj11  23218  nmopsetn0  23370  nmfnsetn0  23383  nmoplb  23412  nmopub  23413  nmfnlb  23429  nmfnleub  23430  nmlnop0iALT  23500  nmlnop0  23503  lnopeq  23514  nmopun  23519  nmcexi  23531  branmfn  23610  pjnmopi  23653  pj3i  23713  atss  23851  atom1d  23858  chirred  23900  cdj3lem2  23940  elabreximd  23993  disjxpin  24030  fmptcof2  24078  xrge0iifcnv  24321  xrge0iifcv  24322  xrge0iifhom  24325  xrge0tmdOLD  24333  xrge0tmd  24334  esumc  24448  sconpi1  24928  cvmlift3lem2  25009  ghomf1olem  25107  relexp0  25131  relexpsucr  25132  relexpsucl  25134  rtrclreclem.trans  25148  prodmo  25264  fprod  25269  br8  25381  br6  25382  br4  25383  rdgprc0  25423  dfrdg2  25425  sltval2  25613  sltintdifex  25620  sltres  25621  dfbigcup2  25746  elsingles  25765  dfiota3  25770  brimageg  25774  brdomaing  25782  brrangeg  25783  dfrdg4  25797  tfrqfree  25798  elaltxp  25822  axpaschlem  25881  axlowdimlem15  25897  axlowdim  25902  funtransport  25967  fvtransport  25968  brsegle  26044  funray  26076  fvray  26077  funline  26078  fvline  26080  ellines  26088  linethru  26089  rankeq1o  26114  supaddc  26239  supadd  26240  mblfinlem1  26245  mblfinlem2  26246  mblfinlem3  26247  mblfinlem4  26248  ismblfin  26249  itg2addnclem  26258  itg2addnclem3  26260  itg2addnc  26261  ftc1anc  26290  subtr  26319  subtr2  26320  nn0prpw  26328  unirep  26416  f1opr  26428  sdclem2  26448  sdclem1  26449  sdc  26450  fdc  26451  isbnd  26491  heibor1lem  26520  heiborlem4  26525  heiborlem6  26527  heiborlem10  26531  maxidlmax  26655  prnc  26679  isfldidl  26680  dmnnzd  26687  elrfi  26750  nacsfg  26761  mzpcompact2lem  26810  eldioph2b  26823  eldioph3  26826  eldiophss  26835  diophrex  26836  elnn0rabdioph  26865  rencldnfilem  26883  elpell1qr  26912  elpell14qr  26914  elpell1234qr  26916  divalgmodcl  27060  jm2.27  27081  rmydioph  27087  expdiophlem2  27095  wepwsolem  27118  aomclem6  27136  uvcvval  27214  ellspd  27233  lnr2i  27299  lpirlnr  27300  hbtlem2  27307  hbtlem4  27309  hbtlem5  27311  rngunsnply  27357  flcidc  27358  psgneu  27408  psgnval  27409  psgnvali  27410  psgnvalii  27411  pm13.192  27589  refsum2cnlem1  27686  stoweidlem46  27773  afv0fv0  27991  afvfv0bi  27994  afvelrnb  28005  afvelrnb0  28006  otiunsndisj  28069  otiunsndisjX  28070  f0rn0  28081  oprabv  28091  2ffzoeq  28151  euhash1  28178  reumodprminv  28249  cshwssizesame  28310  2wlkeq  28329  wwlkn0  28359  wlklniswwlkn1  28369  frgra3vlem1  28452  3vfriswmgralem  28456  frgrancvvdeqlem4  28484  2spotiundisj  28513  usgreghash2spotv  28517  frgregordn0  28521  sgnval  28580  equncomVD  29042  csbingVD  29058  csbsngVD  29067  csbfv12gALTVD  29073  relopabVD  29075  bnj1468  29279  lshpdisj  29847  lsat0cv  29893  lcvexchlem4  29897  lcvexchlem5  29898  lshpkrlem1  29970  lshpkrlem2  29971  lshpkrlem3  29972  lshpkrcl  29976  islshpkrN  29980  atnle  30177  glbconxN  30237  isline  30598  ispointN  30601  pmapglbx  30628  ispsubcl2N  30806  lhp2atnle  30892  cdleme43fsv1snlem  31279  cdleme40v  31328  cdlemkid5  31794  cdlemkid  31795  dvhb1dimN  31845  dib1dim  32025  dicopelval  32037  dicelval1sta  32047  diclspsn  32054  dihvalcqpre  32095  dihglblem2aN  32153  dihglblem2N  32154  dih1dimatlem  32189  dihpN  32196  dochfl1  32336  lcfl7N  32361  lcf1o  32411  hvmapvalvalN  32621  hdmapval2lem  32694
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2431
  Copyright terms: Public domain W3C validator