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  5520  fun11iun  5593  fvelrnb  5681  fvmptg  5710  fndmin  5742  eldmrexrn  5776  fmptco  5801  foco2  5877  elabrex  5881  elabrexg  5882  abrexco  5883  f1veqaeq  5893  f1oiso  5950  eusvobj2  5987  acexmidlema  5992  acexmidlemb  5993  acexmidlem2  5998  acexmidlemv  5999  oprabid  6033  mpofun  6106  elrnmpog  6117  elrnmpo  6118  ralrnmpo  6119  rexrnmpo  6120  ovi3  6142  ov6g  6143  ovelrn  6154  caovcang  6167  caovcan  6170  eloprabi  6342  dftpos4  6409  tfr1onlemaccex  6494  tfrcllemaccex  6507  elqsg  6732  qsel  6759  brecop  6772  eroveu  6773  erovlem  6774  th3qlem1  6784  th3q  6787  elixpsn  6882  ixpsnf1o  6883  2dom  6958  fundmen  6959  xpf1o  7005  nneneq  7018  tridc  7061  prfidceq  7090  tpfidceq  7092  fisseneq  7096  fidcenumlemrks  7120  elfi  7138  supsnti  7172  isotilem  7173  updjudhcoinrg  7248  updjud  7249  omp1eom  7262  difinfsn  7267  ctmlemr  7275  ismkvnex  7322  omniwomnimkv  7334  nninfwlpoimlemginf  7343  nninfwlpoimlemdc  7344  nninfinfwlpolem  7345  exmidaclem  7390  exmidac  7391  onntri35  7422  exmidapne  7446  indpi  7529  nqtri3or  7583  enq0sym  7619  enq0ref  7620  enq0tr  7621  enq0breq  7623  addnq0mo  7634  mulnq0mo  7635  mulnnnq0  7637  genipv  7696  genpelvl  7699  genpelvu  7700  addsrmo  7930  mulsrmo  7931  aptisr  7966  ltresr  8026  axcnre  8068  axpre-apti  8072  ltordlem  8629  apreap  8734  apreim  8750  aprcl  8793  aptap  8797  sup3exmid  9104  creur  9106  creui  9107  nn1m1nn  9128  nn1gt1  9144  elz  9448  nn0ind-raph  9564  nltpnft  10010  xnegeq  10023  xrpnfdc  10038  xrmnfdc  10039  xleaddadd  10083  flqeqceilz  10540  1tonninf  10663  iseqf1olemqval  10722  iseqf1olemqk  10729  seq3f1olemqsum  10735  exp3val  10763  wrd2ind  11255  shftfvalg  11329  shftfval  11332  summodc  11894  fsum3  11898  telfsumo  11977  mertenslemub  12045  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  prodmodc  12089  fprodseq  12094  fprodcl2lem  12116  ndvdssub  12441  gcdval  12480  bezoutlemnewy  12517  bezoutlema  12520  bezoutlemb  12521  lcmval  12585  coprmgcdb  12610  coprmdvds1  12613  divgcdcoprmex  12624  dvdsprime  12644  nprm  12645  dvdsprm  12659  coprm  12666  qnumval  12707  qdenval  12708  m1dvdsndvds  12771  reumodprminv  12776  pceu  12818  pcval  12819  pczpre  12820  pcdiv  12825  4sqlem2  12912  4sqlem4  12915  4sqlemafi  12918  4sqexercise1  12921  4sqexercise2  12922  4sqlemsdc  12923  4sqlem12  12925  4sq  12933  ennnfonelemj0  12972  ennnfonelemjn  12973  ennnfonelem0  12976  ennnfonelemp1  12977  ennnfonelemnn0  12993  ennnfonelemim  12995  unct  13013  gsum0g  13429  gsumval2  13430  ghmf1  13810  rrgeq0i  14228  domneq0  14236  lss1d  14347  lspsn  14380  ellspsn  14381  znf1o  14615  znidom  14621  znunit  14623  istopon  14687  toponsspwpwg  14696  epttop  14764  txuni2  14930  xmeteq0  15033  comet  15173  elply  15408  elply2  15409  mpodvdsmulf1o  15664  perfectlem2  15674  lgsval  15683  lgsfvalg  15684  lgsval2lem  15689  gausslemma2dlem0i  15736  2lgslem1b  15768  2lgslem3  15780  2sqlem2  15794  2sqlem8  15802  2sqlem9  15803  upgredg2vtx  15946  uspgredg2v  16019  ushgredgedgloop  16026  wlkeq  16065  bj-charfunbi  16174  bj-nn0suc0  16313  bj-inf2vnlem1  16333  bj-inf2vnlem2  16334  bj-nn0sucALT  16341  subctctexmid  16366  pw1nct  16369  nnsf  16371  peano3nninf  16373  nninfall  16375  exmidsbthr  16391  trilpo  16411  trirec0  16412  redcwlpo  16423  redc0  16425  dceqnconst  16428