Theorem eqeq1 2200

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 2187	. . . . . 6 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
2	1	biimpi 120	. . . . 5 |- ( A = B -> A. x ( x e. A <-> x e. B ) )
3	2	19.21bi 1569	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
4	3	bibi1d 233	. . 3 |- ( A = B -> ( ( x e. A <-> x e. C ) <-> ( x e. B <-> x e. C ) ) )
5	4	albidv 1835	. 2 |- ( A = B -> ( A. x ( x e. A <-> x e. C ) <-> A. x ( x e. B <-> x e. C ) ) )
6		dfcleq 2187	. 2 |- ( A = C <-> A. x ( x e. A <-> x e. C ) )
7		dfcleq 2187	. 2 |- ( B = C <-> A. x ( x e. B <-> x e. C ) )
8	5, 6, 7	3bitr4g 223	1 |- ( A = B -> ( A = C <-> B = C ) )

Syntax hints:   -> wi 4   <-> wb 105   A.wal 1362   = wceq 1364   e. wcel 2164

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186

This theorem is referenced by:  eqeq1i  2201  eqeq1d  2202  eqeq2  2203  eqeq12  2206  eqtr  2211  eqsb1lem  2296  clelab  2319  neeq1  2377  pm13.18  2445  issetf  2767  sbhypf  2810  vtoclgft  2811  eqvincf  2886  pm13.183  2899  eueq  2932  mob  2943  euind  2948  reuind  2966  eqsbc1  3026  csbhypf  3120  uniiunlem  3269  snjust  3624  elsng  3634  elprg  3639  rabrsndc  3687  sneqrg  3789  preq12bg  3800  intab  3900  dfiin2g  3946  exmidsssnc  4233  exmid1stab  4238  opthg  4268  copsexg  4274  euotd  4284  elopab  4289  snnex  4480  uniuni  4483  eusv1  4484  reusv3  4492  ordtriexmid  4554  ontriexmidim  4555  onsucelsucexmidlem1  4561  onsucelsucexmid  4563  regexmidlemm  4565  regexmidlem1  4566  reg2exmidlema  4567  wetriext  4610  nn0suc  4637  nndceq0  4651  0elnn  4652  elxpi  4676  opbrop  4739  relop  4813  ideqg  4814  elrnmpt  4912  elrnmpt1  4914  elrnmptg  4915  restidsing  4999  cnveqb  5122  relcoi1  5198  funopg  5289  funcnvuni  5324  f0rn0  5449  fun11iun  5522  fvelrnb  5605  fvmptg  5634  fndmin  5666  eldmrexrn  5700  fmptco  5725  foco2  5797  elabrex  5801  elabrexg  5802  abrexco  5803  f1veqaeq  5813  f1oiso  5870  eusvobj2  5905  acexmidlema  5910  acexmidlemb  5911  acexmidlem2  5916  acexmidlemv  5917  oprabid  5951  mpofun  6021  elrnmpog  6032  elrnmpo  6033  ralrnmpo  6034  rexrnmpo  6035  ovi3  6057  ov6g  6058  ovelrn  6069  caovcang  6082  caovcan  6085  eloprabi  6251  dftpos4  6318  tfr1onlemaccex  6403  tfrcllemaccex  6416  elqsg  6641  qsel  6668  brecop  6681  eroveu  6682  erovlem  6683  th3qlem1  6693  th3q  6696  elixpsn  6791  ixpsnf1o  6792  2dom  6861  fundmen  6862  xpf1o  6902  nneneq  6915  tridc  6957  fisseneq  6990  fidcenumlemrks  7014  elfi  7032  supsnti  7066  isotilem  7067  updjudhcoinrg  7142  updjud  7143  omp1eom  7156  difinfsn  7161  ctmlemr  7169  ismkvnex  7216  omniwomnimkv  7228  nninfwlpoimlemginf  7237  nninfwlpoimlemdc  7238  exmidaclem  7270  exmidac  7271  onntri35  7299  exmidapne  7322  indpi  7404  nqtri3or  7458  enq0sym  7494  enq0ref  7495  enq0tr  7496  enq0breq  7498  addnq0mo  7509  mulnq0mo  7510  mulnnnq0  7512  genipv  7571  genpelvl  7574  genpelvu  7575  addsrmo  7805  mulsrmo  7806  aptisr  7841  ltresr  7901  axcnre  7943  axpre-apti  7947  ltordlem  8503  apreap  8608  apreim  8624  aprcl  8667  aptap  8671  sup3exmid  8978  creur  8980  creui  8981  nn1m1nn  9002  nn1gt1  9018  elz  9322  nn0ind-raph  9437  nltpnft  9883  xnegeq  9896  xrpnfdc  9911  xrmnfdc  9912  xleaddadd  9956  flqeqceilz  10392  1tonninf  10515  iseqf1olemqval  10574  iseqf1olemqk  10581  seq3f1olemqsum  10587  exp3val  10615  shftfvalg  10965  shftfval  10968  summodc  11529  fsum3  11533  telfsumo  11612  mertenslemub  11680  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  prodmodc  11724  fprodseq  11729  fprodcl2lem  11751  ndvdssub  12074  gcdval  12099  bezoutlemnewy  12136  bezoutlema  12139  bezoutlemb  12140  lcmval  12204  coprmgcdb  12229  coprmdvds1  12232  divgcdcoprmex  12243  dvdsprime  12263  nprm  12264  dvdsprm  12278  coprm  12285  qnumval  12326  qdenval  12327  m1dvdsndvds  12389  reumodprminv  12394  pceu  12436  pcval  12437  pczpre  12438  pcdiv  12443  4sqlem2  12530  4sqlem4  12533  4sqlemafi  12536  4sqexercise1  12539  4sqexercise2  12540  4sqlemsdc  12541  4sqlem12  12543  4sq  12551  ennnfonelemj0  12561  ennnfonelemjn  12562  ennnfonelem0  12565  ennnfonelemp1  12566  ennnfonelemnn0  12582  ennnfonelemim  12584  unct  12602  gsum0g  12982  gsumval2  12983  ghmf1  13346  rrgeq0i  13763  domneq0  13771  lss1d  13882  lspsn  13915  ellspsn  13916  znf1o  14150  znidom  14156  znunit  14158  istopon  14192  toponsspwpwg  14201  epttop  14269  txuni2  14435  xmeteq0  14538  comet  14678  elply  14913  elply2  14914  lgsval  15161  lgsfvalg  15162  lgsval2lem  15167  gausslemma2dlem0i  15214  2lgslem1b  15246  2lgslem3  15258  2sqlem2  15272  2sqlem8  15280  2sqlem9  15281  bj-charfunbi  15373  bj-nn0suc0  15512  bj-inf2vnlem1  15532  bj-inf2vnlem2  15533  bj-nn0sucALT  15540  subctctexmid  15561  pw1nct  15563  nnsf  15565  peano3nninf  15567  nninfall  15569  exmidsbthr  15583  trilpo  15603  trirec0  15604  redcwlpo  15615  redc0  15617  dceqnconst  15620