Theorem eqeq1 2236

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 2223	. . . . . 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 1604	. . . 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 1870	. 2 |- ( A = B -> ( A. x ( x e. A <-> x e. C ) <-> A. x ( x e. B <-> x e. C ) ) )
6		dfcleq 2223	. 2 |- ( A = C <-> A. x ( x e. A <-> x e. C ) )
7		dfcleq 2223	. 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 1393   = wceq 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqeq1i  2237  eqeq1d  2238  eqeq2  2239  eqeq12  2242  eqtr  2247  eqsb1lem  2332  clelab  2355  neeq1  2413  pm13.18  2481  issetf  2807  sbhypf  2850  vtoclgft  2851  eqvincf  2928  pm13.183  2941  eueq  2974  mob  2985  euind  2990  reuind  3008  eqsbc1  3068  csbhypf  3163  uniiunlem  3313  snjust  3671  elsng  3681  elprg  3686  rabrsndc  3734  sneqrg  3840  preq12bg  3851  intab  3952  dfiin2g  3998  exmidsssnc  4287  exmid1stab  4292  opthg  4324  copsexg  4330  euotd  4341  elopab  4346  snnex  4539  uniuni  4542  eusv1  4543  reusv3  4551  ordtriexmid  4613  ontriexmidim  4614  onsucelsucexmidlem1  4620  onsucelsucexmid  4622  regexmidlemm  4624  regexmidlem1  4625  reg2exmidlema  4626  wetriext  4669  nn0suc  4696  nndceq0  4710  0elnn  4711  elxpi  4735  opbrop  4798  relop  4872  ideqg  4873  elrnmpt  4973  elrnmpt1  4975  elrnmptg  4976  restidsing  5061  cnveqb  5184  relcoi1  5260  funopg  5352  funcnvuni  5390  f0rn0  5522  fun11iun  5595  fvelrnb  5683  fvmptg  5712  fndmin  5744  eldmrexrn  5778  fmptco  5803  foco2  5883  elabrex  5887  elabrexg  5888  abrexco  5889  f1veqaeq  5899  f1oiso  5956  eusvobj2  5993  acexmidlema  5998  acexmidlemb  5999  acexmidlem2  6004  acexmidlemv  6005  oprabid  6039  mpofun  6112  elrnmpog  6123  elrnmpo  6124  ralrnmpo  6125  rexrnmpo  6126  ovi3  6148  ov6g  6149  ovelrn  6160  caovcang  6173  caovcan  6176  eloprabi  6348  dftpos4  6415  tfr1onlemaccex  6500  tfrcllemaccex  6513  elqsg  6740  qsel  6767  brecop  6780  eroveu  6781  erovlem  6782  th3qlem1  6792  th3q  6795  elixpsn  6890  ixpsnf1o  6891  2dom  6966  fundmen  6967  xpf1o  7013  nneneq  7026  tridc  7070  elssdc  7075  eqsndc  7076  prfidceq  7101  tpfidceq  7103  fisseneq  7107  fidcenumlemrks  7131  elfi  7149  supsnti  7183  isotilem  7184  updjudhcoinrg  7259  updjud  7260  omp1eom  7273  difinfsn  7278  ctmlemr  7286  ismkvnex  7333  omniwomnimkv  7345  nninfwlpoimlemginf  7354  nninfwlpoimlemdc  7355  nninfinfwlpolem  7356  exmidaclem  7401  exmidac  7402  onntri35  7433  exmidapne  7457  indpi  7540  nqtri3or  7594  enq0sym  7630  enq0ref  7631  enq0tr  7632  enq0breq  7634  addnq0mo  7645  mulnq0mo  7646  mulnnnq0  7648  genipv  7707  genpelvl  7710  genpelvu  7711  addsrmo  7941  mulsrmo  7942  aptisr  7977  ltresr  8037  axcnre  8079  axpre-apti  8083  ltordlem  8640  apreap  8745  apreim  8761  aprcl  8804  aptap  8808  sup3exmid  9115  creur  9117  creui  9118  nn1m1nn  9139  nn1gt1  9155  elz  9459  nn0ind-raph  9575  nltpnft  10022  xnegeq  10035  xrpnfdc  10050  xrmnfdc  10051  xleaddadd  10095  flqeqceilz  10552  1tonninf  10675  iseqf1olemqval  10734  iseqf1olemqk  10741  seq3f1olemqsum  10747  exp3val  10775  wrd2ind  11271  shftfvalg  11345  shftfval  11348  summodc  11910  fsum3  11914  telfsumo  11993  mertenslemub  12061  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  prodmodc  12105  fprodseq  12110  fprodcl2lem  12132  ndvdssub  12457  gcdval  12496  bezoutlemnewy  12533  bezoutlema  12536  bezoutlemb  12537  lcmval  12601  coprmgcdb  12626  coprmdvds1  12629  divgcdcoprmex  12640  dvdsprime  12660  nprm  12661  dvdsprm  12675  coprm  12682  qnumval  12723  qdenval  12724  m1dvdsndvds  12787  reumodprminv  12792  pceu  12834  pcval  12835  pczpre  12836  pcdiv  12841  4sqlem2  12928  4sqlem4  12931  4sqlemafi  12934  4sqexercise1  12937  4sqexercise2  12938  4sqlemsdc  12939  4sqlem12  12941  4sq  12949  ennnfonelemj0  12988  ennnfonelemjn  12989  ennnfonelem0  12992  ennnfonelemp1  12993  ennnfonelemnn0  13009  ennnfonelemim  13011  unct  13029  gsum0g  13445  gsumval2  13446  ghmf1  13826  rrgeq0i  14244  domneq0  14252  lss1d  14363  lspsn  14396  ellspsn  14397  znf1o  14631  znidom  14637  znunit  14639  istopon  14703  toponsspwpwg  14712  epttop  14780  txuni2  14946  xmeteq0  15049  comet  15189  elply  15424  elply2  15425  mpodvdsmulf1o  15680  perfectlem2  15690  lgsval  15699  lgsfvalg  15700  lgsval2lem  15705  gausslemma2dlem0i  15752  2lgslem1b  15784  2lgslem3  15796  2sqlem2  15810  2sqlem8  15818  2sqlem9  15819  upgredg2vtx  15962  uspgredg2v  16035  ushgredgedgloop  16042  vtxduspgrfvedgfi  16061  wlkeq  16100  bj-charfunbi  16257  bj-nn0suc0  16396  bj-inf2vnlem1  16416  bj-inf2vnlem2  16417  bj-nn0sucALT  16424  subctctexmid  16453  pw1nct  16456  nnsf  16459  peano3nninf  16461  nninfall  16463  exmidsbthr  16479  trilpo  16499  trirec0  16500  redcwlpo  16511  redc0  16513  dceqnconst  16516