Theorem eqeq1 2238

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 2225	. . . . . 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 1606	. . . 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 1872	. 2 |- ( A = B -> ( A. x ( x e. A <-> x e. C ) <-> A. x ( x e. B <-> x e. C ) ) )
6		dfcleq 2225	. 2 |- ( A = C <-> A. x ( x e. A <-> x e. C ) )
7		dfcleq 2225	. 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 1395   = wceq 1397   e. wcel 2202

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  eqeq1i  2239  eqeq1d  2240  eqeq2  2241  eqeq12  2244  eqtr  2249  eqsb1lem  2334  clelab  2357  neeq1  2415  pm13.18  2483  issetf  2810  sbhypf  2853  vtoclgft  2854  eqvincf  2931  pm13.183  2944  eueq  2977  mob  2988  euind  2993  reuind  3011  eqsbc1  3071  csbhypf  3166  uniiunlem  3316  snjust  3674  elsng  3684  elprg  3689  rabrsndc  3739  sneqrg  3845  preq12bg  3856  intab  3957  dfiin2g  4003  exmidsssnc  4293  exmid1stab  4298  opthg  4330  copsexg  4336  euotd  4347  elopab  4352  snnex  4545  uniuni  4548  eusv1  4549  reusv3  4557  ordtriexmid  4619  ontriexmidim  4620  onsucelsucexmidlem1  4626  onsucelsucexmid  4628  regexmidlemm  4630  regexmidlem1  4631  reg2exmidlema  4632  wetriext  4675  nn0suc  4702  nndceq0  4716  0elnn  4717  elxpi  4741  opbrop  4805  relop  4880  ideqg  4881  elrnmpt  4981  elrnmpt1  4983  elrnmptg  4984  restidsing  5069  cnveqb  5192  relcoi1  5268  funopg  5360  funcnvuni  5399  f0rn0  5531  fun11iun  5604  fvelrnb  5693  fvmptg  5722  fndmin  5754  eldmrexrn  5788  fmptco  5813  foco2  5894  elabrex  5898  elabrexg  5899  abrexco  5900  f1veqaeq  5910  f1oiso  5967  eusvobj2  6004  acexmidlema  6009  acexmidlemb  6010  acexmidlem2  6015  acexmidlemv  6016  oprabid  6050  mpofun  6123  elrnmpog  6134  elrnmpo  6135  ralrnmpo  6136  rexrnmpo  6137  ovi3  6159  ov6g  6160  ovelrn  6171  caovcang  6184  caovcan  6187  eloprabi  6361  dftpos4  6429  tfr1onlemaccex  6514  tfrcllemaccex  6527  elqsg  6754  qsel  6781  brecop  6794  eroveu  6795  erovlem  6796  th3qlem1  6806  th3q  6809  elixpsn  6904  ixpsnf1o  6905  2dom  6980  fundmen  6981  xpf1o  7030  nneneq  7043  tridc  7089  elssdc  7094  eqsndc  7095  prfidceq  7120  tpfidceq  7122  fisseneq  7127  fidcenumlemrks  7152  elfi  7170  supsnti  7204  isotilem  7205  updjudhcoinrg  7280  updjud  7281  omp1eom  7294  difinfsn  7299  ctmlemr  7307  ismkvnex  7354  omniwomnimkv  7366  nninfwlpoimlemginf  7375  nninfwlpoimlemdc  7376  nninfinfwlpolem  7377  exmidaclem  7423  exmidac  7424  onntri35  7455  exmidapne  7479  indpi  7562  nqtri3or  7616  enq0sym  7652  enq0ref  7653  enq0tr  7654  enq0breq  7656  addnq0mo  7667  mulnq0mo  7668  mulnnnq0  7670  genipv  7729  genpelvl  7732  genpelvu  7733  addsrmo  7963  mulsrmo  7964  aptisr  7999  ltresr  8059  axcnre  8101  axpre-apti  8105  ltordlem  8662  apreap  8767  apreim  8783  aprcl  8826  aptap  8830  sup3exmid  9137  creur  9139  creui  9140  nn1m1nn  9161  nn1gt1  9177  elz  9481  nn0ind-raph  9597  nltpnft  10049  xnegeq  10062  xrpnfdc  10077  xrmnfdc  10078  xleaddadd  10122  flqeqceilz  10581  1tonninf  10704  iseqf1olemqval  10763  iseqf1olemqk  10770  seq3f1olemqsum  10776  exp3val  10804  wrd2ind  11308  shftfvalg  11396  shftfval  11399  summodc  11962  fsum3  11966  telfsumo  12045  mertenslemub  12113  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  prodmodc  12157  fprodseq  12162  fprodcl2lem  12184  ndvdssub  12509  gcdval  12548  bezoutlemnewy  12585  bezoutlema  12588  bezoutlemb  12589  lcmval  12653  coprmgcdb  12678  coprmdvds1  12681  divgcdcoprmex  12692  dvdsprime  12712  nprm  12713  dvdsprm  12727  coprm  12734  qnumval  12775  qdenval  12776  m1dvdsndvds  12839  reumodprminv  12844  pceu  12886  pcval  12887  pczpre  12888  pcdiv  12893  4sqlem2  12980  4sqlem4  12983  4sqlemafi  12986  4sqexercise1  12989  4sqexercise2  12990  4sqlemsdc  12991  4sqlem12  12993  4sq  13001  ennnfonelemj0  13040  ennnfonelemjn  13041  ennnfonelem0  13044  ennnfonelemp1  13045  ennnfonelemnn0  13061  ennnfonelemim  13063  unct  13081  gsum0g  13497  gsumval2  13498  ghmf1  13878  rrgeq0i  14297  domneq0  14305  lss1d  14416  lspsn  14449  ellspsn  14450  znf1o  14684  znidom  14690  znunit  14692  istopon  14756  toponsspwpwg  14765  epttop  14833  txuni2  14999  xmeteq0  15102  comet  15242  elply  15477  elply2  15478  mpodvdsmulf1o  15733  perfectlem2  15743  lgsval  15752  lgsfvalg  15753  lgsval2lem  15758  gausslemma2dlem0i  15805  2lgslem1b  15837  2lgslem3  15849  2sqlem2  15863  2sqlem8  15871  2sqlem9  15872  upgredg2vtx  16018  uspgredg2v  16091  ushgredgedgloop  16098  vtxduspgrfvedgfi  16171  1loopgrvd2fi  16175  wlkeq  16224  depindlem1  16376  bj-charfunbi  16457  bj-nn0suc0  16596  bj-inf2vnlem1  16616  bj-inf2vnlem2  16617  bj-nn0sucALT  16624  subctctexmid  16652  pw1nct  16655  nnsf  16658  peano3nninf  16660  nninfall  16662  exmidsbthr  16678  trilpo  16698  trirec0  16699  redcwlpo  16711  redc0  16713  dceqnconst  16716  gfsumval  16732