Theorem eqeq1 2184

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 2171	. . . . . 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 1558	. . . 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 1824	. 2 |- ( A = B -> ( A. x ( x e. A <-> x e. C ) <-> A. x ( x e. B <-> x e. C ) ) )
6		dfcleq 2171	. 2 |- ( A = C <-> A. x ( x e. A <-> x e. C ) )
7		dfcleq 2171	. 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 1351   = wceq 1353   e. wcel 2148

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  eqeq1i  2185  eqeq1d  2186  eqeq2  2187  eqeq12  2190  eqtr  2195  eqsb1lem  2280  clelab  2303  neeq1  2360  pm13.18  2428  issetf  2744  sbhypf  2786  vtoclgft  2787  eqvincf  2862  pm13.183  2875  eueq  2908  mob  2919  euind  2924  reuind  2942  eqsbc1  3002  csbhypf  3095  uniiunlem  3244  snjust  3597  elsng  3607  elprg  3612  rabrsndc  3660  sneqrg  3762  preq12bg  3773  intab  3873  dfiin2g  3919  exmidsssnc  4202  exmid1stab  4207  opthg  4237  copsexg  4243  euotd  4253  elopab  4257  snnex  4447  uniuni  4450  eusv1  4451  reusv3  4459  ordtriexmid  4519  ontriexmidim  4520  onsucelsucexmidlem1  4526  onsucelsucexmid  4528  regexmidlemm  4530  regexmidlem1  4531  reg2exmidlema  4532  wetriext  4575  nn0suc  4602  nndceq0  4616  0elnn  4617  elxpi  4641  opbrop  4704  relop  4776  ideqg  4777  elrnmpt  4875  elrnmpt1  4877  elrnmptg  4878  restidsing  4962  cnveqb  5083  relcoi1  5159  funopg  5249  funcnvuni  5284  f0rn0  5409  fun11iun  5481  fvelrnb  5562  fvmptg  5591  fndmin  5622  eldmrexrn  5656  fmptco  5681  foco2  5752  elabrex  5756  abrexco  5757  f1veqaeq  5767  f1oiso  5824  eusvobj2  5858  acexmidlema  5863  acexmidlemb  5864  acexmidlem2  5869  acexmidlemv  5870  oprabid  5904  mpofun  5974  elrnmpog  5984  elrnmpo  5985  ralrnmpo  5986  rexrnmpo  5987  ovi3  6008  ov6g  6009  ovelrn  6020  caovcang  6033  caovcan  6036  eloprabi  6194  dftpos4  6261  tfr1onlemaccex  6346  tfrcllemaccex  6359  elqsg  6582  qsel  6609  brecop  6622  eroveu  6623  erovlem  6624  th3qlem1  6634  th3q  6637  elixpsn  6732  ixpsnf1o  6733  2dom  6802  fundmen  6803  xpf1o  6841  nneneq  6854  tridc  6896  fisseneq  6928  fidcenumlemrks  6949  elfi  6967  supsnti  7001  isotilem  7002  updjudhcoinrg  7077  updjud  7078  omp1eom  7091  difinfsn  7096  ctmlemr  7104  ismkvnex  7150  omniwomnimkv  7162  nninfwlpoimlemginf  7171  nninfwlpoimlemdc  7172  exmidaclem  7204  exmidac  7205  onntri35  7233  exmidapne  7256  indpi  7338  nqtri3or  7392  enq0sym  7428  enq0ref  7429  enq0tr  7430  enq0breq  7432  addnq0mo  7443  mulnq0mo  7444  mulnnnq0  7446  genipv  7505  genpelvl  7508  genpelvu  7509  addsrmo  7739  mulsrmo  7740  aptisr  7775  ltresr  7835  axcnre  7877  axpre-apti  7881  ltordlem  8435  apreap  8540  apreim  8556  aprcl  8599  aptap  8603  sup3exmid  8910  creur  8912  creui  8913  nn1m1nn  8933  nn1gt1  8949  elz  9251  nn0ind-raph  9366  nltpnft  9810  xnegeq  9823  xrpnfdc  9838  xrmnfdc  9839  xleaddadd  9883  flqeqceilz  10313  1tonninf  10435  iseqf1olemqval  10482  iseqf1olemqk  10489  seq3f1olemqsum  10495  exp3val  10517  shftfvalg  10820  shftfval  10823  summodc  11384  fsum3  11388  telfsumo  11467  mertenslemub  11535  mertenslemi1  11536  mertenslem2  11537  mertensabs  11538  prodmodc  11579  fprodseq  11584  fprodcl2lem  11606  ndvdssub  11927  gcdval  11952  bezoutlemnewy  11989  bezoutlema  11992  bezoutlemb  11993  lcmval  12055  coprmgcdb  12080  coprmdvds1  12083  divgcdcoprmex  12094  dvdsprime  12114  nprm  12115  dvdsprm  12129  coprm  12136  qnumval  12177  qdenval  12178  m1dvdsndvds  12240  reumodprminv  12245  pceu  12287  pcval  12288  pczpre  12289  pcdiv  12294  4sqlem2  12379  4sqlem4  12382  ennnfonelemj0  12394  ennnfonelemjn  12395  ennnfonelem0  12398  ennnfonelemp1  12399  ennnfonelemnn0  12415  ennnfonelemim  12417  unct  12435  istopon  13382  toponsspwpwg  13391  epttop  13461  txuni2  13627  xmeteq0  13730  comet  13870  lgsval  14276  lgsfvalg  14277  lgsval2lem  14282  2sqlem2  14322  2sqlem8  14330  2sqlem9  14331  bj-charfunbi  14423  bj-nn0suc0  14562  bj-inf2vnlem1  14582  bj-inf2vnlem2  14583  bj-nn0sucALT  14590  subctctexmid  14610  pw1nct  14612  nnsf  14614  peano3nninf  14616  nninfall  14618  exmidsbthr  14631  trilpo  14651  trirec0  14652  redcwlpo  14663  redc0  14665  dceqnconst  14667