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 1607	. . . 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 1396   = wceq 1398   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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  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  2358  neeq1  2416  pm13.18  2484  issetf  2811  sbhypf  2854  vtoclgft  2855  eqvincf  2932  pm13.183  2945  eueq  2978  mob  2989  euind  2994  reuind  3012  eqsbc1  3072  csbhypf  3167  uniiunlem  3318  snjust  3678  elsng  3688  elprg  3693  rabrsndc  3743  sneqrg  3850  preq12bg  3861  intab  3962  dfiin2g  4008  exmidsssnc  4299  exmid1stab  4304  opthg  4336  copsexg  4342  euotd  4353  elopab  4358  snnex  4551  uniuni  4554  eusv1  4555  reusv3  4563  ordtriexmid  4625  ontriexmidim  4626  onsucelsucexmidlem1  4632  onsucelsucexmid  4634  regexmidlemm  4636  regexmidlem1  4637  reg2exmidlema  4638  wetriext  4681  nn0suc  4708  nndceq0  4722  0elnn  4723  elxpi  4747  opbrop  4811  relop  4886  ideqg  4887  elrnmpt  4987  elrnmpt1  4989  elrnmptg  4990  restidsing  5075  cnveqb  5199  relcoi1  5275  funopg  5367  funcnvuni  5406  f0rn0  5540  fun11iun  5613  fvelrnb  5702  fvmptg  5731  fndmin  5763  eldmrexrn  5796  fmptco  5821  foco2  5904  elabrex  5908  elabrexg  5909  abrexco  5910  f1veqaeq  5920  f1oiso  5977  eusvobj2  6014  acexmidlema  6019  acexmidlemb  6020  acexmidlem2  6025  acexmidlemv  6026  oprabid  6060  mpofun  6133  elrnmpog  6144  elrnmpo  6145  ralrnmpo  6146  rexrnmpo  6147  ovi3  6169  ov6g  6170  ovelrn  6181  caovcang  6194  caovcan  6197  eloprabi  6370  funsssuppss  6436  suppssrst  6439  suppssrgst  6440  dftpos4  6472  tfr1onlemaccex  6557  tfrcllemaccex  6570  elqsg  6797  qsel  6824  brecop  6837  eroveu  6838  erovlem  6839  th3qlem1  6849  th3q  6852  elixpsn  6947  ixpsnf1o  6948  2dom  7023  fundmen  7024  xpf1o  7073  nneneq  7086  tridc  7132  elssdc  7137  eqsndc  7138  prfidceq  7163  tpfidceq  7165  fisseneq  7170  fidcenumlemrks  7195  elfi  7230  supsnti  7264  isotilem  7265  updjudhcoinrg  7340  updjud  7341  omp1eom  7354  difinfsn  7359  ctmlemr  7367  ismkvnex  7414  omniwomnimkv  7426  nninfwlpoimlemginf  7435  nninfwlpoimlemdc  7436  nninfinfwlpolem  7437  exmidaclem  7483  exmidac  7484  onntri35  7515  exmidapne  7539  indpi  7622  nqtri3or  7676  enq0sym  7712  enq0ref  7713  enq0tr  7714  enq0breq  7716  addnq0mo  7727  mulnq0mo  7728  mulnnnq0  7730  genipv  7789  genpelvl  7792  genpelvu  7793  addsrmo  8023  mulsrmo  8024  aptisr  8059  ltresr  8119  axcnre  8161  axpre-apti  8165  ltordlem  8721  apreap  8826  apreim  8842  aprcl  8885  aptap  8889  sup3exmid  9196  creur  9198  creui  9199  nn1m1nn  9220  nn1gt1  9236  elz  9542  nn0ind-raph  9658  nltpnft  10110  xnegeq  10123  xrpnfdc  10138  xrmnfdc  10139  xleaddadd  10183  flqeqceilz  10643  1tonninf  10766  iseqf1olemqval  10825  iseqf1olemqk  10832  seq3f1olemqsum  10838  exp3val  10866  wrd2ind  11370  shftfvalg  11458  shftfval  11461  summodc  12024  fsum3  12028  telfsumo  12107  mertenslemub  12175  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  prodmodc  12219  fprodseq  12224  fprodcl2lem  12246  ndvdssub  12571  gcdval  12610  bezoutlemnewy  12647  bezoutlema  12650  bezoutlemb  12651  lcmval  12715  coprmgcdb  12740  coprmdvds1  12743  divgcdcoprmex  12754  dvdsprime  12774  nprm  12775  dvdsprm  12789  coprm  12796  qnumval  12837  qdenval  12838  m1dvdsndvds  12901  reumodprminv  12906  pceu  12948  pcval  12949  pczpre  12950  pcdiv  12955  4sqlem2  13042  4sqlem4  13045  4sqlemafi  13048  4sqexercise1  13051  4sqexercise2  13052  4sqlemsdc  13053  4sqlem12  13055  4sq  13063  ennnfonelemj0  13102  ennnfonelemjn  13103  ennnfonelem0  13106  ennnfonelemp1  13107  ennnfonelemnn0  13123  ennnfonelemim  13125  unct  13143  gsum0g  13559  gsumval2  13560  ghmf1  13940  rrgeq0i  14359  domneq0  14368  lss1d  14479  lspsn  14512  ellspsn  14513  znf1o  14747  znidom  14753  znunit  14755  istopon  14824  toponsspwpwg  14833  epttop  14901  txuni2  15067  xmeteq0  15170  comet  15310  elply  15545  elply2  15546  mpodvdsmulf1o  15804  perfectlem2  15814  lgsval  15823  lgsfvalg  15824  lgsval2lem  15829  gausslemma2dlem0i  15876  2lgslem1b  15908  2lgslem3  15920  2sqlem2  15934  2sqlem8  15942  2sqlem9  15943  upgredg2vtx  16089  uspgredg2v  16162  ushgredgedgloop  16169  vtxduspgrfvedgfi  16242  1loopgrvd2fi  16246  wlkeq  16295  depindlem1  16447  bj-charfunbi  16527  bj-nn0suc0  16666  bj-inf2vnlem1  16686  bj-inf2vnlem2  16687  bj-nn0sucALT  16694  subctctexmid  16722  pw1nct  16725  exmidnotnotr  16727  exmidcon  16728  exmidpeirce  16729  nnsf  16731  peano3nninf  16733  nninfall  16735  exmidsbthr  16751  trilpo  16775  trirec0  16776  redcwlpo  16788  redc0  16790  dceqnconst  16793  gfsumval  16809