Theorem eqeq1 1528

Description: Equality implies equivalence of equalities.

Assertion

Ref	Expression
eqeq1	|- (A = B -> (A = C <-> B = C))

Proof of Theorem eqeq1

Step	Hyp	Ref	Expression
1		dfcleq 1516	. . . . . 6 |- (A = B <-> A.x(x e. A <-> x e. B))
2	1	biimpi 158	. . . . 5 |- (A = B -> A.x(x e. A <-> x e. B))
3	2	19.21bi 1101	. . . 4 |- (A = B -> (x e. A <-> x e. B))
4	3	bibi1d 630	. . 3 |- (A = B -> ((x e. A <-> x e. C) <-> (x e. B <-> x e. C)))
5	4	albidv 1320	. 2 |- (A = B -> (A.x(x e. A <-> x e. C) <-> A.x(x e. B <-> x e. C)))
6		dfcleq 1516	. 2 |- (A = C <-> A.x(x e. A <-> x e. C))
7		dfcleq 1516	. 2 |- (B = C <-> A.x(x e. B <-> x e. C))
8	5, 6, 7	3bitr4g 566	1 |- (A = B -> (A = C <-> B = C))

Syntax hints:   -> wi 3   <-> wb 153  A.wal 995   = wceq 997   e. wcel 999

This theorem is referenced by:  eqeq1i 1529  eqeq1d 1530  eqeq2 1531  eqeq12 1534  eqtr 1539  clelab 1628  neeq1 1637  vtoclgf 1893  cla4gf 1907  eqvinc 1930  eqvincf 1931  eueq 1963  moi 1972  reu3 1978  reu7 1982  sbhypf 1986  sbhyp 1987  cbvsbcv 2007  uniiunlem 2183  elprg 2475  intab 2614  dfiun2g 2640  dfiin2 2642  opth 2843  opthgg 2845  copsexg 2848  elopab 2867  solin 2913  snnex 2933  uniuni 2937  limeq 3017  orduninsuc 3171  opbrop 3295  relop 3332  ideqg 3333  funopg 3604  funcnvuni 3621  fnopabfv 3815  fvelrnb 3817  fvopab4g 3836  fvopabn 3843  eqfnfv 3854  abrexexlem2 3916  funiunfv 3923  f1fvf 3932  f1fveq 3934  isowe 3961  f1oiso 3962  f1oweALT 3964  tz7.44-1 3986  tz7.44-2 3987  tz7.44-3 3988  rdglem2 3996  eloprabg 4065  oprabval2gf 4084  oprabval3 4088  oprabval6g 4090  oprvalelrn 4097  caoprcan 4113  oev 4211  oalimcl 4252  omlimcl 4267  odi 4268  nneob 4313  elqs 4348  elqsOLD 4349  elqsi 4350  elqsiOLD 4351  brecop 4367  eceqopreq 4374  th3qlem1 4375  th3q 4378  2dom 4488  fundmen 4489  pw2en 4509  xpmapenlem4 4564  nneneq 4577  abfii3 4623  abfii4 4624  tz9.12lem1 4721  tz9.12lem3 4723  scott0 4779  aceq3lem 4794  aceq5lem3 4799  aceq5lem4 4800  aceq6b 4804  ac6 4817  kmlem9 4835  kmlem12 4838  brdom7disj 4866  brdom6disj 4867  card1 4896  unxpdomlem 4908  cardiun 4924  alephval3 4968  cardcf 4976  cfeq0 4979  cfsuc 4980  ltsopq 5140  genpv 5167  genpelv 5168  genpprecl 5169  genpnnp 5173  prlem934b 5203  ltsosr 5268  ltresr 5323  ltsor 5326  axcnre 5351  addcan 5417  neg11 5474  lesub0 5743  mulcant2i 5753  mulcant2iOLD 5754  mul0or 5761  div11 5822  rec11i 5836  eqneg 5863  nnleltp1 6015  elz 6219  nn0ind-raph 6299  elq 6309  fseqsupcl 6551  fseqsupubi 6552  seq1suclem 6575  expval 6659  sq11 6718  sqeqor 6738  nn0opth2 6758  sqrlem21 6783  sqrlem22 6784  sqr00 6804  cru 6828  reval 6845  imval 6846  abs00 6943  sumeq1 7072  climuni 7189  infcvgaux1i 7309  infcvgaux2i 7310  infcvglem1 7311  ef1tlubi 7472  reef11 7500  acdc3 7579  acdc2 7582  acdc5 7585  acdc 7587  ruclem12 7613  infxpidmlem2 7645  eltopsp 7695  tpsex 7696  istps 7697  eltg3 7715  subtop 7733  cctop 7737  meteq0 7897  dscmet 8003  nvz 8381  nmosetn0 8512  nmolb 8518  nmoubi 8519  nmlno0lem 8537  nmlno0i 8538  minveclem10 8638  minveclem14 8642  minvecex 8662  spwval2 8737  cosh111 8800  efghgrpilem 8802  efifolem3 8807  circgrp 8823  hvsubeq0 9018  hvaddcan 9020  normsub0 9086  hlimunii 9192  norm1exi 9205  projlem8 9276  projlem10 9278  projlem13 9281  projlem15 9283  pjth 9317  pjval 9322  omlsii 9328  omlsi 9329  pjoml 9352  shsel 9361  h1de2ci 9562  spansneleq 9576  h1datomi 9587  h1datom 9588  spansncv 9681  5oalem6 9687  pj11 9742  eigorth 9847  nmopsetn0 9875  nmfnsetn0 9888  nmoplb 9914  nmopub 9915  nmfnlb 9931  nmfnleub 9932  nmlnop0iALT 10003  nmlnop0 10006  lnopeq 10017  nmopun 10022  nmcopexlem1 10034  lnopconi 10046  nmcfnexlem1 10063  lnfnconi 10073  branmfn 10121  pjnmopi 10158  pj3i 10220  atss 10357  atom1d 10364  irred 10406  cdj3lem2 10446  ghomf1olem 10481  elo 10530  spfi 10531  fiiu 10535  cmpbva 10545  fiiu2 10574  bsi 10589  hmeogrp 10632  homcard 10633  fipfil2 10658  efilcp 10664  fisub 10666  rcfpfillem1 10671  rcfpfillem3 10673  rcfpfillem6 10676  rcfpfil 10677  iint 10716  trnij 10719  cnvtr 10720  eloi 10741  ismonb2 10822  cmpmon 10825  isepib2 10832

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-cleq 1515

Copyright terms: Public domain