Theorem eqeq1 2214

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 2201	. . . . . 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 1582	. . . 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 1848	. 2 |- ( A = B -> ( A. x ( x e. A <-> x e. C ) <-> A. x ( x e. B <-> x e. C ) ) )
6		dfcleq 2201	. 2 |- ( A = C <-> A. x ( x e. A <-> x e. C ) )
7		dfcleq 2201	. 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 2178

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  eqeq1i  2215  eqeq1d  2216  eqeq2  2217  eqeq12  2220  eqtr  2225  eqsb1lem  2310  clelab  2333  neeq1  2391  pm13.18  2459  issetf  2784  sbhypf  2827  vtoclgft  2828  eqvincf  2905  pm13.183  2918  eueq  2951  mob  2962  euind  2967  reuind  2985  eqsbc1  3045  csbhypf  3140  uniiunlem  3290  snjust  3648  elsng  3658  elprg  3663  rabrsndc  3711  sneqrg  3816  preq12bg  3827  intab  3928  dfiin2g  3974  exmidsssnc  4263  exmid1stab  4268  opthg  4300  copsexg  4306  euotd  4317  elopab  4322  snnex  4513  uniuni  4516  eusv1  4517  reusv3  4525  ordtriexmid  4587  ontriexmidim  4588  onsucelsucexmidlem1  4594  onsucelsucexmid  4596  regexmidlemm  4598  regexmidlem1  4599  reg2exmidlema  4600  wetriext  4643  nn0suc  4670  nndceq0  4684  0elnn  4685  elxpi  4709  opbrop  4772  relop  4846  ideqg  4847  elrnmpt  4946  elrnmpt1  4948  elrnmptg  4949  restidsing  5034  cnveqb  5157  relcoi1  5233  funopg  5324  funcnvuni  5362  f0rn0  5492  fun11iun  5565  fvelrnb  5649  fvmptg  5678  fndmin  5710  eldmrexrn  5744  fmptco  5769  foco2  5845  elabrex  5849  elabrexg  5850  abrexco  5851  f1veqaeq  5861  f1oiso  5918  eusvobj2  5953  acexmidlema  5958  acexmidlemb  5959  acexmidlem2  5964  acexmidlemv  5965  oprabid  5999  mpofun  6070  elrnmpog  6081  elrnmpo  6082  ralrnmpo  6083  rexrnmpo  6084  ovi3  6106  ov6g  6107  ovelrn  6118  caovcang  6131  caovcan  6134  eloprabi  6305  dftpos4  6372  tfr1onlemaccex  6457  tfrcllemaccex  6470  elqsg  6695  qsel  6722  brecop  6735  eroveu  6736  erovlem  6737  th3qlem1  6747  th3q  6750  elixpsn  6845  ixpsnf1o  6846  2dom  6921  fundmen  6922  xpf1o  6966  nneneq  6979  tridc  7022  prfidceq  7051  tpfidceq  7053  fisseneq  7057  fidcenumlemrks  7081  elfi  7099  supsnti  7133  isotilem  7134  updjudhcoinrg  7209  updjud  7210  omp1eom  7223  difinfsn  7228  ctmlemr  7236  ismkvnex  7283  omniwomnimkv  7295  nninfwlpoimlemginf  7304  nninfwlpoimlemdc  7305  nninfinfwlpolem  7306  exmidaclem  7351  exmidac  7352  onntri35  7383  exmidapne  7407  indpi  7490  nqtri3or  7544  enq0sym  7580  enq0ref  7581  enq0tr  7582  enq0breq  7584  addnq0mo  7595  mulnq0mo  7596  mulnnnq0  7598  genipv  7657  genpelvl  7660  genpelvu  7661  addsrmo  7891  mulsrmo  7892  aptisr  7927  ltresr  7987  axcnre  8029  axpre-apti  8033  ltordlem  8590  apreap  8695  apreim  8711  aprcl  8754  aptap  8758  sup3exmid  9065  creur  9067  creui  9068  nn1m1nn  9089  nn1gt1  9105  elz  9409  nn0ind-raph  9525  nltpnft  9971  xnegeq  9984  xrpnfdc  9999  xrmnfdc  10000  xleaddadd  10044  flqeqceilz  10500  1tonninf  10623  iseqf1olemqval  10682  iseqf1olemqk  10689  seq3f1olemqsum  10695  exp3val  10723  wrd2ind  11214  shftfvalg  11244  shftfval  11247  summodc  11809  fsum3  11813  telfsumo  11892  mertenslemub  11960  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  prodmodc  12004  fprodseq  12009  fprodcl2lem  12031  ndvdssub  12356  gcdval  12395  bezoutlemnewy  12432  bezoutlema  12435  bezoutlemb  12436  lcmval  12500  coprmgcdb  12525  coprmdvds1  12528  divgcdcoprmex  12539  dvdsprime  12559  nprm  12560  dvdsprm  12574  coprm  12581  qnumval  12622  qdenval  12623  m1dvdsndvds  12686  reumodprminv  12691  pceu  12733  pcval  12734  pczpre  12735  pcdiv  12740  4sqlem2  12827  4sqlem4  12830  4sqlemafi  12833  4sqexercise1  12836  4sqexercise2  12837  4sqlemsdc  12838  4sqlem12  12840  4sq  12848  ennnfonelemj0  12887  ennnfonelemjn  12888  ennnfonelem0  12891  ennnfonelemp1  12892  ennnfonelemnn0  12908  ennnfonelemim  12910  unct  12928  gsum0g  13343  gsumval2  13344  ghmf1  13724  rrgeq0i  14141  domneq0  14149  lss1d  14260  lspsn  14293  ellspsn  14294  znf1o  14528  znidom  14534  znunit  14536  istopon  14600  toponsspwpwg  14609  epttop  14677  txuni2  14843  xmeteq0  14946  comet  15086  elply  15321  elply2  15322  mpodvdsmulf1o  15577  perfectlem2  15587  lgsval  15596  lgsfvalg  15597  lgsval2lem  15602  gausslemma2dlem0i  15649  2lgslem1b  15681  2lgslem3  15693  2sqlem2  15707  2sqlem8  15715  2sqlem9  15716  upgredg2vtx  15852  bj-charfunbi  15946  bj-nn0suc0  16085  bj-inf2vnlem1  16105  bj-inf2vnlem2  16106  bj-nn0sucALT  16113  subctctexmid  16139  pw1nct  16142  nnsf  16144  peano3nninf  16146  nninfall  16148  exmidsbthr  16164  trilpo  16184  trirec0  16185  redcwlpo  16196  redc0  16198  dceqnconst  16201