Theorem eqeq1 1478

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 1468	. . . . . 6 |- (A = B <-> A.x(x e. A <-> x e. B))
2	1	biimp 151	. . . . 5 |- (A = B -> A.x(x e. A <-> x e. B))
3	2	19.21bi 1058	. . . 4 |- (A = B -> (x e. A <-> x e. B))
4	3	bibi1d 618	. . 3 |- (A = B -> ((x e. A <-> x e. C) <-> (x e. B <-> x e. C)))
5	4	albidv 1276	. 2 |- (A = B -> (A.x(x e. A <-> x e. C) <-> A.x(x e. B <-> x e. C)))
6		dfcleq 1468	. 2 |- (A = C <-> A.x(x e. A <-> x e. C))
7		dfcleq 1468	. 2 |- (B = C <-> A.x(x e. B <-> x e. C))
8	5, 6, 7	3bitr4g 554	1 |- (A = B -> (A = C <-> B = C))

Syntax hints:   -> wi 3   <-> wb 146  A.wal 952   = wceq 954   e. wcel 956

This theorem is referenced by:  eqeq1i 1479  eqeq1d 1480  eqeq2 1481  eqeq12 1484  eqtrt 1489  clelab 1578  neeq1 1587  vtoclgf 1842  cla4gf 1856  eqvinc 1879  eqvincf 1880  eueq 1912  moi 1921  reu3 1927  reu7 1931  sbhypf 1935  sbhyp 1936  uniiunlem 2128  elprg 2419  intab 2555  dfiun2g 2581  dfiin2 2583  opth 2782  opthgg 2784  copsexg 2787  elopab 2806  solin 2852  uniuni 2875  limeq 2955  orduninsuc 3109  opbrop 3233  relop 3270  ideqg 3271  funopg 3539  funcnvuni 3556  fnopabfv 3749  fvelrnb 3751  fvopab4g 3770  fvopabn 3777  eqfnfv 3788  abrexexlem2 3850  funiunfv 3857  f1fvf 3866  f1fveq 3867  isowe 3894  f1oiso 3895  f1oweALT 3897  tz7.44-1 3919  tz7.44-2 3920  tz7.44-3 3921  rdglem2 3929  eloprabg 3998  oprabval2gf 4017  oprabval3 4021  oprabval6g 4023  oprvalelrn 4030  caoprcan 4047  oev 4143  oalimcl 4184  omlimcl 4199  odi 4200  nneob 4245  elqs 4280  elqsi 4281  brecop 4296  eceqopreq 4303  th3qlem1 4304  th3q 4307  2dom 4414  fundmen 4415  pw2en 4432  xpmapenlem4 4485  nneneq 4498  abfii3 4543  abfii4 4544  tz9.12lem1 4639  tz9.12lem3 4641  scott0 4697  aceq3lem 4712  aceq5lem3 4717  aceq5lem4 4718  aceq6b 4722  ac6 4735  kmlem9 4753  kmlem12 4756  brdom7disj 4784  brdom6disj 4785  card1 4813  unxpdomlem 4823  cardiun 4839  alephval3 4883  cardcf 4891  cfeq0 4894  cfsuc 4895  ltsopq 5055  genpv 5082  genpelv 5083  genpprecl 5084  genpnnp 5088  prlem934b 5118  ltsosr 5183  ltresr 5238  ltsor 5241  axcnre 5266  addcant 5332  neg11t 5389  lesub0t 5659  mulcant2 5668  mul0ort 5673  div11t 5729  rec11 5742  eqnegt 5769  nnleltp1t 5909  elz 6092  nn0ind-raph 6170  elq 6203  seq1suclem 6261  fseqsupcl 6465  fseqsupub 6466  expvalt 6510  sq0t 6558  sq11t 6568  sqeqort 6588  nn0opth2t 6606  sqrlem21 6631  sqrlem22 6632  sqr00t 6652  crut 6676  revalt 6694  imvalt 6695  abs00t 6796  sumeq1 6928  climuni 7044  infcvgaux1 7162  infcvgaux2 7163  infcvglem1 7164  ef1tlub 7332  reeff1 7358  acdc3 7437  acdc2 7440  acdc5 7443  acdc 7445  ruclem12 7472  infxpidmlem2 7504  eltopsp 7554  tpsex 7555  istps 7556  eltg3t 7576  subbas 7594  subbas2 7595  subtop 7596  fctop 7600  cctop 7602  meteq0 7762  dscmet 7870  nvz 8249  nmosetn0 8373  nmolb 8379  nmoubi 8380  nmlno0lem 8398  nmlno0i 8399  minveclem10 8498  minveclem14 8502  minvecex 8522  spwval2 8595  cosh111t 8651  efghgrpilem 8653  efifolem3 8658  circgrp 8679  hvsubeq0t 8874  hvaddcant 8876  normsub0t 8942  hlimuni 9048  norm1ex 9061  projlem8 9132  projlem10 9134  projlem13 9137  projlem15 9139  pjtht 9172  pjvalt 9177  omlsi 9183  omls 9184  pjomlt 9207  shselt 9216  h1de2ct 9418  spansneleq 9432  spansneleqOLD 9433  h1datom 9444  h1datomt 9445  spansncvt 9538  5oalem6 9544  pj11t 9599  eigortht 9704  nmopsetn0 9732  nmfnsetn0 9745  nmoplbt 9771  nmopubt 9772  nmfnlbt 9787  nmfnleubt 9788  nmlnop0ALT 9858  nmlnop0t 9861  lnopeqt 9872  nmopunt 9877  nmcopexlem1 9889  lnopcon 9901  nmcfnexlem1 9918  lnfncon 9928  branmfnt 9976  pjnmop 10013  pj3 10074  atss 10210  atom1d 10217  irredt 10259  cdj3lem2 10296  ghomf1olem 10330  elo 10381  spfi 10382  fiiu 10386  cmpbva 10396  fiiu2 10413  bsi 10418  hmeogrp 10461  homcard 10462  fipfil2 10475  efilcp 10481  fisub 10483  iint 10514  trnij 10517  cnvtr 10518  eloi 10539  ismonb2 10618  cmpmon 10621

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1467

Copyright terms: Public domain