Theorem eqeq1 2212

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 2199	. . . . . 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 1581	. . . 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 1847	. 2 |- ( A = B -> ( A. x ( x e. A <-> x e. C ) <-> A. x ( x e. B <-> x e. C ) ) )
6		dfcleq 2199	. 2 |- ( A = C <-> A. x ( x e. A <-> x e. C ) )
7		dfcleq 2199	. 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 2176

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  eqeq1i  2213  eqeq1d  2214  eqeq2  2215  eqeq12  2218  eqtr  2223  eqsb1lem  2308  clelab  2331  neeq1  2389  pm13.18  2457  issetf  2779  sbhypf  2822  vtoclgft  2823  eqvincf  2898  pm13.183  2911  eueq  2944  mob  2955  euind  2960  reuind  2978  eqsbc1  3038  csbhypf  3132  uniiunlem  3282  snjust  3638  elsng  3648  elprg  3653  rabrsndc  3701  sneqrg  3803  preq12bg  3814  intab  3914  dfiin2g  3960  exmidsssnc  4247  exmid1stab  4252  opthg  4282  copsexg  4288  euotd  4299  elopab  4304  snnex  4495  uniuni  4498  eusv1  4499  reusv3  4507  ordtriexmid  4569  ontriexmidim  4570  onsucelsucexmidlem1  4576  onsucelsucexmid  4578  regexmidlemm  4580  regexmidlem1  4581  reg2exmidlema  4582  wetriext  4625  nn0suc  4652  nndceq0  4666  0elnn  4667  elxpi  4691  opbrop  4754  relop  4828  ideqg  4829  elrnmpt  4927  elrnmpt1  4929  elrnmptg  4930  restidsing  5015  cnveqb  5138  relcoi1  5214  funopg  5305  funcnvuni  5343  f0rn0  5470  fun11iun  5543  fvelrnb  5626  fvmptg  5655  fndmin  5687  eldmrexrn  5721  fmptco  5746  foco2  5822  elabrex  5826  elabrexg  5827  abrexco  5828  f1veqaeq  5838  f1oiso  5895  eusvobj2  5930  acexmidlema  5935  acexmidlemb  5936  acexmidlem2  5941  acexmidlemv  5942  oprabid  5976  mpofun  6047  elrnmpog  6058  elrnmpo  6059  ralrnmpo  6060  rexrnmpo  6061  ovi3  6083  ov6g  6084  ovelrn  6095  caovcang  6108  caovcan  6111  eloprabi  6282  dftpos4  6349  tfr1onlemaccex  6434  tfrcllemaccex  6447  elqsg  6672  qsel  6699  brecop  6712  eroveu  6713  erovlem  6714  th3qlem1  6724  th3q  6727  elixpsn  6822  ixpsnf1o  6823  2dom  6897  fundmen  6898  xpf1o  6941  nneneq  6954  tridc  6996  prfidceq  7025  tpfidceq  7027  fisseneq  7031  fidcenumlemrks  7055  elfi  7073  supsnti  7107  isotilem  7108  updjudhcoinrg  7183  updjud  7184  omp1eom  7197  difinfsn  7202  ctmlemr  7210  ismkvnex  7257  omniwomnimkv  7269  nninfwlpoimlemginf  7278  nninfwlpoimlemdc  7279  nninfinfwlpolem  7280  exmidaclem  7320  exmidac  7321  onntri35  7349  exmidapne  7372  indpi  7455  nqtri3or  7509  enq0sym  7545  enq0ref  7546  enq0tr  7547  enq0breq  7549  addnq0mo  7560  mulnq0mo  7561  mulnnnq0  7563  genipv  7622  genpelvl  7625  genpelvu  7626  addsrmo  7856  mulsrmo  7857  aptisr  7892  ltresr  7952  axcnre  7994  axpre-apti  7998  ltordlem  8555  apreap  8660  apreim  8676  aprcl  8719  aptap  8723  sup3exmid  9030  creur  9032  creui  9033  nn1m1nn  9054  nn1gt1  9070  elz  9374  nn0ind-raph  9490  nltpnft  9936  xnegeq  9949  xrpnfdc  9964  xrmnfdc  9965  xleaddadd  10009  flqeqceilz  10463  1tonninf  10586  iseqf1olemqval  10645  iseqf1olemqk  10652  seq3f1olemqsum  10658  exp3val  10686  shftfvalg  11129  shftfval  11132  summodc  11694  fsum3  11698  telfsumo  11777  mertenslemub  11845  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  prodmodc  11889  fprodseq  11894  fprodcl2lem  11916  ndvdssub  12241  gcdval  12280  bezoutlemnewy  12317  bezoutlema  12320  bezoutlemb  12321  lcmval  12385  coprmgcdb  12410  coprmdvds1  12413  divgcdcoprmex  12424  dvdsprime  12444  nprm  12445  dvdsprm  12459  coprm  12466  qnumval  12507  qdenval  12508  m1dvdsndvds  12571  reumodprminv  12576  pceu  12618  pcval  12619  pczpre  12620  pcdiv  12625  4sqlem2  12712  4sqlem4  12715  4sqlemafi  12718  4sqexercise1  12721  4sqexercise2  12722  4sqlemsdc  12723  4sqlem12  12725  4sq  12733  ennnfonelemj0  12772  ennnfonelemjn  12773  ennnfonelem0  12776  ennnfonelemp1  12777  ennnfonelemnn0  12793  ennnfonelemim  12795  unct  12813  gsum0g  13228  gsumval2  13229  ghmf1  13609  rrgeq0i  14026  domneq0  14034  lss1d  14145  lspsn  14178  ellspsn  14179  znf1o  14413  znidom  14419  znunit  14421  istopon  14485  toponsspwpwg  14494  epttop  14562  txuni2  14728  xmeteq0  14831  comet  14971  elply  15206  elply2  15207  mpodvdsmulf1o  15462  perfectlem2  15472  lgsval  15481  lgsfvalg  15482  lgsval2lem  15487  gausslemma2dlem0i  15534  2lgslem1b  15566  2lgslem3  15578  2sqlem2  15592  2sqlem8  15600  2sqlem9  15601  bj-charfunbi  15751  bj-nn0suc0  15890  bj-inf2vnlem1  15910  bj-inf2vnlem2  15911  bj-nn0sucALT  15918  subctctexmid  15941  pw1nct  15944  nnsf  15946  peano3nninf  15948  nninfall  15950  exmidsbthr  15966  trilpo  15986  trirec0  15987  redcwlpo  15998  redc0  16000  dceqnconst  16003