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 194 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1804 . . . 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 1679 . 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 288 1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1367    = wceq 1369    e. wcel 1756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2431
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  2972  sbhypf  3014  vtoclgft  3015  rexraleqim  3080  eqvincf  3082  pm13.183  3095  eueq  3126  mob  3136  euind  3141  reuind  3157  eqsbc3  3221  csbhypf  3302  uniiunlem  3435  snjust  3871  elprg  3888  elsncg  3895  rabrsn  3940  sneqrg  4037  preq12bg  4046  prel12g  4047  intab  4153  uniintsn  4160  dfiin2g  4198  disji2  4274  disjprg  4283  eusv1  4481  reusv2lem2  4489  reusv3  4495  reusv6OLD  4498  opthg  4562  copsexg  4571  copsexgOLD  4572  euotd  4587  elopab  4592  solin  4659  elxpi  4851  opbrop  4911  relop  4985  ideqg  4986  elrnmpt  5081  elrnmpt1  5083  elrnmptg  5084  somin1  5229  cnveqb  5288  relcoi1  5361  funopg  5445  fvelrnb  5734  fvmptg  5767  fndmin  5805  eldmrexrn  5844  foelrn  5857  foco2  5858  fmptco  5871  fmptsng  5895  eufnfv  5946  elabrex  5955  abrexco  5956  f1veqaeq  5967  isosolem  6033  f1oiso  6037  eusvobj2  6079  oprabid  6110  mpt2fun  6187  elrnmpt2g  6197  elrnmpt2  6198  elrnmpt2res  6199  ralrnmpt2  6200  ov3  6222  ov6g  6223  ovelrn  6234  caovcang  6259  caovcan  6262  snnex  6377  uniuni  6380  orduninsuc  6449  funcnvuni  6525  fun11iun  6532  f1oweALT  6556  opiota  6628  eloprabi  6631  frxp  6677  funsssuppss  6710  dftpos4  6759  tz7.44-2  6855  tz7.44-3  6856  oev  6946  oalimcl  6991  omlimcl  7009  odi  7010  omeu  7016  oeeui  7033  nneob  7083  omopth  7089  elqsg  7144  qsdisj  7169  qsel  7171  brecop  7185  eroveu  7187  erovlem  7188  th3qlem1  7198  th3q  7201  elixpsn  7294  ixpsnf1o  7295  boxcutc  7298  2dom  7374  fundmen  7375  xpf1o  7465  nneneq  7486  fofinf1o  7584  elfi  7655  elfiun  7672  dffi3  7673  brwdom  7774  brwdom3  7789  unwdomg  7791  xpwdomg  7792  noinfep  7857  cantnfp1lem1  7878  cantnfp1lem3  7880  cantnflem1  7889  cantnfp1lem1OLD  7904  cantnfp1lem3OLD  7906  cantnfp1OLD  7907  cantnflem1OLD  7912  scott0  8085  carden2a  8128  cardiun  8144  pm54.43lem  8161  alephval3  8272  dfac5lem3  8287  dfac5lem4  8288  dfac2  8292  kmlem9  8319  kmlem12  8322  cardcf  8413  cfeq0  8417  cfsuc  8418  cff1  8419  cflim2  8424  cfss  8426  isfin5  8460  fin1a2lem11  8571  fin1a2lem13  8573  brdom7disj  8690  brdom6disj  8691  canthp1lem2  8812  canthp1  8813  tskuni  8942  gruina  8977  genpv  9160  genpelv  9161  ltsosr  9253  ltresr  9299  axcnre  9323  axpre-lttri  9324  ltordlem  9857  ltord1  9858  fimaxre3  10271  supmul1  10287  supmullem1  10288  supmullem2  10289  supmul  10290  creur  10308  creui  10309  nn1m1nn  10334  elz  10640  nn0ind-raph  10734  xnegeq  11169  xmullem2  11220  xmulasslem  11240  fleqceilz  11685  fseqsupubi  11792  sqeqor  11972  nn0opth2  12042  hash1snb  12163  euhash1  12164  hash2prde  12171  hash2prd  12173  hash2pwpr  12174  brfi1uzind  12211  wrd2ind  12364  cshfn  12419  ccatco  12455  shftfval  12551  sgnval  12569  sqrlem6  12729  summo  13186  fsum  13189  fsumtscopo  13257  infcvgaux1i  13311  infcvgaux2i  13312  mertenslem1  13336  mertenslem2  13337  mertens  13338  ruclem12  13515  divalg  13599  ndvdssub  13603  bitsinvp1  13637  sadcp1  13643  smupp1  13668  gcdval  13684  bezoutlem1  13714  bezoutlem3  13716  bezoutlem4  13717  bezout  13718  dvdsprime  13768  nprm  13769  dvdsprm  13777  coprm  13778  qnumval  13807  qdenval  13808  reumodprminv  13864  pcval  13903  pceu  13905  pczpre  13906  pcdiv  13911  4sqlem2  14002  4sqlem4  14005  4sqlem12  14009  4sq  14017  vdwapval  14026  vdwapun  14027  vdwlem6  14039  cshwrepswhash1  14121  acsfn  14589  posi  15112  gsumval2a  15503  ghmf1  15766  conjnmzb  15772  orbsta  15822  symgextfv  15914  symgextfo  15918  symgfixfo  15936  pmtrprfval  15984  pmtrprfvalrn  15985  psgneu  16003  psgnval  16004  psgnvali  16005  psgnvalii  16006  odval  16028  dfod2  16056  submod  16059  isslw  16098  sylow2alem1  16107  sylow3lem2  16118  lsmelvalm  16141  lsmdisj2  16170  efgrelexlemb  16238  frgpup3lem  16265  cyggeninv  16351  cygabl  16358  gsumval3eu  16372  gsumval3OLD  16373  gsumval3lem2  16375  dprddisj2  16525  dprddisj2OLD  16526  dpjrid  16549  pgpfac1lem3  16566  abveq0  16889  abvtrivd  16903  lss1d  17021  lspsn  17060  lspsnel  17061  lspprel  17152  rrgeq0i  17337  domneq0  17346  psrlidm  17451  psrlidmOLD  17452  psrridm  17453  psrridmOLD  17454  mvrval2  17472  mvrf1  17475  mplmonmul  17520  evlslem3  17575  coe1tm  17701  coe1tmfv2  17703  xrsdsreval  17833  prmirredlem  17892  prmirredlemOLD  17895  znf1o  17959  znfld  17968  znunit  17971  cygznlem3  17977  psgndif  18007  ipeq0  18042  obsip  18121  frlmphl  18181  uvcvval  18186  ellspd  18205  ellspdOLD  18206  mamufacex  18264  dmatcomp  18278  mavmulsolcl  18337  marrepeval  18349  marepveval  18354  mdetunilem8  18400  maducoeval2  18421  madugsum  18424  minmar1eval  18430  symgmatr01lem  18434  symgmatr01  18435  gsummatr01lem3  18438  gsummatr01lem4  18439  gsummatr01  18440  eltopspOLD  18498  istpsOLD  18500  istopon  18505  fctop  18583  cctop  18585  ppttop  18586  pptbas  18587  epttop  18588  t0sep  18903  t1sep2  18948  cmpsublem  18977  cmpsub  18978  txuni2  19113  elpt  19120  ptbasfi  19129  xkoopn  19137  ptpjopn  19160  ptclsg  19163  dfac14lem  19165  ptcnp  19170  ptrescn  19187  tx1stc  19198  qtopeu  19264  kqt0lem  19284  isr0  19285  hauspwpwf1  19535  xmeteq0  19888  imasf1oxmet  19925  comet  20063  stdbdxmet  20065  met2ndci  20072  prdsxmslem2  20079  nrmmetd  20142  tngngp  20215  xrsxmet  20361  iccpnfcnv  20491  iccpnfhmeo  20492  oprpiece1res2  20499  cnheibor  20502  phtpycc  20538  elovolm  20933  ovolgelb  20938  ovolicc1  20974  ovolicc  20981  ioorval  21029  uniioombllem6  21043  dyadmax  21053  dyadmbl  21055  i1fadd  21148  i1fmul  21149  itg1addlem3  21151  i1fmulc  21156  itg2l  21182  itg2leub  21187  limcmpt  21333  limcco  21343  dvcobr  21395  deg1ldg  21538  ig1pval  21619  elply  21638  elply2  21639  coeval  21666  coe1termlem  21700  coe1term  21701  quotval  21733  plydivlem4  21737  plydivex  21738  vieta1  21753  aannenlem2  21770  aalioulem2  21774  abelthlem9  21880  logtayllem  22079  logtayl  22080  isosctrlem2  22192  atantayl2  22308  leibpilem2  22311  rlimcnp2  22335  efrlim  22338  dvdsmulf1o  22509  perfectlem2  22544  lgsfval  22615  lgsval2lem  22620  lgsdchrval  22661  2sqlem2  22678  2sqlem8  22686  2sqlem9  22687  2sqlem11  22689  dchrisum0flblem1  22732  padicval  22841  padicabv  22854  ostth1  22857  axtgcgrid  22899  axtgbtwnid  22902  axpaschlem  23137  axlowdimlem15  23153  axlowdim  23158  cusgrafilem2  23339  cusgrafi  23341  wlkntrllem3  23411  fargshiftf1  23474  fargshiftfo  23475  constr3trllem2  23488  vdusgraval  23528  gxval  23696  gxdi  23734  ismgm  23758  nvz  24008  nmosetn0  24116  nmoolb  24122  nmoubi  24123  nmlno0lem  24144  nmlno0i  24145  hvsubeq0  24421  hvaddcan  24423  normsub0  24489  norm1exi  24604  pjhval  24751  omlsii  24757  omlsi  24758  pjoml  24790  h1de2ci  24910  spansneleq  24924  h1datomi  24935  h1datom  24936  spansncv  25007  5oalem6  25013  pj11  25068  nmopsetn0  25220  nmfnsetn0  25233  nmoplb  25262  nmopub  25263  nmfnlb  25279  nmfnleub  25280  nmlnop0iALT  25350  nmlnop0  25353  lnopeq  25364  nmopun  25369  nmcexi  25381  branmfn  25460  pjnmopi  25503  pj3i  25563  atss  25701  atom1d  25708  chirred  25750  cdj3lem2  25790  elabreximd  25842  disjxpin  25881  disjunsn  25887  br8d  25893  fmptcof2  25930  sgnsval  26142  xrge0iifcnv  26315  xrge0iifcv  26316  xrge0iifhom  26319  xrge0tmdOLD  26327  xrge0tmd  26328  esumc  26457  sgn3da  26876  sgnmul  26877  sgnnbi  26880  sgnpbi  26881  sgn0bi  26882  ccatmulgnn0dir  26892  plymulx0  26900  plymulx  26901  signspval  26905  sconpi1  27080  cvmlift3lem2  27161  ghomf1olem  27264  relexp0  27282  relexpsucr  27283  relexpsucl  27285  rtrclreclem.trans  27299  prodmo  27400  fprod  27405  br8  27517  br6  27518  br4  27519  rdgprc0  27558  dfrdg2  27560  sltval2  27748  sltintdifex  27755  sltres  27756  dfbigcup2  27881  elsingles  27900  dfiota3  27905  brimageg  27909  brdomaing  27917  brrangeg  27918  dfrdg4  27932  tfrqfree  27933  elaltxp  27957  funtransport  28013  fvtransport  28014  brsegle  28090  funray  28122  fvray  28123  funline  28124  fvline  28126  ellines  28134  linethru  28135  rankeq1o  28160  fin2so  28369  supaddc  28370  supadd  28371  ptrest  28378  heicant  28379  mblfinlem1  28381  mblfinlem2  28382  mblfinlem3  28383  mblfinlem4  28384  ismblfin  28385  itg2addnclem  28396  itg2addnclem3  28398  itg2addnc  28399  ftc1anc  28428  subtr  28462  subtr2  28463  nn0prpw  28471  unirep  28559  f1opr  28571  sdclem2  28591  sdclem1  28592  sdc  28593  fdc  28594  isbnd  28632  heibor1lem  28661  heiborlem4  28666  heiborlem6  28668  heiborlem10  28672  maxidlmax  28796  prnc  28820  isfldidl  28821  dmnnzd  28828  elrfi  28983  nacsfg  28994  mzpcompact2lem  29041  eldioph2b  29054  eldioph3  29057  eldiophss  29066  diophrex  29067  elnn0rabdioph  29094  rencldnfilem  29112  elpell1qr  29141  elpell14qr  29143  elpell1234qr  29145  divalgmodcl  29289  jm2.27  29310  rmydioph  29316  expdiophlem2  29324  wepwsolem  29347  aomclem6  29365  lnr2i  29425  lpirlnr  29426  hbtlem2  29433  hbtlem4  29435  hbtlem5  29437  rngunsnply  29483  flcidc  29484  pm13.192  29617  refsum2cnlem1  29712  stoweidlem46  29794  afv0fv0  30008  afvfv0bi  30011  afvelrnb  30022  afvelrnb0  30023  otiunsndisj  30085  otiunsndisjX  30086  f0rn0  30094  oprabv  30110  2ffzoeq  30167  m1dvdsndvds  30200  2wlkeq  30241  wwlkn0  30276  wlklniswwlkn1  30286  clwlkisclwwlklem2a1  30394  cshwlemma1  30442  scshwfzeqfzo  30445  Lemma2  30446  eleclclwwlkn  30460  hashecclwwlkn1  30461  usghashecclwwlk  30462  rusgranumwlkl1  30512  frgra3vlem1  30545  3vfriswmgralem  30549  frgrancvvdeqlem4  30579  2spotiundisj  30608  usgreghash2spotv  30612  frgregordn0  30616  numclwlk1lem2f1  30640  frgrareggt1  30662  fmptsnd  30674  suppmptcfin  30743  mat1dimelbas  30790  mat1dimid  30793  lcoval  30835  linc0scn0  30846  linc1  30848  el0ldep  30889  snlindsntor  30894  equncomVD  31491  csbingVD  31507  csbsngVD  31516  csbfv12gALTVD  31522  relopabVD  31524  bnj1468  31726  riotasvd  32447  lshpdisj  32472  lsat0cv  32518  lcvexchlem4  32522  lcvexchlem5  32523  lshpkrlem1  32595  lshpkrlem2  32596  lshpkrlem3  32597  lshpkrcl  32601  islshpkrN  32605  atnle  32802  glbconxN  32862  isline  33223  ispointN  33226  pmapglbx  33253  ispsubcl2N  33431  lhp2atnle  33517  cdleme43fsv1snlem  33904  cdleme40v  33953  cdlemkid5  34419  cdlemkid  34420  dvhb1dimN  34470  dib1dim  34650  dicopelval  34662  dicelval1sta  34672  diclspsn  34679  dihvalcqpre  34720  dihglblem2aN  34778  dihglblem2N  34779  dih1dimatlem  34814  dihpN  34821  dochfl1  34961  lcfl7N  34986  lcf1o  35036  hvmapvalvalN  35246  hdmapval2lem  35319
  Copyright terms: Public domain W3C validator