Theorem eqeq1 2146

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 2133	. . . . . 6 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
2	1	biimpi 119	. . . . 5 |- ( A = B -> A. x ( x e. A <-> x e. B ) )
3	2	19.21bi 1537	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
4	3	bibi1d 232	. . 3 |- ( A = B -> ( ( x e. A <-> x e. C ) <-> ( x e. B <-> x e. C ) ) )
5	4	albidv 1796	. 2 |- ( A = B -> ( A. x ( x e. A <-> x e. C ) <-> A. x ( x e. B <-> x e. C ) ) )
6		dfcleq 2133	. 2 |- ( A = C <-> A. x ( x e. A <-> x e. C ) )
7		dfcleq 2133	. 2 |- ( B = C <-> A. x ( x e. B <-> x e. C ) )
8	5, 6, 7	3bitr4g 222	1 |- ( A = B -> ( A = C <-> B = C ) )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1329   = wceq 1331   e. wcel 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  eqeq1i  2147  eqeq1d  2148  eqeq2  2149  eqeq12  2152  eqtr  2157  eqsb3lem  2242  clelab  2265  neeq1  2321  pm13.18  2389  issetf  2693  sbhypf  2735  vtoclgft  2736  eqvincf  2810  pm13.183  2822  eueq  2855  mob  2866  euind  2871  reuind  2889  eqsbc3  2948  csbhypf  3038  uniiunlem  3185  snjust  3532  elsng  3542  elprg  3547  rabrsndc  3591  sneqrg  3689  preq12bg  3700  intab  3800  dfiin2g  3846  exmidsssnc  4126  opthg  4160  copsexg  4166  euotd  4176  elopab  4180  snnex  4369  uniuni  4372  eusv1  4373  reusv3  4381  ordtriexmid  4437  onsucelsucexmidlem1  4443  onsucelsucexmid  4445  regexmidlemm  4447  regexmidlem1  4448  reg2exmidlema  4449  wetriext  4491  nn0suc  4518  nndceq0  4531  0elnn  4532  elxpi  4555  opbrop  4618  relop  4689  ideqg  4690  elrnmpt  4788  elrnmpt1  4790  elrnmptg  4791  cnveqb  4994  relcoi1  5070  funopg  5157  funcnvuni  5192  f0rn0  5317  fun11iun  5388  fvelrnb  5469  fvmptg  5497  fndmin  5527  eldmrexrn  5561  fmptco  5586  foco2  5655  elabrex  5659  abrexco  5660  f1veqaeq  5670  f1oiso  5727  eusvobj2  5760  acexmidlema  5765  acexmidlemb  5766  acexmidlem2  5771  acexmidlemv  5772  oprabid  5803  mpofun  5873  elrnmpog  5883  elrnmpo  5884  ralrnmpo  5885  rexrnmpo  5886  ovi3  5907  ov6g  5908  ovelrn  5919  caovcang  5932  caovcan  5935  eloprabi  6094  dftpos4  6160  tfr1onlemaccex  6245  tfrcllemaccex  6258  elqsg  6479  qsel  6506  brecop  6519  eroveu  6520  erovlem  6521  th3qlem1  6531  th3q  6534  elixpsn  6629  ixpsnf1o  6630  2dom  6699  fundmen  6700  xpf1o  6738  nneneq  6751  tridc  6793  fisseneq  6820  fidcenumlemrks  6841  elfi  6859  supsnti  6892  isotilem  6893  updjudhcoinrg  6966  updjud  6967  omp1eom  6980  difinfsn  6985  ctmlemr  6993  ismkvnex  7029  exmidaclem  7064  exmidac  7065  indpi  7150  nqtri3or  7204  enq0sym  7240  enq0ref  7241  enq0tr  7242  enq0breq  7244  addnq0mo  7255  mulnq0mo  7256  mulnnnq0  7258  genipv  7317  genpelvl  7320  genpelvu  7321  addsrmo  7551  mulsrmo  7552  aptisr  7587  ltresr  7647  axcnre  7689  axpre-apti  7693  ltordlem  8244  apreap  8349  apreim  8365  aprcl  8408  sup3exmid  8715  creur  8717  creui  8718  nn1m1nn  8738  nn1gt1  8754  elz  9056  nn0ind-raph  9168  nltpnft  9597  xnegeq  9610  xrpnfdc  9625  xrmnfdc  9626  xleaddadd  9670  flqeqceilz  10091  1tonninf  10213  iseqf1olemqval  10260  iseqf1olemqk  10267  seq3f1olemqsum  10273  exp3val  10295  shftfvalg  10590  shftfval  10593  summodc  11152  fsum3  11156  telfsumo  11235  mertenslemub  11303  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  prodmodc  11347  ndvdssub  11627  gcdval  11648  bezoutlemnewy  11684  bezoutlema  11687  bezoutlemb  11688  lcmval  11744  coprmgcdb  11769  coprmdvds1  11772  divgcdcoprmex  11783  dvdsprime  11803  nprm  11804  dvdsprm  11817  coprm  11822  qnumval  11863  qdenval  11864  ennnfonelemj0  11914  ennnfonelemjn  11915  ennnfonelem0  11918  ennnfonelemp1  11919  ennnfonelemnn0  11935  ennnfonelemim  11937  unct  11954  istopon  12180  toponsspwpwg  12189  epttop  12259  txuni2  12425  xmeteq0  12528  comet  12668  bj-nn0suc0  13148  bj-inf2vnlem1  13168  bj-inf2vnlem2  13169  bj-nn0sucALT  13176  exmid1stab  13195  subctctexmid  13196  nnsf  13199  peano3nninf  13201  nninfall  13204  exmidsbthr  13218  trilpo  13236