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  eqsb1lem  2453  clelab  2474  neeq1  2525  pm13.18  2589  issetf  2865  sbhypf  2905  vtoclgft  2906  eqvincf  2968  pm13.183  2980  eueq  3009  mob  3019  euind  3024  reu6  3026  reu7  3032  reuind  3040  eqsbc1  3086  csbhypf  3172  uniiunlem  3354  snjust  3741  elprg  3751  elsncg  3756  sneqrg  3875  intab  3957  uniintsn  3964  dfiin2g  4001  pwadjoin  4120  preqr2g  4127  preq12bg  4129  el1c  4140  elxpk  4197  opkelopkabg  4246  opkelins2kg  4252  opkelins3kg  4253  opkelsikg  4265  sikss1c1c  4268  opkelidkg  4275  eladdc  4399  0nelsuc  4401  nnc0suc  4413  nndisjeq  4430  opklefing  4449  opkltfing  4450  leltfintr  4459  lefinlteq  4464  ltfintri  4467  tfineq  4489  tfin11  4494  0ceven  4506  evennn  4507  oddnn  4508  evennnul  4509  oddnnul  4510  sucevenodd  4511  sucoddeven  4512  evenodddisjlem1  4516  evenodddisj  4517  eventfin  4518  oddtfin  4519  nnadjoin  4521  nnadjoinpw  4522  tfinnn  4535  vfinncvntsp  4550  vfinspsslem1  4551  vfinspss  4552  dfphi2  4570  phi11lem1  4596  0cnelphi  4598  proj1op  4601  proj2op  4602  copsexg  4608  phialllem1  4617  elopab  4697  br1stg  4731  brsi  4762  elxpi  4801  opbrop  4842  br1st  4859  br2nd  4860  brswap2  4861  ideqg  4869  ideqg2  4870  funcnvuni  5162  fun11iun  5306  dffn5  5364  fvelrnb  5366  fvopab4t  5386  fvopab4g  5389  eqfnfv  5393  fnasrn  5418  foelrn  5426  foco2  5427  abrexco  5464  funiunfv  5468  dff13f  5473  f1fveq  5474  f1oiso  5500  brswap  5510  funsi  5521  oprabid  5551  eloprabga  5579  ov3  5600  ov6g  5601  ovelrn  5609  caovcan  5629  brsnsi  5774  brtxp  5784  op1st2nd  5791  fnpprod  5844  extd  5924  antid  5930  elqsg  5977  qsdisj  5996  ncseqnc  6129  ncspw1eu  6160  eqtc  6162  nc0le1  6217  taddc  6230  letc  6232  ce0t  6233  ce0lenc1  6240  muc0or  6253  csucex  6260  brcsuc  6261  addccan2nclem1  6264  addccan2nclem2  6265  nncdiv3  6278  nnc3n3p1  6279  spaccl  6287  spacind  6288  nchoicelem3  6292  nchoicelem12  6301  nchoicelem16  6305  frecsuc  6323  scancan  6332