Theorem eqeq1 2212

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 2199	. . . . . 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 1581	. . . 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 1847	. 2 |- ( A = B -> ( A. x ( x e. A <-> x e. C ) <-> A. x ( x e. B <-> x e. C ) ) )
6		dfcleq 2199	. 2 |- ( A = C <-> A. x ( x e. A <-> x e. C ) )
7		dfcleq 2199	. 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 1371   = wceq 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  eqeq1i  2213  eqeq1d  2214  eqeq2  2215  eqeq12  2218  eqtr  2223  eqsb1lem  2308  clelab  2331  neeq1  2389  pm13.18  2457  issetf  2779  sbhypf  2822  vtoclgft  2823  eqvincf  2898  pm13.183  2911  eueq  2944  mob  2955  euind  2960  reuind  2978  eqsbc1  3038  csbhypf  3132  uniiunlem  3282  snjust  3638  elsng  3648  elprg  3653  rabrsndc  3701  sneqrg  3803  preq12bg  3814  intab  3914  dfiin2g  3960  exmidsssnc  4248  exmid1stab  4253  opthg  4283  copsexg  4289  euotd  4300  elopab  4305  snnex  4496  uniuni  4499  eusv1  4500  reusv3  4508  ordtriexmid  4570  ontriexmidim  4571  onsucelsucexmidlem1  4577  onsucelsucexmid  4579  regexmidlemm  4581  regexmidlem1  4582  reg2exmidlema  4583  wetriext  4626  nn0suc  4653  nndceq0  4667  0elnn  4668  elxpi  4692  opbrop  4755  relop  4829  ideqg  4830  elrnmpt  4928  elrnmpt1  4930  elrnmptg  4931  restidsing  5016  cnveqb  5139  relcoi1  5215  funopg  5306  funcnvuni  5344  f0rn0  5472  fun11iun  5545  fvelrnb  5628  fvmptg  5657  fndmin  5689  eldmrexrn  5723  fmptco  5748  foco2  5824  elabrex  5828  elabrexg  5829  abrexco  5830  f1veqaeq  5840  f1oiso  5897  eusvobj2  5932  acexmidlema  5937  acexmidlemb  5938  acexmidlem2  5943  acexmidlemv  5944  oprabid  5978  mpofun  6049  elrnmpog  6060  elrnmpo  6061  ralrnmpo  6062  rexrnmpo  6063  ovi3  6085  ov6g  6086  ovelrn  6097  caovcang  6110  caovcan  6113  eloprabi  6284  dftpos4  6351  tfr1onlemaccex  6436  tfrcllemaccex  6449  elqsg  6674  qsel  6701  brecop  6714  eroveu  6715  erovlem  6716  th3qlem1  6726  th3q  6729  elixpsn  6824  ixpsnf1o  6825  2dom  6899  fundmen  6900  xpf1o  6943  nneneq  6956  tridc  6998  prfidceq  7027  tpfidceq  7029  fisseneq  7033  fidcenumlemrks  7057  elfi  7075  supsnti  7109  isotilem  7110  updjudhcoinrg  7185  updjud  7186  omp1eom  7199  difinfsn  7204  ctmlemr  7212  ismkvnex  7259  omniwomnimkv  7271  nninfwlpoimlemginf  7280  nninfwlpoimlemdc  7281  nninfinfwlpolem  7282  exmidaclem  7322  exmidac  7323  onntri35  7351  exmidapne  7374  indpi  7457  nqtri3or  7511  enq0sym  7547  enq0ref  7548  enq0tr  7549  enq0breq  7551  addnq0mo  7562  mulnq0mo  7563  mulnnnq0  7565  genipv  7624  genpelvl  7627  genpelvu  7628  addsrmo  7858  mulsrmo  7859  aptisr  7894  ltresr  7954  axcnre  7996  axpre-apti  8000  ltordlem  8557  apreap  8662  apreim  8678  aprcl  8721  aptap  8725  sup3exmid  9032  creur  9034  creui  9035  nn1m1nn  9056  nn1gt1  9072  elz  9376  nn0ind-raph  9492  nltpnft  9938  xnegeq  9951  xrpnfdc  9966  xrmnfdc  9967  xleaddadd  10011  flqeqceilz  10465  1tonninf  10588  iseqf1olemqval  10647  iseqf1olemqk  10654  seq3f1olemqsum  10660  exp3val  10688  shftfvalg  11162  shftfval  11165  summodc  11727  fsum3  11731  telfsumo  11810  mertenslemub  11878  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  prodmodc  11922  fprodseq  11927  fprodcl2lem  11949  ndvdssub  12274  gcdval  12313  bezoutlemnewy  12350  bezoutlema  12353  bezoutlemb  12354  lcmval  12418  coprmgcdb  12443  coprmdvds1  12446  divgcdcoprmex  12457  dvdsprime  12477  nprm  12478  dvdsprm  12492  coprm  12499  qnumval  12540  qdenval  12541  m1dvdsndvds  12604  reumodprminv  12609  pceu  12651  pcval  12652  pczpre  12653  pcdiv  12658  4sqlem2  12745  4sqlem4  12748  4sqlemafi  12751  4sqexercise1  12754  4sqexercise2  12755  4sqlemsdc  12756  4sqlem12  12758  4sq  12766  ennnfonelemj0  12805  ennnfonelemjn  12806  ennnfonelem0  12809  ennnfonelemp1  12810  ennnfonelemnn0  12826  ennnfonelemim  12828  unct  12846  gsum0g  13261  gsumval2  13262  ghmf1  13642  rrgeq0i  14059  domneq0  14067  lss1d  14178  lspsn  14211  ellspsn  14212  znf1o  14446  znidom  14452  znunit  14454  istopon  14518  toponsspwpwg  14527  epttop  14595  txuni2  14761  xmeteq0  14864  comet  15004  elply  15239  elply2  15240  mpodvdsmulf1o  15495  perfectlem2  15505  lgsval  15514  lgsfvalg  15515  lgsval2lem  15520  gausslemma2dlem0i  15567  2lgslem1b  15599  2lgslem3  15611  2sqlem2  15625  2sqlem8  15633  2sqlem9  15634  bj-charfunbi  15784  bj-nn0suc0  15923  bj-inf2vnlem1  15943  bj-inf2vnlem2  15944  bj-nn0sucALT  15951  subctctexmid  15974  pw1nct  15977  nnsf  15979  peano3nninf  15981  nninfall  15983  exmidsbthr  15999  trilpo  16019  trirec0  16020  redcwlpo  16031  redc0  16033  dceqnconst  16036