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

Theorem eqeq1 2410
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 2398 . . . . . 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 1770 . . . 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 1632 . 2  |-  ( A  =  B  ->  ( A. x ( x  e.  A  <->  x  e.  C
)  <->  A. x ( x  e.  B  <->  x  e.  C ) ) )
6 dfcleq 2398 . 2  |-  ( A  =  C  <->  A. x
( x  e.  A  <->  x  e.  C ) )
7 dfcleq 2398 . 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 1546    = wceq 1649    e. wcel 1721
This theorem is referenced by:  eqeq1i  2411  eqeq1d  2412  eqeq2  2413  eqeq12  2416  eqtr  2421  eqsb3lem  2504  clelab  2524  neeq1  2575  pm13.18  2639  issetf  2921  sbhypf  2961  vtoclgft  2962  eqvincf  3024  pm13.183  3036  eueq  3066  mob  3076  euind  3081  reuind  3097  eqsbc3  3160  csbhypf  3246  uniiunlem  3391  snjust  3779  elprg  3791  elsncg  3796  rabrsn  3834  sneqrg  3928  preq12bg  3937  intab  4040  uniintsn  4047  dfiin2g  4084  disji2  4159  disjprg  4168  opthg  4396  copsexg  4402  euotd  4417  elopab  4422  solin  4486  snnex  4672  uniuni  4675  eusv1  4676  reusv2lem2  4684  reusv3  4690  reusv6OLD  4693  orduninsuc  4782  elxpi  4853  opbrop  4914  relop  4982  ideqg  4983  elrnmpt  5076  elrnmpt1  5078  elrnmptg  5079  somin1  5229  cnveqb  5285  relcoi1  5357  funopg  5444  funcnvuni  5477  fun11iun  5654  fvelrnb  5733  fvmptg  5763  fndmin  5796  eldmrexrn  5835  foelrn  5847  foco2  5848  fmptco  5860  eufnfv  5931  elabrex  5944  abrexco  5945  f1veqaeq  5964  isosolem  6026  f1oiso  6030  f1oweALT  6033  oprabid  6064  mpt2fun  6131  elrnmpt2g  6141  elrnmpt2  6142  ralrnmpt2  6143  ov3  6169  ov6g  6170  ovelrn  6181  caovcang  6207  caovcan  6210  eloprabi  6372  frxp  6415  dftpos4  6457  opiota  6494  eusvobj2  6541  riotasvd  6551  riotasvdOLD  6552  tz7.44-2  6624  tz7.44-3  6625  oev  6717  oalimcl  6762  omlimcl  6780  odi  6781  omeu  6787  oeeui  6804  nneob  6854  omopth  6860  elqsg  6915  qsdisj  6940  qsel  6942  brecop  6956  eroveu  6958  erovlem  6959  th3qlem1  6969  th3q  6972  elixpsn  7060  ixpsnf1o  7061  boxcutc  7064  2dom  7138  fundmen  7139  xpf1o  7228  nneneq  7249  fofinf1o  7346  elfi  7376  elfiun  7393  dffi3  7394  brwdom  7491  brwdom3  7506  unwdomg  7508  xpwdomg  7509  noinfep  7570  cantnfp1lem1  7590  cantnfp1lem3  7592  cantnfp1  7593  cantnflem1  7601  scott0  7766  carden2a  7809  cardiun  7825  pm54.43lem  7842  alephval3  7947  dfac5lem3  7962  dfac5lem4  7963  dfac2  7967  kmlem9  7994  kmlem12  7997  cardcf  8088  cfeq0  8092  cfsuc  8093  cff1  8094  cflim2  8099  cfss  8101  isfin5  8135  fin1a2lem11  8246  fin1a2lem13  8248  brdom7disj  8365  brdom6disj  8366  canthp1lem2  8484  canthp1  8485  tskuni  8614  gruina  8649  genpv  8832  genpelv  8833  ltsosr  8925  ltresr  8971  axcnre  8995  axpre-lttri  8996  ltordlem  9508  ltord1  9509  fimaxre3  9913  supmul1  9929  supmullem1  9930  supmullem2  9931  supmul  9932  creur  9950  creui  9951  nn1m1nn  9976  elz  10240  nn0ind-raph  10326  xnegeq  10749  xmullem2  10800  xmulasslem  10820  fseqsupubi  11272  sqeqor  11450  nn0opth2  11520  hash1snb  11636  hash2prde  11643  brfi1uzind  11670  ccatco  11759  shftfval  11840  sqrlem6  12008  summo  12466  fsum  12469  fsumtscopo  12536  infcvgaux1i  12591  infcvgaux2i  12592  mertenslem1  12616  mertenslem2  12617  mertens  12618  ruclem12  12795  divalg  12878  ndvdssub  12882  bitsinvp1  12916  sadcp1  12922  smupp1  12947  gcdval  12963  bezoutlem1  12993  bezoutlem3  12995  bezoutlem4  12996  bezout  12997  dvdsprime  13047  nprm  13048  dvdsprm  13054  coprm  13055  qnumval  13084  qdenval  13085  pcval  13173  pceu  13175  pczpre  13176  pcdiv  13181  4sqlem2  13272  4sqlem4  13275  4sqlem12  13279  4sq  13287  vdwapval  13296  vdwapun  13297  vdwlem6  13309  acsfn  13839  posi  14362  gsumval2a  14737  ghmf1  14989  conjnmzb  14995  orbsta  15045  odval  15127  dfod2  15155  submod  15158  isslw  15197  sylow2alem1  15206  sylow3lem2  15217  lsmelvalm  15240  lsmdisj2  15269  efgrelexlemb  15337  frgpup3lem  15364  cyggeninv  15448  cygabl  15455  gsumval3eu  15468  gsumval3  15469  dprddisj2  15552  dpjrid  15575  pgpfac1lem3  15590  abveq0  15869  abvtrivd  15883  lss1d  15994  lspsn  16033  lspsnel  16034  lspprel  16121  rrgeq0i  16304  domneq0  16312  psrlidm  16422  psrridm  16423  mvrval2  16441  mvrf1  16444  mplmonmul  16482  coe1tm  16620  coe1tmfv2  16622  xrsdsreval  16698  prmirredlem  16728  znf1o  16787  znfld  16796  znunit  16799  cygznlem3  16805  ipeq0  16824  obsip  16903  eltopspOLD  16938  istpsOLD  16940  istopon  16945  fctop  17023  cctop  17025  ppttop  17026  pptbas  17027  epttop  17028  t0sep  17342  t1sep2  17387  cmpsublem  17416  cmpsub  17417  txuni2  17550  elpt  17557  ptbasfi  17566  xkoopn  17574  ptpjopn  17597  ptclsg  17600  dfac14lem  17602  ptcnp  17607  ptrescn  17624  tx1stc  17635  qtopeu  17701  kqt0lem  17721  isr0  17722  hauspwpwf1  17972  xmeteq0  18321  imasf1oxmet  18358  comet  18496  stdbdxmet  18498  met2ndci  18505  prdsxmslem2  18512  nrmmetd  18575  tngngp  18648  xrsxmet  18793  iccpnfcnv  18922  iccpnfhmeo  18923  oprpiece1res2  18930  cnheibor  18933  phtpycc  18969  elovolm  19324  ovolgelb  19329  ovolicc1  19365  ovolicc  19372  ioorval  19419  uniioombllem6  19433  dyadmax  19443  dyadmbl  19445  i1fadd  19540  i1fmul  19541  itg1addlem3  19543  i1fmulc  19548  itg2l  19574  itg2leub  19579  limcmpt  19723  limcco  19733  dvcobr  19785  evlslem3  19888  deg1ldg  19968  ig1pval  20048  elply  20067  elply2  20068  coeval  20095  coe1termlem  20129  coe1term  20130  quotval  20162  plydivlem4  20166  plydivex  20167  vieta1  20182  aannenlem2  20199  aalioulem2  20203  abelthlem9  20309  logtayllem  20503  logtayl  20504  isosctrlem2  20616  atantayl2  20731  leibpilem2  20734  rlimcnp2  20758  efrlim  20761  dvdsmulf1o  20932  perfectlem2  20967  lgsfval  21038  lgsval2lem  21043  lgsdchrval  21084  2sqlem2  21101  2sqlem8  21109  2sqlem9  21110  2sqlem11  21112  dchrisum0flblem1  21155  padicval  21264  padicabv  21277  ostth1  21280  cusgrafilem2  21442  cusgrafi  21444  wlkntrllem3  21514  fargshiftf1  21577  fargshiftfo  21578  constr3trllem2  21591  vdusgraval  21631  gxval  21799  gxdi  21837  ismgm  21861  nvz  22111  nmosetn0  22219  nmoolb  22225  nmoubi  22226  nmlno0lem  22247  nmlno0i  22248  hvsubeq0  22523  hvaddcan  22525  normsub0  22591  norm1exi  22705  pjhval  22852  omlsii  22858  omlsi  22859  pjoml  22891  h1de2ci  23011  spansneleq  23025  h1datomi  23036  h1datom  23037  spansncv  23108  5oalem6  23114  pj11  23169  nmopsetn0  23321  nmfnsetn0  23334  nmoplb  23363  nmopub  23364  nmfnlb  23380  nmfnleub  23381  nmlnop0iALT  23451  nmlnop0  23454  lnopeq  23465  nmopun  23470  nmcexi  23482  branmfn  23561  pjnmopi  23604  pj3i  23664  atss  23802  atom1d  23809  chirred  23851  cdj3lem2  23891  elabreximd  23944  disjxpin  23981  fmptcof2  24029  xrge0iifcnv  24272  xrge0iifcv  24273  xrge0iifhom  24276  xrge0tmdOLD  24284  xrge0tmd  24285  esumc  24399  sconpi1  24879  cvmlift3lem2  24960  ghomf1olem  25058  relexp0  25082  relexpsucr  25083  relexpsucl  25085  rtrclreclem.trans  25099  prodmo  25215  fprod  25220  br8  25327  br6  25328  br4  25329  rdgprc0  25364  dfrdg2  25366  sltval2  25524  sltintdifex  25531  sltres  25532  dfbigcup2  25653  elfuns  25668  elsingles  25671  dfiota3  25676  brimageg  25680  brdomaing  25688  brrangeg  25689  dfrdg4  25703  tfrqfree  25704  elaltxp  25724  axpaschlem  25783  axlowdimlem15  25799  axlowdim  25804  funtransport  25869  fvtransport  25870  brsegle  25946  funray  25978  fvray  25979  funline  25980  fvline  25982  ellines  25990  linethru  25991  rankeq1o  26016  supaddc  26137  supadd  26138  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  subtr  26207  subtr2  26208  nn0prpw  26216  unirep  26304  f1opr  26316  sdclem2  26336  sdclem1  26337  sdc  26338  fdc  26339  isbnd  26379  heibor1lem  26408  heiborlem4  26413  heiborlem6  26415  heiborlem10  26419  maxidlmax  26543  prnc  26567  isfldidl  26568  dmnnzd  26575  elrfi  26638  nacsfg  26649  mzpcompact2lem  26698  eldioph2b  26711  eldioph3  26714  eldiophss  26723  diophrex  26724  elnn0rabdioph  26753  rencldnfilem  26771  elpell1qr  26800  elpell14qr  26802  elpell1234qr  26804  divalgmodcl  26948  jm2.27  26969  rmydioph  26975  expdiophlem2  26983  wepwsolem  27006  aomclem6  27024  uvcvval  27103  ellspd  27122  lnr2i  27188  lpirlnr  27189  hbtlem2  27196  hbtlem4  27198  hbtlem5  27200  rngunsnply  27246  flcidc  27247  psgneu  27297  psgnval  27298  psgnvali  27299  psgnvalii  27300  pm13.192  27478  refsum2cnlem1  27575  stoweidlem46  27662  afv0fv0  27880  afvfv0bi  27883  afvelrnb  27894  afvelrnb0  27895  otiunsndisj  27954  otiunsndisjX  27955  euhash1  27998  swrdccat3b  28031  frgra3vlem1  28104  3vfriswmgralem  28108  frgrancvvdeqlem4  28136  2spotiundisj  28165  usgreghash2spotv  28169  frgregordn0  28173  sgnval  28232  equncomVD  28689  csbingVD  28705  csbsngVD  28714  csbfv12gALTVD  28720  relopabVD  28722  bnj1468  28923  lshpdisj  29470  lsat0cv  29516  lcvexchlem4  29520  lcvexchlem5  29521  lshpkrlem1  29593  lshpkrlem2  29594  lshpkrlem3  29595  lshpkrcl  29599  islshpkrN  29603  atnle  29800  glbconxN  29860  isline  30221  ispointN  30224  pmapglbx  30251  ispsubcl2N  30429  lhp2atnle  30515  cdleme43fsv1snlem  30902  cdleme40v  30951  cdlemkid5  31417  cdlemkid  31418  dvhb1dimN  31468  dib1dim  31648  dicopelval  31660  dicelval1sta  31670  diclspsn  31677  dihvalcqpre  31718  dihglblem2aN  31776  dihglblem2N  31777  dih1dimatlem  31812  dihpN  31819  dochfl1  31959  lcfl7N  31984  lcf1o  32034  hvmapvalvalN  32244  hdmapval2lem  32317
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator