Theorem eqeq1 2359

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.

Step	Hyp	Ref	Expression
1		dfcleq 2347	. . . . . 6 |- (A = B <-> A.x(x e. A <-> x e. B))
2	1	biimpi 186	. . . . 5 |- (A = B -> A.x(x e. A <-> x e. B))
3	2	19.21bi 1758	. . . 4 |- (A = B -> (x e. A <-> x e. B))
4	3	bibi1d 310	. . 3 |- (A = B -> ((x e. A <-> x e. C) <-> (x e. B <-> x e. C)))
5	4	albidv 1625	. 2 |- (A = B -> (A.x(x e. A <-> x e. C) <-> A.x(x e. B <-> x e. C)))
6		dfcleq 2347	. 2 |- (A = C <-> A.x(x e. A <-> x e. C))
7		dfcleq 2347	. 2 |- (B = C <-> A.x(x e. B <-> x e. C))
8	5, 6, 7	3bitr4g 279	1 |- (A = B -> (A = C <-> B = C))

Syntax hints:   -> wi 4   <-> wb 176  A.wal 1540   = wceq 1642   e. wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  eqeq1i  2360  eqeq1d  2361  eqeq2  2362  eqeq12  2365  eqtr  2370  eqsb3lem  2453  clelab  2473  neeq1  2524  pm13.18  2588  issetf  2864  sbhypf  2904  vtoclgft  2905  eqvincf  2967  pm13.183  2979  eueq  3008  mob  3018  euind  3023  reu6  3025  reu7  3031  reuind  3039  eqsbc3  3085  csbhypf  3171  uniiunlem  3353  snjust  3740  elprg  3750  elsncg  3755  sneqrg  3874  intab  3956  uniintsn  3963  dfiin2g  4000  pwadjoin  4119  preqr2g  4126  preq12bg  4128  el1c  4139  elxpk  4196  opkelopkabg  4245  opkelins2kg  4251  opkelins3kg  4252  opkelsikg  4264  sikss1c1c  4267  opkelidkg  4274  eladdc  4398  0nelsuc  4400  nnc0suc  4412  nndisjeq  4429  opklefing  4448  opkltfing  4449  leltfintr  4458  lefinlteq  4463  ltfintri  4466  tfineq  4488  tfin11  4493  0ceven  4505  evennn  4506  oddnn  4507  evennnul  4508  oddnnul  4509  sucevenodd  4510  sucoddeven  4511  evenodddisjlem1  4515  evenodddisj  4516  eventfin  4517  oddtfin  4518  nnadjoin  4520  nnadjoinpw  4521  tfinnn  4534  vfinncvntsp  4549  vfinspsslem1  4550  vfinspss  4551  dfphi2  4569  phi11lem1  4595  0cnelphi  4597  proj1op  4600  proj2op  4601  copsexg  4607  phialllem1  4616  elopab  4696  br1stg  4730  brsi  4761  elxpi  4800  opbrop  4841  br1st  4858  br2nd  4859  brswap2  4860  ideqg  4868  ideqg2  4869  funcnvuni  5161  fun11iun  5305  dffn5  5363  fvelrnb  5365  fvopab4t  5385  fvopab4g  5388  eqfnfv  5392  fnasrn  5417  foelrn  5425  foco2  5426  abrexco  5463  funiunfv  5467  dff13f  5472  f1fveq  5473  f1oiso  5499  brswap  5509  funsi  5520  oprabid  5550  eloprabga  5578  ov3  5599  ov6g  5600  ovelrn  5608  caovcan  5628  brsnsi  5773  brtxp  5783  op1st2nd  5790  fnpprod  5843  extd  5923  antid  5929  elqsg  5976  qsdisj  5995  ncseqnc  6128  ncspw1eu  6159  eqtc  6161  nc0le1  6216  taddc  6229  letc  6231  ce0t  6232  ce0lenc1  6239  muc0or  6252  csucex  6259  brcsuc  6260  addccan2nclem1  6263  addccan2nclem2  6264  nncdiv3  6277  nnc3n3p1  6278  spaccl  6286  spacind  6287  nchoicelem3  6291  nchoicelem12  6300  nchoicelem16  6304  frecsuc  6322  scancan  6331