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

Theorem eqeq1 2439
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 2427 . . . . . 6  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
21biimpi 194 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1803 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
43bibi1d 319 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  <->  x  e.  C )  <->  ( x  e.  B  <->  x  e.  C
) ) )
54albidv 1678 . 2  |-  ( A  =  B  ->  ( A. x ( x  e.  A  <->  x  e.  C
)  <->  A. x ( x  e.  B  <->  x  e.  C ) ) )
6 dfcleq 2427 . 2  |-  ( A  =  C  <->  A. x
( x  e.  A  <->  x  e.  C ) )
7 dfcleq 2427 . 2  |-  ( B  =  C  <->  A. x
( x  e.  B  <->  x  e.  C ) )
85, 6, 73bitr4g 288 1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1360    = wceq 1362    e. wcel 1755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-ex 1590  df-cleq 2426
This theorem is referenced by:  eqeq1i  2440  eqeq1d  2441  eqeq2  2442  eqeq12  2445  eqtr  2450  eqsb3lem  2533  clelab  2553  neeq1  2606  pm13.18  2673  issetf  2967  sbhypf  3008  vtoclgft  3009  rexraleqim  3074  eqvincf  3076  pm13.183  3089  eueq  3120  mob  3130  euind  3135  reuind  3151  eqsbc3  3214  csbhypf  3295  uniiunlem  3428  snjust  3864  elprg  3881  elsncg  3888  rabrsn  3933  sneqrg  4030  preq12bg  4039  prel12g  4040  intab  4146  uniintsn  4153  dfiin2g  4191  disji2  4267  disjprg  4276  eusv1  4474  reusv2lem2  4482  reusv3  4488  reusv6OLD  4491  opthg  4555  copsexg  4564  copsexgOLD  4565  euotd  4580  elopab  4585  solin  4651  elxpi  4843  opbrop  4903  relop  4977  ideqg  4978  elrnmpt  5073  elrnmpt1  5075  elrnmptg  5076  somin1  5222  cnveqb  5281  relcoi1  5354  funopg  5438  fvelrnb  5727  fvmptg  5760  fndmin  5798  eldmrexrn  5837  foelrn  5850  foco2  5851  fmptco  5863  fmptsng  5887  eufnfv  5938  elabrex  5947  abrexco  5948  f1veqaeq  5959  isosolem  6025  f1oiso  6029  eusvobj2  6072  oprabid  6104  mpt2fun  6181  elrnmpt2g  6191  elrnmpt2  6192  elrnmpt2res  6193  ralrnmpt2  6194  ov3  6216  ov6g  6217  ovelrn  6228  caovcang  6253  caovcan  6256  snnex  6371  uniuni  6374  orduninsuc  6443  funcnvuni  6519  fun11iun  6526  f1oweALT  6550  opiota  6622  eloprabi  6625  frxp  6671  funsssuppss  6704  dftpos4  6753  tz7.44-2  6849  tz7.44-3  6850  oev  6942  oalimcl  6987  omlimcl  7005  odi  7006  omeu  7012  oeeui  7029  nneob  7079  omopth  7085  elqsg  7140  qsdisj  7165  qsel  7167  brecop  7181  eroveu  7183  erovlem  7184  th3qlem1  7194  th3q  7197  elixpsn  7290  ixpsnf1o  7291  boxcutc  7294  2dom  7370  fundmen  7371  xpf1o  7461  nneneq  7482  fofinf1o  7580  elfi  7651  elfiun  7668  dffi3  7669  brwdom  7770  brwdom3  7785  unwdomg  7787  xpwdomg  7788  noinfep  7853  cantnfp1lem1  7874  cantnfp1lem3  7876  cantnflem1  7885  cantnfp1lem1OLD  7900  cantnfp1lem3OLD  7902  cantnfp1OLD  7903  cantnflem1OLD  7908  scott0  8081  carden2a  8124  cardiun  8140  pm54.43lem  8157  alephval3  8268  dfac5lem3  8283  dfac5lem4  8284  dfac2  8288  kmlem9  8315  kmlem12  8318  cardcf  8409  cfeq0  8413  cfsuc  8414  cff1  8415  cflim2  8420  cfss  8422  isfin5  8456  fin1a2lem11  8567  fin1a2lem13  8569  brdom7disj  8686  brdom6disj  8687  canthp1lem2  8808  canthp1  8809  tskuni  8938  gruina  8973  genpv  9156  genpelv  9157  ltsosr  9249  ltresr  9295  axcnre  9319  axpre-lttri  9320  ltordlem  9853  ltord1  9854  fimaxre3  10267  supmul1  10283  supmullem1  10284  supmullem2  10285  supmul  10286  creur  10304  creui  10305  nn1m1nn  10330  elz  10636  nn0ind-raph  10730  xnegeq  11165  xmullem2  11216  xmulasslem  11236  fleqceilz  11677  fseqsupubi  11784  sqeqor  11964  nn0opth2  12034  hash1snb  12155  euhash1  12156  hash2prde  12163  hash2prd  12165  hash2pwpr  12166  brfi1uzind  12203  wrd2ind  12356  cshfn  12411  ccatco  12447  shftfval  12543  sgnval  12561  sqrlem6  12721  summo  13178  fsum  13181  fsumtscopo  13248  infcvgaux1i  13302  infcvgaux2i  13303  mertenslem1  13327  mertenslem2  13328  mertens  13329  ruclem12  13506  divalg  13590  ndvdssub  13594  bitsinvp1  13628  sadcp1  13634  smupp1  13659  gcdval  13675  bezoutlem1  13705  bezoutlem3  13707  bezoutlem4  13708  bezout  13709  dvdsprime  13759  nprm  13760  dvdsprm  13768  coprm  13769  qnumval  13798  qdenval  13799  reumodprminv  13855  pcval  13894  pceu  13896  pczpre  13897  pcdiv  13902  4sqlem2  13993  4sqlem4  13996  4sqlem12  14000  4sq  14008  vdwapval  14017  vdwapun  14018  vdwlem6  14030  cshwrepswhash1  14112  acsfn  14580  posi  15103  gsumval2a  15492  ghmf1  15755  conjnmzb  15761  orbsta  15811  symgextfv  15903  symgextfo  15907  symgfixfo  15925  pmtrprfval  15973  pmtrprfvalrn  15974  psgneu  15992  psgnval  15993  psgnvali  15994  psgnvalii  15995  odval  16017  dfod2  16045  submod  16048  isslw  16087  sylow2alem1  16096  sylow3lem2  16107  lsmelvalm  16130  lsmdisj2  16159  efgrelexlemb  16227  frgpup3lem  16254  cyggeninv  16340  cygabl  16347  gsumval3eu  16361  gsumval3OLD  16362  gsumval3lem2  16364  dprddisj2  16511  dprddisj2OLD  16512  dpjrid  16535  pgpfac1lem3  16552  abveq0  16835  abvtrivd  16849  lss1d  16966  lspsn  17005  lspsnel  17006  lspprel  17097  rrgeq0i  17282  domneq0  17291  psrlidm  17408  psrlidmOLD  17409  psrridm  17410  psrridmOLD  17411  mvrval2  17429  mvrf1  17432  mplmonmul  17477  coe1tm  17624  coe1tmfv2  17626  xrsdsreval  17702  prmirredlem  17759  prmirredlemOLD  17762  znf1o  17826  znfld  17835  znunit  17838  cygznlem3  17844  psgndif  17874  ipeq0  17909  obsip  17988  frlmphl  18048  uvcvval  18053  ellspd  18072  ellspdOLD  18073  mamufacex  18131  dmatcomp  18145  mavmulsolcl  18204  marrepeval  18216  marepveval  18221  mdetunilem8  18267  maducoeval2  18288  madugsum  18291  minmar1eval  18297  symgmatr01lem  18301  symgmatr01  18302  gsummatr01lem3  18305  gsummatr01lem4  18306  gsummatr01  18307  eltopspOLD  18365  istpsOLD  18367  istopon  18372  fctop  18450  cctop  18452  ppttop  18453  pptbas  18454  epttop  18455  t0sep  18770  t1sep2  18815  cmpsublem  18844  cmpsub  18845  txuni2  18980  elpt  18987  ptbasfi  18996  xkoopn  19004  ptpjopn  19027  ptclsg  19030  dfac14lem  19032  ptcnp  19037  ptrescn  19054  tx1stc  19065  qtopeu  19131  kqt0lem  19151  isr0  19152  hauspwpwf1  19402  xmeteq0  19755  imasf1oxmet  19792  comet  19930  stdbdxmet  19932  met2ndci  19939  prdsxmslem2  19946  nrmmetd  20009  tngngp  20082  xrsxmet  20228  iccpnfcnv  20358  iccpnfhmeo  20359  oprpiece1res2  20366  cnheibor  20369  phtpycc  20405  elovolm  20800  ovolgelb  20805  ovolicc1  20841  ovolicc  20848  ioorval  20896  uniioombllem6  20910  dyadmax  20920  dyadmbl  20922  i1fadd  21015  i1fmul  21016  itg1addlem3  21018  i1fmulc  21023  itg2l  21049  itg2leub  21054  limcmpt  21200  limcco  21210  dvcobr  21262  evlslem3  21366  deg1ldg  21448  ig1pval  21529  elply  21548  elply2  21549  coeval  21576  coe1termlem  21610  coe1term  21611  quotval  21643  plydivlem4  21647  plydivex  21648  vieta1  21663  aannenlem2  21680  aalioulem2  21684  abelthlem9  21790  logtayllem  21989  logtayl  21990  isosctrlem2  22102  atantayl2  22218  leibpilem2  22221  rlimcnp2  22245  efrlim  22248  dvdsmulf1o  22419  perfectlem2  22454  lgsfval  22525  lgsval2lem  22530  lgsdchrval  22571  2sqlem2  22588  2sqlem8  22596  2sqlem9  22597  2sqlem11  22599  dchrisum0flblem1  22642  padicval  22751  padicabv  22764  ostth1  22767  axtgcgrid  22809  axtgbtwnid  22812  axpaschlem  23009  axlowdimlem15  23025  axlowdim  23030  cusgrafilem2  23211  cusgrafi  23213  wlkntrllem3  23283  fargshiftf1  23346  fargshiftfo  23347  constr3trllem2  23360  vdusgraval  23400  gxval  23568  gxdi  23606  ismgm  23630  nvz  23880  nmosetn0  23988  nmoolb  23994  nmoubi  23995  nmlno0lem  24016  nmlno0i  24017  hvsubeq0  24293  hvaddcan  24295  normsub0  24361  norm1exi  24476  pjhval  24623  omlsii  24629  omlsi  24630  pjoml  24662  h1de2ci  24782  spansneleq  24796  h1datomi  24807  h1datom  24808  spansncv  24879  5oalem6  24885  pj11  24940  nmopsetn0  25092  nmfnsetn0  25105  nmoplb  25134  nmopub  25135  nmfnlb  25151  nmfnleub  25152  nmlnop0iALT  25222  nmlnop0  25225  lnopeq  25236  nmopun  25241  nmcexi  25253  branmfn  25332  pjnmopi  25375  pj3i  25435  atss  25573  atom1d  25580  chirred  25622  cdj3lem2  25662  elabreximd  25715  disjxpin  25754  disjunsn  25760  br8d  25766  fmptcof2  25803  sgnsval  26015  xrge0iifcnv  26217  xrge0iifcv  26218  xrge0iifhom  26221  xrge0tmdOLD  26229  xrge0tmd  26230  esumc  26359  sgn3da  26772  sgnmul  26773  sgnnbi  26776  sgnpbi  26777  sgn0bi  26778  ccatmulgnn0dir  26788  plymulx0  26796  plymulx  26797  signspval  26801  sconpi1  26976  cvmlift3lem2  27057  ghomf1olem  27160  relexp0  27178  relexpsucr  27179  relexpsucl  27181  rtrclreclem.trans  27195  prodmo  27296  fprod  27301  br8  27413  br6  27414  br4  27415  rdgprc0  27454  dfrdg2  27456  sltval2  27644  sltintdifex  27651  sltres  27652  dfbigcup2  27777  elsingles  27796  dfiota3  27801  brimageg  27805  brdomaing  27813  brrangeg  27814  dfrdg4  27828  tfrqfree  27829  elaltxp  27853  funtransport  27909  fvtransport  27910  brsegle  27986  funray  28018  fvray  28019  funline  28020  fvline  28022  ellines  28030  linethru  28031  rankeq1o  28056  fin2so  28260  supaddc  28261  supadd  28262  ptrest  28269  heicant  28270  mblfinlem1  28272  mblfinlem2  28273  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  itg2addnclem  28287  itg2addnclem3  28289  itg2addnc  28290  ftc1anc  28319  subtr  28353  subtr2  28354  nn0prpw  28362  unirep  28450  f1opr  28462  sdclem2  28482  sdclem1  28483  sdc  28484  fdc  28485  isbnd  28523  heibor1lem  28552  heiborlem4  28557  heiborlem6  28559  heiborlem10  28563  maxidlmax  28687  prnc  28711  isfldidl  28712  dmnnzd  28719  elrfi  28875  nacsfg  28886  mzpcompact2lem  28933  eldioph2b  28946  eldioph3  28949  eldiophss  28958  diophrex  28959  elnn0rabdioph  28986  rencldnfilem  29004  elpell1qr  29033  elpell14qr  29035  elpell1234qr  29037  divalgmodcl  29181  jm2.27  29202  rmydioph  29208  expdiophlem2  29216  wepwsolem  29239  aomclem6  29257  lnr2i  29317  lpirlnr  29318  hbtlem2  29325  hbtlem4  29327  hbtlem5  29329  rngunsnply  29375  flcidc  29376  pm13.192  29509  refsum2cnlem1  29604  stoweidlem46  29687  afv0fv0  29901  afvfv0bi  29904  afvelrnb  29915  afvelrnb0  29916  otiunsndisj  29978  otiunsndisjX  29979  f0rn0  29987  oprabv  30003  2ffzoeq  30060  m1dvdsndvds  30093  2wlkeq  30134  wwlkn0  30169  wlklniswwlkn1  30179  clwlkisclwwlklem2a1  30287  cshwlemma1  30335  scshwfzeqfzo  30338  Lemma2  30339  eleclclwwlkn  30353  hashecclwwlkn1  30354  usghashecclwwlk  30355  rusgranumwlkl1  30405  frgra3vlem1  30438  3vfriswmgralem  30442  frgrancvvdeqlem4  30472  2spotiundisj  30501  usgreghash2spotv  30505  frgregordn0  30509  numclwlk1lem2f1  30533  frgrareggt1  30555  fmptsnd  30567  suppmptcfin  30623  lcoval  30655  linc0scn0  30666  linc1  30668  el0ldep  30709  snlindsntor  30714  equncomVD  31306  csbingVD  31322  csbsngVD  31331  csbfv12gALTVD  31337  relopabVD  31339  bnj1468  31541  riotasvd  32180  lshpdisj  32205  lsat0cv  32251  lcvexchlem4  32255  lcvexchlem5  32256  lshpkrlem1  32328  lshpkrlem2  32329  lshpkrlem3  32330  lshpkrcl  32334  islshpkrN  32338  atnle  32535  glbconxN  32595  isline  32956  ispointN  32959  pmapglbx  32986  ispsubcl2N  33164  lhp2atnle  33250  cdleme43fsv1snlem  33637  cdleme40v  33686  cdlemkid5  34152  cdlemkid  34153  dvhb1dimN  34203  dib1dim  34383  dicopelval  34395  dicelval1sta  34405  diclspsn  34412  dihvalcqpre  34453  dihglblem2aN  34511  dihglblem2N  34512  dih1dimatlem  34547  dihpN  34554  dochfl1  34694  lcfl7N  34719  lcf1o  34769  hvmapvalvalN  34979  hdmapval2lem  35052
  Copyright terms: Public domain W3C validator