Theorem eqeq1 2245

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 2232	. . . . . 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 1611	. . . 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 1877	. 2 |- ( A = B -> ( A. x ( x e. A <-> x e. C ) <-> A. x ( x e. B <-> x e. C ) ) )
6		dfcleq 2232	. 2 |- ( A = C <-> A. x ( x e. A <-> x e. C ) )
7		dfcleq 2232	. 2 |- ( B = C <-> A. x ( x e. B <-> x e. C ) )
8	5, 6, 7	3bitr4g 223	1 |- ( A = B -> ( A = C <-> B = C ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   A.wal 1400   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqeq1i  2246  eqeq1d  2247  eqeq2  2248  eqeq12  2251  eqtr  2256  eqsb1lem  2341  clelab  2366  neeq1  2433  pm13.18  2501  issetf  2829  sbhypf  2872  vtoclgft  2873  eqvincf  2951  pm13.183  2964  eueq  2997  mob  3008  euind  3013  reuind  3031  eqsbc1  3091  csbhypf  3186  uniiunlem  3338  snjust  3714  elsng  3724  elprg  3729  rabrsndc  3779  sneqrg  3887  preq12bg  3898  intab  3999  dfiin2g  4045  exmidsssnc  4340  exmid1stab  4345  opthg  4378  copsexg  4384  euotd  4395  elopab  4400  snnex  4594  uniuni  4597  eusv1  4598  reusv3  4606  ordtriexmid  4668  ontriexmidim  4669  onsucelsucexmidlem1  4675  onsucelsucexmid  4677  regexmidlemm  4679  regexmidlem1  4680  reg2exmidlema  4681  wetriext  4724  nn0suc  4751  nndceq0  4765  0elnn  4766  elxpi  4790  opbrop  4854  relop  4930  ideqg  4931  elrnmpt  5031  elrnmpt1  5033  elrnmptg  5034  restidsing  5119  cnveqb  5243  relcoi1  5319  funopg  5411  funcnvuni  5450  f0rn0  5587  fun11iun  5660  fvelrnb  5750  fvmptg  5781  fndmin  5816  eldmrexrn  5849  fmptco  5874  foco2  5959  elabrex  5963  elabrexg  5964  abrexco  5965  f1veqaeq  5975  f1oiso  6032  eusvobj2  6071  acexmidlema  6076  acexmidlemb  6077  acexmidlem2  6082  acexmidlemv  6083  oprabid  6117  mpofun  6190  elrnmpog  6201  elrnmpo  6202  ralrnmpo  6203  rexrnmpo  6204  ovi3  6226  ov6g  6227  ovelrn  6238  caovcang  6251  caovcan  6254  elabreximd  6356  eloprabi  6432  funsssuppss  6498  suppssrst  6501  suppssrgst  6502  dftpos4  6534  tfr1onlemaccex  6619  tfrcllemaccex  6632  elqsg  6859  qsel  6886  brecop  6899  eroveu  6900  erovlem  6901  th3qlem1  6911  th3q  6914  elixpsn  7017  ixpsnf1o  7018  2dom  7093  fundmen  7094  xpf1o  7144  nneneq  7158  tridc  7204  elssdc  7209  eqsndc  7210  prfidceq  7235  tpfidceq  7237  fisseneq  7242  fidcenumlemrks  7270  elfi  7305  supsnti  7345  isotilem  7346  updjudhcoinrg  7421  updjud  7422  omp1eom  7435  difinfsn  7440  ctmlemr  7448  ismkvnex  7495  omniwomnimkv  7507  nninfwlpoimlemginf  7516  nninfwlpoimlemdc  7517  nninfinfwlpolem  7518  exmidaclem  7564  exmidac  7565  onntri35  7596  exmidapne  7626  indpi  7709  nqtri3or  7763  enq0sym  7799  enq0ref  7800  enq0tr  7801  enq0breq  7803  addnq0mo  7814  mulnq0mo  7815  mulnnnq0  7817  genipv  7876  genpelvl  7879  genpelvu  7880  addsrmo  8110  mulsrmo  8111  aptisr  8146  ltresr  8206  axcnre  8248  axpre-apti  8252  ltordlem  8811  apreap  8917  apreim  8933  aprcl  8976  aptap  8980  sup3exmid  9289  creur  9291  creui  9292  nn1m1nn  9324  nn1gt1  9340  elz  9650  nn0ind-raph  9767  nltpnft  10226  xnegeq  10239  xrpnfdc  10254  xrmnfdc  10255  xleaddadd  10299  flqeqceilz  10768  1tonninf  10891  iseqf1olemqval  10950  iseqf1olemqk  10957  seq3f1olemqsum  10963  exp3val  10991  wrd2ind  11509  shftfvalg  11597  shftfval  11600  summodc  12166  fsum3  12170  telfsumo  12249  mertenslemub  12317  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  prodmodc  12361  fprodseq  12366  fprodcl2lem  12388  ndvdssub  12713  gcdval  12752  bezoutlemnewy  12789  bezoutlema  12792  bezoutlemb  12793  lcmval  12857  coprmgcdb  12882  coprmdvds1  12885  divgcdcoprmex  12896  dvdsprime  12916  nprm  12917  dvdsprm  12932  coprm  12939  qnumval  12981  qdenval  12982  m1dvdsndvds  13047  reumodprminv  13052  pceu  13094  pcval  13095  pczpre  13096  pcdiv  13101  4sqlem2  13188  4sqlem4  13191  4sqlemafi  13194  4sqexercise1  13197  4sqexercise2  13198  4sqlemsdc  13199  4sqlem12  13201  4sq  13209  ballotfilem2  13277  ennnfonelemj0  13341  ennnfonelemjn  13342  ennnfonelem0  13345  ennnfonelemp1  13346  ennnfonelemnn0  13362  ennnfonelemim  13364  unct  13382  gzsum0  13762  gzsumval2  13763  ghmf1  14125  gsumvalfi  14201  rrgeq0i  14621  domneq0  14630  lss1d  14769  lspsn  14802  ellspsn  14803  znf1o  15035  znidom  15041  znunit  15043  istopon  15163  toponsspwpwg  15172  epttop  15240  txuni2  15406  xmeteq0  15509  comet  15649  elply  15884  elply2  15885  mpodvdsmulf1o  16185  perfectlem2  16198  lgsval  16221  lgsfvalg  16222  lgsval2lem  16227  gausslemma2dlem0i  16274  2lgslem1b  16306  2lgslem3  16318  2sqlem2  16332  2sqlem8  16340  2sqlem9  16341  upgredg2vtx  16487  uspgredg2v  16560  ushgredgedgloop  16567  vtxduspgrfvedgfi  16640  1loopgrvd2fi  16644  wlkeq  16693  depindlem1  16845  bj-charfunbi  16935  bj-nn0suc0  17074  bj-inf2vnlem1  17094  bj-inf2vnlem2  17095  bj-nn0sucALT  17102  subctctexmid  17128  pw1nct  17131  exmidnotnotr  17134  exmidcon  17135  exmidpeirce  17136  stnot  17137  wexmiddc  17140  nnsf  17146  peano3nninf  17148  nninfall  17150  exmidsbthr  17166  trilpo  17190  trirec0  17191  redcwlpo  17203  redc0  17205  dceqnconst  17208