Theorem eqeq1 2172

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 2159	. . . . . 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 1546	. . . 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 1812	. 2 |- ( A = B -> ( A. x ( x e. A <-> x e. C ) <-> A. x ( x e. B <-> x e. C ) ) )
6		dfcleq 2159	. 2 |- ( A = C <-> A. x ( x e. A <-> x e. C ) )
7		dfcleq 2159	. 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 1341   = wceq 1343   e. wcel 2136

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  eqeq1i  2173  eqeq1d  2174  eqeq2  2175  eqeq12  2178  eqtr  2183  eqsb1lem  2268  clelab  2291  neeq1  2348  pm13.18  2416  issetf  2732  sbhypf  2774  vtoclgft  2775  eqvincf  2850  pm13.183  2863  eueq  2896  mob  2907  euind  2912  reuind  2930  eqsbc1  2989  csbhypf  3082  uniiunlem  3230  snjust  3580  elsng  3590  elprg  3595  rabrsndc  3643  sneqrg  3741  preq12bg  3752  intab  3852  dfiin2g  3898  exmidsssnc  4181  opthg  4215  copsexg  4221  euotd  4231  elopab  4235  snnex  4425  uniuni  4428  eusv1  4429  reusv3  4437  ordtriexmid  4497  ontriexmidim  4498  onsucelsucexmidlem1  4504  onsucelsucexmid  4506  regexmidlemm  4508  regexmidlem1  4509  reg2exmidlema  4510  wetriext  4553  nn0suc  4580  nndceq0  4594  0elnn  4595  elxpi  4619  opbrop  4682  relop  4753  ideqg  4754  elrnmpt  4852  elrnmpt1  4854  elrnmptg  4855  cnveqb  5058  relcoi1  5134  funopg  5221  funcnvuni  5256  f0rn0  5381  fun11iun  5452  fvelrnb  5533  fvmptg  5561  fndmin  5591  eldmrexrn  5625  fmptco  5650  foco2  5721  elabrex  5725  abrexco  5726  f1veqaeq  5736  f1oiso  5793  eusvobj2  5827  acexmidlema  5832  acexmidlemb  5833  acexmidlem2  5838  acexmidlemv  5839  oprabid  5870  mpofun  5940  elrnmpog  5950  elrnmpo  5951  ralrnmpo  5952  rexrnmpo  5953  ovi3  5974  ov6g  5975  ovelrn  5986  caovcang  5999  caovcan  6002  eloprabi  6161  dftpos4  6227  tfr1onlemaccex  6312  tfrcllemaccex  6325  elqsg  6547  qsel  6574  brecop  6587  eroveu  6588  erovlem  6589  th3qlem1  6599  th3q  6602  elixpsn  6697  ixpsnf1o  6698  2dom  6767  fundmen  6768  xpf1o  6806  nneneq  6819  tridc  6861  fisseneq  6893  fidcenumlemrks  6914  elfi  6932  supsnti  6966  isotilem  6967  updjudhcoinrg  7042  updjud  7043  omp1eom  7056  difinfsn  7061  ctmlemr  7069  ismkvnex  7115  omniwomnimkv  7127  exmidaclem  7160  exmidac  7161  onntri35  7189  indpi  7279  nqtri3or  7333  enq0sym  7369  enq0ref  7370  enq0tr  7371  enq0breq  7373  addnq0mo  7384  mulnq0mo  7385  mulnnnq0  7387  genipv  7446  genpelvl  7449  genpelvu  7450  addsrmo  7680  mulsrmo  7681  aptisr  7716  ltresr  7776  axcnre  7818  axpre-apti  7822  ltordlem  8376  apreap  8481  apreim  8497  aprcl  8540  sup3exmid  8848  creur  8850  creui  8851  nn1m1nn  8871  nn1gt1  8887  elz  9189  nn0ind-raph  9304  nltpnft  9746  xnegeq  9759  xrpnfdc  9774  xrmnfdc  9775  xleaddadd  9819  flqeqceilz  10249  1tonninf  10371  iseqf1olemqval  10418  iseqf1olemqk  10425  seq3f1olemqsum  10431  exp3val  10453  shftfvalg  10756  shftfval  10759  summodc  11320  fsum3  11324  telfsumo  11403  mertenslemub  11471  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  prodmodc  11515  fprodseq  11520  fprodcl2lem  11542  ndvdssub  11863  gcdval  11888  bezoutlemnewy  11925  bezoutlema  11928  bezoutlemb  11929  lcmval  11991  coprmgcdb  12016  coprmdvds1  12019  divgcdcoprmex  12030  dvdsprime  12050  nprm  12051  dvdsprm  12065  coprm  12072  qnumval  12113  qdenval  12114  m1dvdsndvds  12176  reumodprminv  12181  pceu  12223  pcval  12224  pczpre  12225  pcdiv  12230  4sqlem2  12315  4sqlem4  12318  ennnfonelemj0  12330  ennnfonelemjn  12331  ennnfonelem0  12334  ennnfonelemp1  12335  ennnfonelemnn0  12351  ennnfonelemim  12353  unct  12371  istopon  12611  toponsspwpwg  12620  epttop  12690  txuni2  12856  xmeteq0  12959  comet  13099  lgsval  13505  lgsfvalg  13506  lgsval2lem  13511  2sqlem2  13551  2sqlem8  13559  2sqlem9  13560  bj-charfunbi  13653  bj-nn0suc0  13792  bj-inf2vnlem1  13812  bj-inf2vnlem2  13813  bj-nn0sucALT  13820  exmid1stab  13840  subctctexmid  13841  pw1nct  13843  nnsf  13845  peano3nninf  13847  nninfall  13849  exmidsbthr  13862  trilpo  13882  trirec0  13883  redcwlpo  13894  redc0  13896  dceqnconst  13898