Theorem eqeq1 2203

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 2190	. . . . . 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 1572	. . . 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 1838	. 2 |- ( A = B -> ( A. x ( x e. A <-> x e. C ) <-> A. x ( x e. B <-> x e. C ) ) )
6		dfcleq 2190	. 2 |- ( A = C <-> A. x ( x e. A <-> x e. C ) )
7		dfcleq 2190	. 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 1362   = wceq 1364   e. wcel 2167

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqeq1i  2204  eqeq1d  2205  eqeq2  2206  eqeq12  2209  eqtr  2214  eqsb1lem  2299  clelab  2322  neeq1  2380  pm13.18  2448  issetf  2770  sbhypf  2813  vtoclgft  2814  eqvincf  2889  pm13.183  2902  eueq  2935  mob  2946  euind  2951  reuind  2969  eqsbc1  3029  csbhypf  3123  uniiunlem  3272  snjust  3627  elsng  3637  elprg  3642  rabrsndc  3690  sneqrg  3792  preq12bg  3803  intab  3903  dfiin2g  3949  exmidsssnc  4236  exmid1stab  4241  opthg  4271  copsexg  4277  euotd  4287  elopab  4292  snnex  4483  uniuni  4486  eusv1  4487  reusv3  4495  ordtriexmid  4557  ontriexmidim  4558  onsucelsucexmidlem1  4564  onsucelsucexmid  4566  regexmidlemm  4568  regexmidlem1  4569  reg2exmidlema  4570  wetriext  4613  nn0suc  4640  nndceq0  4654  0elnn  4655  elxpi  4679  opbrop  4742  relop  4816  ideqg  4817  elrnmpt  4915  elrnmpt1  4917  elrnmptg  4918  restidsing  5002  cnveqb  5125  relcoi1  5201  funopg  5292  funcnvuni  5327  f0rn0  5452  fun11iun  5525  fvelrnb  5608  fvmptg  5637  fndmin  5669  eldmrexrn  5703  fmptco  5728  foco2  5800  elabrex  5804  elabrexg  5805  abrexco  5806  f1veqaeq  5816  f1oiso  5873  eusvobj2  5908  acexmidlema  5913  acexmidlemb  5914  acexmidlem2  5919  acexmidlemv  5920  oprabid  5954  mpofun  6024  elrnmpog  6035  elrnmpo  6036  ralrnmpo  6037  rexrnmpo  6038  ovi3  6060  ov6g  6061  ovelrn  6072  caovcang  6085  caovcan  6088  eloprabi  6254  dftpos4  6321  tfr1onlemaccex  6406  tfrcllemaccex  6419  elqsg  6644  qsel  6671  brecop  6684  eroveu  6685  erovlem  6686  th3qlem1  6696  th3q  6699  elixpsn  6794  ixpsnf1o  6795  2dom  6864  fundmen  6865  xpf1o  6905  nneneq  6918  tridc  6960  prfidceq  6989  tpfidceq  6991  fisseneq  6995  fidcenumlemrks  7019  elfi  7037  supsnti  7071  isotilem  7072  updjudhcoinrg  7147  updjud  7148  omp1eom  7161  difinfsn  7166  ctmlemr  7174  ismkvnex  7221  omniwomnimkv  7233  nninfwlpoimlemginf  7242  nninfwlpoimlemdc  7243  exmidaclem  7275  exmidac  7276  onntri35  7304  exmidapne  7327  indpi  7409  nqtri3or  7463  enq0sym  7499  enq0ref  7500  enq0tr  7501  enq0breq  7503  addnq0mo  7514  mulnq0mo  7515  mulnnnq0  7517  genipv  7576  genpelvl  7579  genpelvu  7580  addsrmo  7810  mulsrmo  7811  aptisr  7846  ltresr  7906  axcnre  7948  axpre-apti  7952  ltordlem  8509  apreap  8614  apreim  8630  aprcl  8673  aptap  8677  sup3exmid  8984  creur  8986  creui  8987  nn1m1nn  9008  nn1gt1  9024  elz  9328  nn0ind-raph  9443  nltpnft  9889  xnegeq  9902  xrpnfdc  9917  xrmnfdc  9918  xleaddadd  9962  flqeqceilz  10410  1tonninf  10533  iseqf1olemqval  10592  iseqf1olemqk  10599  seq3f1olemqsum  10605  exp3val  10633  shftfvalg  10983  shftfval  10986  summodc  11548  fsum3  11552  telfsumo  11631  mertenslemub  11699  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  prodmodc  11743  fprodseq  11748  fprodcl2lem  11770  ndvdssub  12095  gcdval  12126  bezoutlemnewy  12163  bezoutlema  12166  bezoutlemb  12167  lcmval  12231  coprmgcdb  12256  coprmdvds1  12259  divgcdcoprmex  12270  dvdsprime  12290  nprm  12291  dvdsprm  12305  coprm  12312  qnumval  12353  qdenval  12354  m1dvdsndvds  12417  reumodprminv  12422  pceu  12464  pcval  12465  pczpre  12466  pcdiv  12471  4sqlem2  12558  4sqlem4  12561  4sqlemafi  12564  4sqexercise1  12567  4sqexercise2  12568  4sqlemsdc  12569  4sqlem12  12571  4sq  12579  ennnfonelemj0  12618  ennnfonelemjn  12619  ennnfonelem0  12622  ennnfonelemp1  12623  ennnfonelemnn0  12639  ennnfonelemim  12641  unct  12659  gsum0g  13039  gsumval2  13040  ghmf1  13403  rrgeq0i  13820  domneq0  13828  lss1d  13939  lspsn  13972  ellspsn  13973  znf1o  14207  znidom  14213  znunit  14215  istopon  14249  toponsspwpwg  14258  epttop  14326  txuni2  14492  xmeteq0  14595  comet  14735  elply  14970  elply2  14971  mpodvdsmulf1o  15226  perfectlem2  15236  lgsval  15245  lgsfvalg  15246  lgsval2lem  15251  gausslemma2dlem0i  15298  2lgslem1b  15330  2lgslem3  15342  2sqlem2  15356  2sqlem8  15364  2sqlem9  15365  bj-charfunbi  15457  bj-nn0suc0  15596  bj-inf2vnlem1  15616  bj-inf2vnlem2  15617  bj-nn0sucALT  15624  subctctexmid  15645  pw1nct  15647  nnsf  15649  peano3nninf  15651  nninfall  15653  exmidsbthr  15667  trilpo  15687  trirec0  15688  redcwlpo  15699  redc0  15701  dceqnconst  15704