Theorem cleq1 1107

Description: Equality implies equivalence of equalities.

Assertion

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

Proof of Theorem cleq1

Step	Hyp	Ref	Expression
1		dfcleq 1098	. . . . . 6 |- (A = B <-> A.x(x e. A <-> x e. B))
2	1	biimp 133	. . . . 5 |- (A = B -> A.x(x e. A <-> x e. B))
3	2	19.21bi 742	. . . 4 |- (A = B -> (x e. A <-> x e. B))
4	3	bibi1d 471	. . 3 |- (A = B -> ((x e. A <-> x e. C) <-> (x e. B <-> x e. C)))
5	4	bialdv 935	. 2 |- (A = B -> (A.x(x e. A <-> x e. C) <-> A.x(x e. B <-> x e. C)))
6		dfcleq 1098	. 2 |- (A = C <-> A.x(x e. A <-> x e. C))
7		dfcleq 1098	. 2 |- (B = C <-> A.x(x e. B <-> x e. C))
8	5, 6, 7	3bitr4g 428	1 |- (A = B -> (A = C <-> B = C))

Syntax hints:   -> wi 2   <-> wb 127  A.wal 672   = wceq 1091   e. wcel 1092

This theorem is referenced by:  cleq1i 1108  cleq1d 1109  cleq2 1110  cleq12 1113  cleqtr 1118  clelab 1187  neeq1 1194  vtoclgf 1382  cla4gf 1394  eqvinc 1407  eqvincf 1408  eueq 1427  vsbcint 1438  elprg 1822  nnullss 1880  0inp0 1888  opth 1898  copsexg 1902  dfiun2 2014  dfiin2 2015  elopab 2110  ideqg 2126  solin 2145  fri 2170  frc 2172  limeq 2211  orduninsuc 2365  opbrop 2472  funcnvuni 2706  tz6.12i 2847  fnopabfv 2858  fvopab4g 2870  fvopabn 2873  cleqfv 2880  abrexexlem2 2911  f1fvf 2917  f1fveq 2918  isofrlem 2939  isowe 2941  f1oiso 2942  f1oweOLD 2944  tz7.44-1 2966  tz7.44-2 2967  tz7.44-3 2968  rdglem2 2976  eloprabg 3035  oprabval2g 3050  oprabval3 3052  caoprcan 3069  oev 3122  oalimcl 3162  elqs 3227  elqsi 3228  brecop 3242  eceqopreq 3249  th3qlem1 3250  th3q 3253  2dom 3332  fundmen 3333  pw2en 3348  xpmapenlem4 3394  nneneq 3408  fiint 3445  tz9.12lem1 3503  tz9.12lem3 3505  scott0 3542  aceq3lem 3555  aceq5lem3 3560  aceq5lem4 3561  aceq5 3563  aceq6b 3565  ac6 3576  kmlem1 3580  kmlem8 3587  kmlem11 3590  kmlem14 3593  numthlem 3598  unxpdomlem 3649  cardiun 3665  cardcf 3706  cfsuc 3709  ltsopq 3869  genpv 3896  genpelv 3897  genpprecl 3898  genpnnp 3902  prlem934b 3932  ltsosr 3997  ltresr 4052  ltsor 4055  axcnre 4087  addcant 4122  subeq0t 4169  mulcant 4208  mul0ort 4212  rec11 4262  lesub0t 4374  ltsqt 4376  nnleltp1t 4448  crut 4531  elz 4565  nn0ind 4612  elq 4629  seqsuclem 4669  sqe11t 4705  nn0opth2t 4726  sqrlem21 4751  sqrlem22 4752  sqr00t 4770  revalt 4794  imvalt 4795  absgt0t 4863  climuni 4884  ruclem12 4896  infxpidmlem2 4934  hvsubeq0t 5040  normsub0t 5085  hlimuni 5144  chocuni 5179  projlem8 5200  projlem10 5202  projlem13 5205  projlem15 5207  pjtht 5240  pjvalt 5246  omlsi 5250  omls 5251  shselt 5280  shintclt 5295  chintclt 5297  chne0t 5452  h1de2ct 5461  elspansn2t 5472  spansneleq 5475  h1datom 5483  h1datomt 5484  spansncvt 5543  5oalem6 5549  3oalem2 5553  pj3 5660  atss 5744  atom1d 5750

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org