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

Theorem eqeq1 2442
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 2430 . . . . . 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 2430 . 2  |-  ( A  =  C  <->  A. x
( x  e.  A  <->  x  e.  C ) )
7 dfcleq 2430 . 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  2443  eqeq1d  2444  eqeq2  2445  eqeq12  2448  eqtr  2453  eqsb3lem  2536  clelab  2556  neeq1  2609  pm13.18  2676  issetf  2961  sbhypf  3001  vtoclgft  3002  eqvincf  3064  pm13.183  3076  eueq  3106  mob  3116  euind  3121  reuind  3137  eqsbc3  3200  csbhypf  3286  uniiunlem  3431  snjust  3819  elprg  3831  elsncg  3836  rabrsn  3874  sneqrg  3968  preq12bg  3977  intab  4080  uniintsn  4087  dfiin2g  4124  disji2  4199  disjprg  4208  opthg  4436  copsexg  4442  euotd  4457  elopab  4462  solin  4526  snnex  4713  uniuni  4716  eusv1  4717  reusv2lem2  4725  reusv3  4731  reusv6OLD  4734  orduninsuc  4823  elxpi  4894  opbrop  4955  relop  5023  ideqg  5024  elrnmpt  5117  elrnmpt1  5119  elrnmptg  5120  somin1  5270  cnveqb  5326  relcoi1  5398  funopg  5485  funcnvuni  5518  fun11iun  5695  fvelrnb  5774  fvmptg  5804  fndmin  5837  eldmrexrn  5876  foelrn  5888  foco2  5889  fmptco  5901  eufnfv  5972  elabrex  5985  abrexco  5986  f1veqaeq  6005  isosolem  6067  f1oiso  6071  f1oweALT  6074  oprabid  6105  mpt2fun  6172  elrnmpt2g  6182  elrnmpt2  6183  ralrnmpt2  6184  ov3  6210  ov6g  6211  ovelrn  6222  caovcang  6248  caovcan  6251  eloprabi  6413  frxp  6456  dftpos4  6498  opiota  6535  eusvobj2  6582  riotasvd  6592  riotasvdOLD  6593  tz7.44-2  6665  tz7.44-3  6666  oev  6758  oalimcl  6803  omlimcl  6821  odi  6822  omeu  6828  oeeui  6845  nneob  6895  omopth  6901  elqsg  6956  qsdisj  6981  qsel  6983  brecop  6997  eroveu  6999  erovlem  7000  th3qlem1  7010  th3q  7013  elixpsn  7101  ixpsnf1o  7102  boxcutc  7105  2dom  7179  fundmen  7180  xpf1o  7269  nneneq  7290  fofinf1o  7387  elfi  7418  elfiun  7435  dffi3  7436  brwdom  7535  brwdom3  7550  unwdomg  7552  xpwdomg  7553  noinfep  7614  cantnfp1lem1  7634  cantnfp1lem3  7636  cantnfp1  7637  cantnflem1  7645  scott0  7810  carden2a  7853  cardiun  7869  pm54.43lem  7886  alephval3  7991  dfac5lem3  8006  dfac5lem4  8007  dfac2  8011  kmlem9  8038  kmlem12  8041  cardcf  8132  cfeq0  8136  cfsuc  8137  cff1  8138  cflim2  8143  cfss  8145  isfin5  8179  fin1a2lem11  8290  fin1a2lem13  8292  brdom7disj  8409  brdom6disj  8410  canthp1lem2  8528  canthp1  8529  tskuni  8658  gruina  8693  genpv  8876  genpelv  8877  ltsosr  8969  ltresr  9015  axcnre  9039  axpre-lttri  9040  ltordlem  9552  ltord1  9553  fimaxre3  9957  supmul1  9973  supmullem1  9974  supmullem2  9975  supmul  9976  creur  9994  creui  9995  nn1m1nn  10020  elz  10284  nn0ind-raph  10370  xnegeq  10793  xmullem2  10844  xmulasslem  10864  fseqsupubi  11317  sqeqor  11495  nn0opth2  11565  hash1snb  11681  hash2prde  11688  brfi1uzind  11715  ccatco  11804  shftfval  11885  sqrlem6  12053  summo  12511  fsum  12514  fsumtscopo  12581  infcvgaux1i  12636  infcvgaux2i  12637  mertenslem1  12661  mertenslem2  12662  mertens  12663  ruclem12  12840  divalg  12923  ndvdssub  12927  bitsinvp1  12961  sadcp1  12967  smupp1  12992  gcdval  13008  bezoutlem1  13038  bezoutlem3  13040  bezoutlem4  13041  bezout  13042  dvdsprime  13092  nprm  13093  dvdsprm  13099  coprm  13100  qnumval  13129  qdenval  13130  pcval  13218  pceu  13220  pczpre  13221  pcdiv  13226  4sqlem2  13317  4sqlem4  13320  4sqlem12  13324  4sq  13332  vdwapval  13341  vdwapun  13342  vdwlem6  13354  acsfn  13884  posi  14407  gsumval2a  14782  ghmf1  15034  conjnmzb  15040  orbsta  15090  odval  15172  dfod2  15200  submod  15203  isslw  15242  sylow2alem1  15251  sylow3lem2  15262  lsmelvalm  15285  lsmdisj2  15314  efgrelexlemb  15382  frgpup3lem  15409  cyggeninv  15493  cygabl  15500  gsumval3eu  15513  gsumval3  15514  dprddisj2  15597  dpjrid  15620  pgpfac1lem3  15635  abveq0  15914  abvtrivd  15928  lss1d  16039  lspsn  16078  lspsnel  16079  lspprel  16166  rrgeq0i  16349  domneq0  16357  psrlidm  16467  psrridm  16468  mvrval2  16486  mvrf1  16489  mplmonmul  16527  coe1tm  16665  coe1tmfv2  16667  xrsdsreval  16743  prmirredlem  16773  znf1o  16832  znfld  16841  znunit  16844  cygznlem3  16850  ipeq0  16869  obsip  16948  eltopspOLD  16983  istpsOLD  16985  istopon  16990  fctop  17068  cctop  17070  ppttop  17071  pptbas  17072  epttop  17073  t0sep  17388  t1sep2  17433  cmpsublem  17462  cmpsub  17463  txuni2  17597  elpt  17604  ptbasfi  17613  xkoopn  17621  ptpjopn  17644  ptclsg  17647  dfac14lem  17649  ptcnp  17654  ptrescn  17671  tx1stc  17682  qtopeu  17748  kqt0lem  17768  isr0  17769  hauspwpwf1  18019  xmeteq0  18368  imasf1oxmet  18405  comet  18543  stdbdxmet  18545  met2ndci  18552  prdsxmslem2  18559  nrmmetd  18622  tngngp  18695  xrsxmet  18840  iccpnfcnv  18969  iccpnfhmeo  18970  oprpiece1res2  18977  cnheibor  18980  phtpycc  19016  elovolm  19371  ovolgelb  19376  ovolicc1  19412  ovolicc  19419  ioorval  19466  uniioombllem6  19480  dyadmax  19490  dyadmbl  19492  i1fadd  19587  i1fmul  19588  itg1addlem3  19590  i1fmulc  19595  itg2l  19621  itg2leub  19626  limcmpt  19770  limcco  19780  dvcobr  19832  evlslem3  19935  deg1ldg  20015  ig1pval  20095  elply  20114  elply2  20115  coeval  20142  coe1termlem  20176  coe1term  20177  quotval  20209  plydivlem4  20213  plydivex  20214  vieta1  20229  aannenlem2  20246  aalioulem2  20250  abelthlem9  20356  logtayllem  20550  logtayl  20551  isosctrlem2  20663  atantayl2  20778  leibpilem2  20781  rlimcnp2  20805  efrlim  20808  dvdsmulf1o  20979  perfectlem2  21014  lgsfval  21085  lgsval2lem  21090  lgsdchrval  21131  2sqlem2  21148  2sqlem8  21156  2sqlem9  21157  2sqlem11  21159  dchrisum0flblem1  21202  padicval  21311  padicabv  21324  ostth1  21327  cusgrafilem2  21489  cusgrafi  21491  wlkntrllem3  21561  fargshiftf1  21624  fargshiftfo  21625  constr3trllem2  21638  vdusgraval  21678  gxval  21846  gxdi  21884  ismgm  21908  nvz  22158  nmosetn0  22266  nmoolb  22272  nmoubi  22273  nmlno0lem  22294  nmlno0i  22295  hvsubeq0  22570  hvaddcan  22572  normsub0  22638  norm1exi  22752  pjhval  22899  omlsii  22905  omlsi  22906  pjoml  22938  h1de2ci  23058  spansneleq  23072  h1datomi  23083  h1datom  23084  spansncv  23155  5oalem6  23161  pj11  23216  nmopsetn0  23368  nmfnsetn0  23381  nmoplb  23410  nmopub  23411  nmfnlb  23427  nmfnleub  23428  nmlnop0iALT  23498  nmlnop0  23501  lnopeq  23512  nmopun  23517  nmcexi  23529  branmfn  23608  pjnmopi  23651  pj3i  23711  atss  23849  atom1d  23856  chirred  23898  cdj3lem2  23938  elabreximd  23991  disjxpin  24028  fmptcof2  24076  xrge0iifcnv  24319  xrge0iifcv  24320  xrge0iifhom  24323  xrge0tmdOLD  24331  xrge0tmd  24332  esumc  24446  sconpi1  24926  cvmlift3lem2  25007  ghomf1olem  25105  relexp0  25129  relexpsucr  25130  relexpsucl  25132  rtrclreclem.trans  25146  prodmo  25262  fprod  25267  br8  25379  br6  25380  br4  25381  rdgprc0  25421  dfrdg2  25423  sltval2  25611  sltintdifex  25618  sltres  25619  dfbigcup2  25744  elsingles  25763  dfiota3  25768  brimageg  25772  brdomaing  25780  brrangeg  25781  dfrdg4  25795  tfrqfree  25796  elaltxp  25820  axpaschlem  25879  axlowdimlem15  25895  axlowdim  25900  funtransport  25965  fvtransport  25966  brsegle  26042  funray  26074  fvray  26075  funline  26076  fvline  26078  ellines  26086  linethru  26087  rankeq1o  26112  supaddc  26237  supadd  26238  mblfinlem1  26243  mblfinlem2  26244  mblfinlem3  26245  mblfinlem4  26246  ismblfin  26247  itg2addnclem  26256  itg2addnclem3  26258  itg2addnc  26259  ftc1anc  26288  subtr  26317  subtr2  26318  nn0prpw  26326  unirep  26414  f1opr  26426  sdclem2  26446  sdclem1  26447  sdc  26448  fdc  26449  isbnd  26489  heibor1lem  26518  heiborlem4  26523  heiborlem6  26525  heiborlem10  26529  maxidlmax  26653  prnc  26677  isfldidl  26678  dmnnzd  26685  elrfi  26748  nacsfg  26759  mzpcompact2lem  26808  eldioph2b  26821  eldioph3  26824  eldiophss  26833  diophrex  26834  elnn0rabdioph  26863  rencldnfilem  26881  elpell1qr  26910  elpell14qr  26912  elpell1234qr  26914  divalgmodcl  27058  jm2.27  27079  rmydioph  27085  expdiophlem2  27093  wepwsolem  27116  aomclem6  27134  uvcvval  27212  ellspd  27231  lnr2i  27297  lpirlnr  27298  hbtlem2  27305  hbtlem4  27307  hbtlem5  27309  rngunsnply  27355  flcidc  27356  psgneu  27406  psgnval  27407  psgnvali  27408  psgnvalii  27409  pm13.192  27587  refsum2cnlem1  27684  stoweidlem46  27771  afv0fv0  27989  afvfv0bi  27992  afvelrnb  28003  afvelrnb0  28004  otiunsndisj  28066  otiunsndisjX  28067  oprabv  28085  2ffzoeq  28140  euhash1  28167  reumodprminv  28227  cshwssizesame  28288  2wlkeq  28303  frgra3vlem1  28390  3vfriswmgralem  28394  frgrancvvdeqlem4  28422  2spotiundisj  28451  usgreghash2spotv  28455  frgregordn0  28459  sgnval  28518  equncomVD  28980  csbingVD  28996  csbsngVD  29005  csbfv12gALTVD  29011  relopabVD  29013  bnj1468  29217  lshpdisj  29785  lsat0cv  29831  lcvexchlem4  29835  lcvexchlem5  29836  lshpkrlem1  29908  lshpkrlem2  29909  lshpkrlem3  29910  lshpkrcl  29914  islshpkrN  29918  atnle  30115  glbconxN  30175  isline  30536  ispointN  30539  pmapglbx  30566  ispsubcl2N  30744  lhp2atnle  30830  cdleme43fsv1snlem  31217  cdleme40v  31266  cdlemkid5  31732  cdlemkid  31733  dvhb1dimN  31783  dib1dim  31963  dicopelval  31975  dicelval1sta  31985  diclspsn  31992  dihvalcqpre  32033  dihglblem2aN  32091  dihglblem2N  32092  dih1dimatlem  32127  dihpN  32134  dochfl1  32274  lcfl7N  32299  lcf1o  32349  hvmapvalvalN  32559  hdmapval2lem  32632
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 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator