Theorem eqeq1 2144

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 2131	. . . . . 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 1537	. . . 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 1796	. 2 |- ( A = B -> ( A. x ( x e. A <-> x e. C ) <-> A. x ( x e. B <-> x e. C ) ) )
6		dfcleq 2131	. 2 |- ( A = C <-> A. x ( x e. A <-> x e. C ) )
7		dfcleq 2131	. 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 1329   = wceq 1331   e. wcel 1480

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

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

This theorem is referenced by:  eqeq1i  2145  eqeq1d  2146  eqeq2  2147  eqeq12  2150  eqtr  2155  eqsb3lem  2240  clelab  2263  neeq1  2319  pm13.18  2387  issetf  2688  sbhypf  2730  vtoclgft  2731  eqvincf  2805  pm13.183  2817  eueq  2850  mob  2861  euind  2866  reuind  2884  eqsbc3  2943  csbhypf  3033  uniiunlem  3180  snjust  3527  elsng  3537  elprg  3542  rabrsndc  3586  sneqrg  3684  preq12bg  3695  intab  3795  dfiin2g  3841  exmidsssnc  4121  opthg  4155  copsexg  4161  euotd  4171  elopab  4175  snnex  4364  uniuni  4367  eusv1  4368  reusv3  4376  ordtriexmid  4432  onsucelsucexmidlem1  4438  onsucelsucexmid  4440  regexmidlemm  4442  regexmidlem1  4443  reg2exmidlema  4444  wetriext  4486  nn0suc  4513  nndceq0  4526  0elnn  4527  elxpi  4550  opbrop  4613  relop  4684  ideqg  4685  elrnmpt  4783  elrnmpt1  4785  elrnmptg  4786  cnveqb  4989  relcoi1  5065  funopg  5152  funcnvuni  5187  f0rn0  5312  fun11iun  5381  fvelrnb  5462  fvmptg  5490  fndmin  5520  eldmrexrn  5554  fmptco  5579  foco2  5648  elabrex  5652  abrexco  5653  f1veqaeq  5663  f1oiso  5720  eusvobj2  5753  acexmidlema  5758  acexmidlemb  5759  acexmidlem2  5764  acexmidlemv  5765  oprabid  5796  mpofun  5866  elrnmpog  5876  elrnmpo  5877  ralrnmpo  5878  rexrnmpo  5879  ovi3  5900  ov6g  5901  ovelrn  5912  caovcang  5925  caovcan  5928  eloprabi  6087  dftpos4  6153  tfr1onlemaccex  6238  tfrcllemaccex  6251  elqsg  6472  qsel  6499  brecop  6512  eroveu  6513  erovlem  6514  th3qlem1  6524  th3q  6527  elixpsn  6622  ixpsnf1o  6623  2dom  6692  fundmen  6693  xpf1o  6731  nneneq  6744  tridc  6786  fisseneq  6813  fidcenumlemrks  6834  elfi  6852  supsnti  6885  isotilem  6886  updjudhcoinrg  6959  updjud  6960  omp1eom  6973  difinfsn  6978  ctmlemr  6986  ismkvnex  7022  exmidaclem  7057  exmidac  7058  indpi  7143  nqtri3or  7197  enq0sym  7233  enq0ref  7234  enq0tr  7235  enq0breq  7237  addnq0mo  7248  mulnq0mo  7249  mulnnnq0  7251  genipv  7310  genpelvl  7313  genpelvu  7314  addsrmo  7544  mulsrmo  7545  aptisr  7580  ltresr  7640  axcnre  7682  axpre-apti  7686  ltordlem  8237  apreap  8342  apreim  8358  aprcl  8401  sup3exmid  8708  creur  8710  creui  8711  nn1m1nn  8731  nn1gt1  8747  elz  9049  nn0ind-raph  9161  nltpnft  9590  xnegeq  9603  xrpnfdc  9618  xrmnfdc  9619  xleaddadd  9663  flqeqceilz  10084  1tonninf  10206  iseqf1olemqval  10253  iseqf1olemqk  10260  seq3f1olemqsum  10266  exp3val  10288  shftfvalg  10583  shftfval  10586  summodc  11145  fsum3  11149  telfsumo  11228  mertenslemub  11296  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  ndvdssub  11616  gcdval  11637  bezoutlemnewy  11673  bezoutlema  11676  bezoutlemb  11677  lcmval  11733  coprmgcdb  11758  coprmdvds1  11761  divgcdcoprmex  11772  dvdsprime  11792  nprm  11793  dvdsprm  11806  coprm  11811  qnumval  11852  qdenval  11853  ennnfonelemj0  11903  ennnfonelemjn  11904  ennnfonelem0  11907  ennnfonelemp1  11908  ennnfonelemnn0  11924  ennnfonelemim  11926  unct  11943  istopon  12169  toponsspwpwg  12178  epttop  12248  txuni2  12414  xmeteq0  12517  comet  12657  bj-nn0suc0  13137  bj-inf2vnlem1  13157  bj-inf2vnlem2  13158  bj-nn0sucALT  13165  exmid1stab  13184  subctctexmid  13185  nnsf  13188  peano3nninf  13190  nninfall  13193  exmidsbthr  13207  trilpo  13225