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

Theorem eqeq1 2441
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 2429 . . . . . 6  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
21biimpi 187 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1774 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
43bibi1d 311 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  <->  x  e.  C )  <->  ( x  e.  B  <->  x  e.  C
) ) )
54albidv 1635 . 2  |-  ( A  =  B  ->  ( A. x ( x  e.  A  <->  x  e.  C
)  <->  A. x ( x  e.  B  <->  x  e.  C ) ) )
6 dfcleq 2429 . 2  |-  ( A  =  C  <->  A. x
( x  e.  A  <->  x  e.  C ) )
7 dfcleq 2429 . 2  |-  ( B  =  C  <->  A. x
( x  e.  B  <->  x  e.  C ) )
85, 6, 73bitr4g 280 1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1549    = wceq 1652    e. wcel 1725
This theorem is referenced by:  eqeq1i  2442  eqeq1d  2443  eqeq2  2444  eqeq12  2447  eqtr  2452  eqsb3lem  2535  clelab  2555  neeq1  2606  pm13.18  2670  issetf  2953  sbhypf  2993  vtoclgft  2994  eqvincf  3056  pm13.183  3068  eueq  3098  mob  3108  euind  3113  reuind  3129  eqsbc3  3192  csbhypf  3278  uniiunlem  3423  snjust  3811  elprg  3823  elsncg  3828  rabrsn  3866  sneqrg  3960  preq12bg  3969  intab  4072  uniintsn  4079  dfiin2g  4116  disji2  4191  disjprg  4200  opthg  4428  copsexg  4434  euotd  4449  elopab  4454  solin  4518  snnex  4704  uniuni  4707  eusv1  4708  reusv2lem2  4716  reusv3  4722  reusv6OLD  4725  orduninsuc  4814  elxpi  4885  opbrop  4946  relop  5014  ideqg  5015  elrnmpt  5108  elrnmpt1  5110  elrnmptg  5111  somin1  5261  cnveqb  5317  relcoi1  5389  funopg  5476  funcnvuni  5509  fun11iun  5686  fvelrnb  5765  fvmptg  5795  fndmin  5828  eldmrexrn  5867  foelrn  5879  foco2  5880  fmptco  5892  eufnfv  5963  elabrex  5976  abrexco  5977  f1veqaeq  5996  isosolem  6058  f1oiso  6062  f1oweALT  6065  oprabid  6096  mpt2fun  6163  elrnmpt2g  6173  elrnmpt2  6174  ralrnmpt2  6175  ov3  6201  ov6g  6202  ovelrn  6213  caovcang  6239  caovcan  6242  eloprabi  6404  frxp  6447  dftpos4  6489  opiota  6526  eusvobj2  6573  riotasvd  6583  riotasvdOLD  6584  tz7.44-2  6656  tz7.44-3  6657  oev  6749  oalimcl  6794  omlimcl  6812  odi  6813  omeu  6819  oeeui  6836  nneob  6886  omopth  6892  elqsg  6947  qsdisj  6972  qsel  6974  brecop  6988  eroveu  6990  erovlem  6991  th3qlem1  7001  th3q  7004  elixpsn  7092  ixpsnf1o  7093  boxcutc  7096  2dom  7170  fundmen  7171  xpf1o  7260  nneneq  7281  fofinf1o  7378  elfi  7409  elfiun  7426  dffi3  7427  brwdom  7524  brwdom3  7539  unwdomg  7541  xpwdomg  7542  noinfep  7603  cantnfp1lem1  7623  cantnfp1lem3  7625  cantnfp1  7626  cantnflem1  7634  scott0  7799  carden2a  7842  cardiun  7858  pm54.43lem  7875  alephval3  7980  dfac5lem3  7995  dfac5lem4  7996  dfac2  8000  kmlem9  8027  kmlem12  8030  cardcf  8121  cfeq0  8125  cfsuc  8126  cff1  8127  cflim2  8132  cfss  8134  isfin5  8168  fin1a2lem11  8279  fin1a2lem13  8281  brdom7disj  8398  brdom6disj  8399  canthp1lem2  8517  canthp1  8518  tskuni  8647  gruina  8682  genpv  8865  genpelv  8866  ltsosr  8958  ltresr  9004  axcnre  9028  axpre-lttri  9029  ltordlem  9541  ltord1  9542  fimaxre3  9946  supmul1  9962  supmullem1  9963  supmullem2  9964  supmul  9965  creur  9983  creui  9984  nn1m1nn  10009  elz  10273  nn0ind-raph  10359  xnegeq  10782  xmullem2  10833  xmulasslem  10853  fseqsupubi  11305  sqeqor  11483  nn0opth2  11553  hash1snb  11669  hash2prde  11676  brfi1uzind  11703  ccatco  11792  shftfval  11873  sqrlem6  12041  summo  12499  fsum  12502  fsumtscopo  12569  infcvgaux1i  12624  infcvgaux2i  12625  mertenslem1  12649  mertenslem2  12650  mertens  12651  ruclem12  12828  divalg  12911  ndvdssub  12915  bitsinvp1  12949  sadcp1  12955  smupp1  12980  gcdval  12996  bezoutlem1  13026  bezoutlem3  13028  bezoutlem4  13029  bezout  13030  dvdsprime  13080  nprm  13081  dvdsprm  13087  coprm  13088  qnumval  13117  qdenval  13118  pcval  13206  pceu  13208  pczpre  13209  pcdiv  13214  4sqlem2  13305  4sqlem4  13308  4sqlem12  13312  4sq  13320  vdwapval  13329  vdwapun  13330  vdwlem6  13342  acsfn  13872  posi  14395  gsumval2a  14770  ghmf1  15022  conjnmzb  15028  orbsta  15078  odval  15160  dfod2  15188  submod  15191  isslw  15230  sylow2alem1  15239  sylow3lem2  15250  lsmelvalm  15273  lsmdisj2  15302  efgrelexlemb  15370  frgpup3lem  15397  cyggeninv  15481  cygabl  15488  gsumval3eu  15501  gsumval3  15502  dprddisj2  15585  dpjrid  15608  pgpfac1lem3  15623  abveq0  15902  abvtrivd  15916  lss1d  16027  lspsn  16066  lspsnel  16067  lspprel  16154  rrgeq0i  16337  domneq0  16345  psrlidm  16455  psrridm  16456  mvrval2  16474  mvrf1  16477  mplmonmul  16515  coe1tm  16653  coe1tmfv2  16655  xrsdsreval  16731  prmirredlem  16761  znf1o  16820  znfld  16829  znunit  16832  cygznlem3  16838  ipeq0  16857  obsip  16936  eltopspOLD  16971  istpsOLD  16973  istopon  16978  fctop  17056  cctop  17058  ppttop  17059  pptbas  17060  epttop  17061  t0sep  17376  t1sep2  17421  cmpsublem  17450  cmpsub  17451  txuni2  17585  elpt  17592  ptbasfi  17601  xkoopn  17609  ptpjopn  17632  ptclsg  17635  dfac14lem  17637  ptcnp  17642  ptrescn  17659  tx1stc  17670  qtopeu  17736  kqt0lem  17756  isr0  17757  hauspwpwf1  18007  xmeteq0  18356  imasf1oxmet  18393  comet  18531  stdbdxmet  18533  met2ndci  18540  prdsxmslem2  18547  nrmmetd  18610  tngngp  18683  xrsxmet  18828  iccpnfcnv  18957  iccpnfhmeo  18958  oprpiece1res2  18965  cnheibor  18968  phtpycc  19004  elovolm  19359  ovolgelb  19364  ovolicc1  19400  ovolicc  19407  ioorval  19454  uniioombllem6  19468  dyadmax  19478  dyadmbl  19480  i1fadd  19575  i1fmul  19576  itg1addlem3  19578  i1fmulc  19583  itg2l  19609  itg2leub  19614  limcmpt  19758  limcco  19768  dvcobr  19820  evlslem3  19923  deg1ldg  20003  ig1pval  20083  elply  20102  elply2  20103  coeval  20130  coe1termlem  20164  coe1term  20165  quotval  20197  plydivlem4  20201  plydivex  20202  vieta1  20217  aannenlem2  20234  aalioulem2  20238  abelthlem9  20344  logtayllem  20538  logtayl  20539  isosctrlem2  20651  atantayl2  20766  leibpilem2  20769  rlimcnp2  20793  efrlim  20796  dvdsmulf1o  20967  perfectlem2  21002  lgsfval  21073  lgsval2lem  21078  lgsdchrval  21119  2sqlem2  21136  2sqlem8  21144  2sqlem9  21145  2sqlem11  21147  dchrisum0flblem1  21190  padicval  21299  padicabv  21312  ostth1  21315  cusgrafilem2  21477  cusgrafi  21479  wlkntrllem3  21549  fargshiftf1  21612  fargshiftfo  21613  constr3trllem2  21626  vdusgraval  21666  gxval  21834  gxdi  21872  ismgm  21896  nvz  22146  nmosetn0  22254  nmoolb  22260  nmoubi  22261  nmlno0lem  22282  nmlno0i  22283  hvsubeq0  22558  hvaddcan  22560  normsub0  22626  norm1exi  22740  pjhval  22887  omlsii  22893  omlsi  22894  pjoml  22926  h1de2ci  23046  spansneleq  23060  h1datomi  23071  h1datom  23072  spansncv  23143  5oalem6  23149  pj11  23204  nmopsetn0  23356  nmfnsetn0  23369  nmoplb  23398  nmopub  23399  nmfnlb  23415  nmfnleub  23416  nmlnop0iALT  23486  nmlnop0  23489  lnopeq  23500  nmopun  23505  nmcexi  23517  branmfn  23596  pjnmopi  23639  pj3i  23699  atss  23837  atom1d  23844  chirred  23886  cdj3lem2  23926  elabreximd  23979  disjxpin  24016  fmptcof2  24064  xrge0iifcnv  24307  xrge0iifcv  24308  xrge0iifhom  24311  xrge0tmdOLD  24319  xrge0tmd  24320  esumc  24434  sconpi1  24914  cvmlift3lem2  24995  ghomf1olem  25093  relexp0  25117  relexpsucr  25118  relexpsucl  25120  rtrclreclem.trans  25134  prodmo  25251  fprod  25256  br8  25368  br6  25369  br4  25370  rdgprc0  25405  dfrdg2  25407  sltval2  25565  sltintdifex  25572  sltres  25573  dfbigcup2  25694  elfuns  25710  elsingles  25713  dfiota3  25718  brimageg  25722  brdomaing  25730  brrangeg  25731  dfrdg4  25745  tfrqfree  25746  elaltxp  25768  axpaschlem  25827  axlowdimlem15  25843  axlowdim  25848  funtransport  25913  fvtransport  25914  brsegle  25990  funray  26022  fvray  26023  funline  26024  fvline  26026  ellines  26034  linethru  26035  rankeq1o  26060  supaddc  26184  supadd  26185  mblfinlem  26190  mblfinlem2  26191  mblfinlem3  26192  ismblfin  26193  itg2addnclem  26202  itg2addnclem3  26204  itg2addnc  26205  subtr  26254  subtr2  26255  nn0prpw  26263  unirep  26351  f1opr  26363  sdclem2  26383  sdclem1  26384  sdc  26385  fdc  26386  isbnd  26426  heibor1lem  26455  heiborlem4  26460  heiborlem6  26462  heiborlem10  26466  maxidlmax  26590  prnc  26614  isfldidl  26615  dmnnzd  26622  elrfi  26685  nacsfg  26696  mzpcompact2lem  26745  eldioph2b  26758  eldioph3  26761  eldiophss  26770  diophrex  26771  elnn0rabdioph  26800  rencldnfilem  26818  elpell1qr  26847  elpell14qr  26849  elpell1234qr  26851  divalgmodcl  26995  jm2.27  27016  rmydioph  27022  expdiophlem2  27030  wepwsolem  27053  aomclem6  27071  uvcvval  27150  ellspd  27169  lnr2i  27235  lpirlnr  27236  hbtlem2  27243  hbtlem4  27245  hbtlem5  27247  rngunsnply  27293  flcidc  27294  psgneu  27344  psgnval  27345  psgnvali  27346  psgnvalii  27347  pm13.192  27525  refsum2cnlem1  27622  stoweidlem46  27709  afv0fv0  27927  afvfv0bi  27930  afvelrnb  27941  afvelrnb0  27942  otiunsndisj  28002  otiunsndisjX  28003  euhash1  28071  swrdccat3b  28106  reumodprminv  28111  shwrdssizesame  28171  frgra3vlem1  28248  3vfriswmgralem  28252  frgrancvvdeqlem4  28280  2spotiundisj  28309  usgreghash2spotv  28313  frgregordn0  28317  sgnval  28376  equncomVD  28834  csbingVD  28850  csbsngVD  28859  csbfv12gALTVD  28865  relopabVD  28867  bnj1468  29071  lshpdisj  29624  lsat0cv  29670  lcvexchlem4  29674  lcvexchlem5  29675  lshpkrlem1  29747  lshpkrlem2  29748  lshpkrlem3  29749  lshpkrcl  29753  islshpkrN  29757  atnle  29954  glbconxN  30014  isline  30375  ispointN  30378  pmapglbx  30405  ispsubcl2N  30583  lhp2atnle  30669  cdleme43fsv1snlem  31056  cdleme40v  31105  cdlemkid5  31571  cdlemkid  31572  dvhb1dimN  31622  dib1dim  31802  dicopelval  31814  dicelval1sta  31824  diclspsn  31831  dihvalcqpre  31872  dihglblem2aN  31930  dihglblem2N  31931  dih1dimatlem  31966  dihpN  31973  dochfl1  32113  lcfl7N  32138  lcf1o  32188  hvmapvalvalN  32398  hdmapval2lem  32471
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator