Theorem eqeq1 2164

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 2151	. . . . . 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 1538	. . . 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 1804	. 2 |- ( A = B -> ( A. x ( x e. A <-> x e. C ) <-> A. x ( x e. B <-> x e. C ) ) )
6		dfcleq 2151	. 2 |- ( A = C <-> A. x ( x e. A <-> x e. C ) )
7		dfcleq 2151	. 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 1333   = wceq 1335   e. wcel 2128

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 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

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

This theorem is referenced by:  eqeq1i  2165  eqeq1d  2166  eqeq2  2167  eqeq12  2170  eqtr  2175  eqsb3lem  2260  clelab  2283  neeq1  2340  pm13.18  2408  issetf  2719  sbhypf  2761  vtoclgft  2762  eqvincf  2837  pm13.183  2850  eueq  2883  mob  2894  euind  2899  reuind  2917  eqsbc3  2976  csbhypf  3069  uniiunlem  3216  snjust  3565  elsng  3575  elprg  3580  rabrsndc  3627  sneqrg  3725  preq12bg  3736  intab  3836  dfiin2g  3882  exmidsssnc  4164  opthg  4198  copsexg  4204  euotd  4214  elopab  4218  snnex  4407  uniuni  4410  eusv1  4411  reusv3  4419  ordtriexmid  4479  ontriexmidim  4480  onsucelsucexmidlem1  4486  onsucelsucexmid  4488  regexmidlemm  4490  regexmidlem1  4491  reg2exmidlema  4492  wetriext  4535  nn0suc  4562  nndceq0  4576  0elnn  4577  elxpi  4601  opbrop  4664  relop  4735  ideqg  4736  elrnmpt  4834  elrnmpt1  4836  elrnmptg  4837  cnveqb  5040  relcoi1  5116  funopg  5203  funcnvuni  5238  f0rn0  5363  fun11iun  5434  fvelrnb  5515  fvmptg  5543  fndmin  5573  eldmrexrn  5607  fmptco  5632  foco2  5701  elabrex  5705  abrexco  5706  f1veqaeq  5716  f1oiso  5773  eusvobj2  5807  acexmidlema  5812  acexmidlemb  5813  acexmidlem2  5818  acexmidlemv  5819  oprabid  5850  mpofun  5920  elrnmpog  5930  elrnmpo  5931  ralrnmpo  5932  rexrnmpo  5933  ovi3  5954  ov6g  5955  ovelrn  5966  caovcang  5979  caovcan  5982  eloprabi  6141  dftpos4  6207  tfr1onlemaccex  6292  tfrcllemaccex  6305  elqsg  6527  qsel  6554  brecop  6567  eroveu  6568  erovlem  6569  th3qlem1  6579  th3q  6582  elixpsn  6677  ixpsnf1o  6678  2dom  6747  fundmen  6748  xpf1o  6786  nneneq  6799  tridc  6841  fisseneq  6873  fidcenumlemrks  6894  elfi  6912  supsnti  6946  isotilem  6947  updjudhcoinrg  7020  updjud  7021  omp1eom  7034  difinfsn  7039  ctmlemr  7047  ismkvnex  7093  omniwomnimkv  7105  exmidaclem  7138  exmidac  7139  onntri35  7167  indpi  7257  nqtri3or  7311  enq0sym  7347  enq0ref  7348  enq0tr  7349  enq0breq  7351  addnq0mo  7362  mulnq0mo  7363  mulnnnq0  7365  genipv  7424  genpelvl  7427  genpelvu  7428  addsrmo  7658  mulsrmo  7659  aptisr  7694  ltresr  7754  axcnre  7796  axpre-apti  7800  ltordlem  8352  apreap  8457  apreim  8473  aprcl  8516  sup3exmid  8823  creur  8825  creui  8826  nn1m1nn  8846  nn1gt1  8862  elz  9164  nn0ind-raph  9276  nltpnft  9713  xnegeq  9726  xrpnfdc  9741  xrmnfdc  9742  xleaddadd  9786  flqeqceilz  10212  1tonninf  10334  iseqf1olemqval  10381  iseqf1olemqk  10388  seq3f1olemqsum  10394  exp3val  10416  shftfvalg  10713  shftfval  10716  summodc  11275  fsum3  11279  telfsumo  11358  mertenslemub  11426  mertenslemi1  11427  mertenslem2  11428  mertensabs  11429  prodmodc  11470  fprodseq  11475  fprodcl2lem  11497  ndvdssub  11815  gcdval  11837  bezoutlemnewy  11874  bezoutlema  11877  bezoutlemb  11878  lcmval  11934  coprmgcdb  11959  coprmdvds1  11962  divgcdcoprmex  11973  dvdsprime  11993  nprm  11994  dvdsprm  12008  coprm  12013  qnumval  12054  qdenval  12055  ennnfonelemj0  12117  ennnfonelemjn  12118  ennnfonelem0  12121  ennnfonelemp1  12122  ennnfonelemnn0  12138  ennnfonelemim  12140  unct  12158  istopon  12398  toponsspwpwg  12407  epttop  12477  txuni2  12643  xmeteq0  12746  comet  12886  bj-charfunbi  13373  bj-nn0suc0  13512  bj-inf2vnlem1  13532  bj-inf2vnlem2  13533  bj-nn0sucALT  13540  exmid1stab  13559  subctctexmid  13560  pw1nct  13562  nnsf  13564  peano3nninf  13566  nninfall  13568  exmidsbthr  13581  trilpo  13601  trirec0  13602  redcwlpo  13613  redc0  13615  dceqnconst  13617