Theorem eqeq1 1481

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 1470	. . . . . 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 1060	. . . 4 |- (A = B -> (x e. A <-> x e. B))
4	3	bibi1d 619	. . 3 |- (A = B -> ((x e. A <-> x e. C) <-> (x e. B <-> x e. C)))
5	4	albidv 1278	. 2 |- (A = B -> (A.x(x e. A <-> x e. C) <-> A.x(x e. B <-> x e. C)))
6		dfcleq 1470	. 2 |- (A = C <-> A.x(x e. A <-> x e. C))
7		dfcleq 1470	. 2 |- (B = C <-> A.x(x e. B <-> x e. C))
8	5, 6, 7	3bitr4g 555	1 |- (A = B -> (A = C <-> B = C))

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

This theorem is referenced by:  eqeq1i 1482  eqeq1d 1483  eqeq2 1484  eqeq12 1487  eqtrt 1492  clelab 1581  neeq1 1590  vtoclgf 1846  cla4gf 1860  eqvinc 1883  eqvincf 1884  eueq 1916  moi 1925  reu3 1931  reu7 1935  sbhypf 1939  sbhyp 1940  uniiunlem 2132  elprg 2423  intab 2560  dfiun2g 2586  dfiin2 2588  opth 2787  opthgg 2789  copsexg 2792  elopab 2811  solin 2857  uniuni 2880  limeq 2960  orduninsuc 3114  opbrop 3238  relop 3275  ideqg 3276  funopg 3547  funcnvuni 3564  fnopabfv 3758  fvelrnb 3760  fvopab4g 3779  fvopabn 3786  eqfnfv 3797  abrexexlem2 3859  funiunfv 3866  f1fvf 3875  f1fveq 3876  isowe 3903  f1oiso 3904  f1oweALT 3906  tz7.44-1 3928  tz7.44-2 3929  tz7.44-3 3930  rdglem2 3938  eloprabg 4007  oprabval2gf 4026  oprabval3 4030  oprabval6g 4032  oprvalelrn 4039  caoprcan 4055  oev 4153  oalimcl 4194  omlimcl 4209  odi 4210  nneob 4255  elqs 4290  elqsi 4291  brecop 4306  eceqopreq 4313  th3qlem1 4314  th3q 4317  2dom 4427  fundmen 4428  pw2en 4446  xpmapenlem4 4499  nneneq 4512  abfii3OLD 4563  abfii4OLD 4564  tz9.12lem1 4659  tz9.12lem3 4661  scott0 4717  aceq3lem 4732  aceq5lem3 4737  aceq5lem4 4738  aceq6b 4742  ac6 4755  kmlem9 4773  kmlem12 4776  brdom7disj 4804  brdom6disj 4805  card1 4833  unxpdomlem 4843  cardiun 4859  alephval3 4903  cardcf 4911  cfeq0 4914  cfsuc 4915  ltsopq 5075  genpv 5102  genpelv 5103  genpprecl 5104  genpnnp 5108  prlem934b 5138  ltsosr 5203  ltresr 5258  ltsor 5261  axcnre 5286  addcant 5352  neg11t 5409  lesub0t 5678  mulcant2 5688  mulcant2OLD 5689  mul0ort 5696  div11t 5765  rec11 5778  eqnegt 5805  nnleltp1t 5954  elz 6137  nn0ind-raph 6214  elq 6257  seq1suclem 6316  fseqsupcl 6525  fseqsupub 6526  expvalt 6570  sq11t 6629  sqeqort 6649  nn0opth2t 6668  sqrlem21 6693  sqrlem22 6694  sqr00t 6714  crut 6738  revalt 6755  imvalt 6756  abs00t 6853  sumeq1 6982  climuni 7099  infcvgaux1 7219  infcvgaux2 7220  infcvglem1 7221  ef1tlub 7382  reef11t 7409  acdc3 7487  acdc2 7490  acdc5 7493  acdc 7495  ruclem12 7521  infxpidmlem2 7553  eltopsp 7604  tpsex 7605  istps 7606  eltg3t 7626  subbasOLD 7644  subbas2OLD 7645  subtop 7646  fctopOLD 7650  cctop 7652  meteq0 7812  dscmet 7918  nvz 8297  nmosetn0 8428  nmolb 8434  nmoubi 8435  nmlno0lem 8453  nmlno0i 8454  minveclem10 8554  minveclem14 8558  minvecex 8578  spwval2 8653  cosh111t 8717  efghgrpilem 8719  efifolem3 8724  circgrp 8740  hvsubeq0t 8935  hvaddcant 8937  normsub0t 9003  hlimuni 9109  norm1ex 9122  projlem8 9193  projlem10 9195  projlem13 9198  projlem15 9200  pjtht 9234  pjvalt 9239  omlsi 9245  omls 9246  pjomlt 9269  shselt 9278  h1de2ct 9479  spansneleq 9493  h1datom 9504  h1datomt 9505  spansncvt 9598  5oalem6 9604  pj11t 9659  eigortht 9764  nmopsetn0 9792  nmfnsetn0 9805  nmoplbt 9831  nmopubt 9832  nmfnlbt 9848  nmfnleubt 9849  nmlnop0ALT 9920  nmlnop0t 9923  lnopeqt 9934  nmopunt 9939  nmcopexlem1 9951  lnopcon 9963  nmcfnexlem1 9980  lnfncon 9990  branmfnt 10038  pjnmop 10075  pj3 10136  atss 10273  atom1d 10280  irredt 10322  cdj3lem2 10362  ghomf1olem 10396  elo 10444  spfi 10445  spfiOLD 10446  fiiu 10453  fiiuOLD 10454  cmpbva 10464  fiiu2 10488  fiiu2OLD 10489  bsi 10495  hmeogrp 10538  homcard 10539  fipfil2 10564  fipfil2OLD 10565  efilcp 10572  efilcpOLD 10573  fisub 10576  fisubOLD 10577  rcfpfillem1 10585  rcfpfillem1OLD 10586  rcfpfillem3 10589  rcfpfillem3OLD 10590  rcfpfillem6 10595  rcfpfillem6OLD 10596  rcfpfil 10597  rcfpfilOLD 10598  iint 10634  trnij 10637  cnvtr 10638  eloi 10659  ismonb2 10740  cmpmon 10743  isepib2 10750

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain