Theorem eqeq1 2147

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 2134	. . . . . 6 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
2	1	biimpi 119	. . . . 5 |- ( A = B -> A. x ( x e. A <-> x e. B ) )
3	2	19.21bi 1538	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
4	3	bibi1d 232	. . 3 |- ( A = B -> ( ( x e. A <-> x e. C ) <-> ( x e. B <-> x e. C ) ) )
5	4	albidv 1797	. 2 |- ( A = B -> ( A. x ( x e. A <-> x e. C ) <-> A. x ( x e. B <-> x e. C ) ) )
6		dfcleq 2134	. 2 |- ( A = C <-> A. x ( x e. A <-> x e. C ) )
7		dfcleq 2134	. 2 |- ( B = C <-> A. x ( x e. B <-> x e. C ) )
8	5, 6, 7	3bitr4g 222	1 |- ( A = B -> ( A = C <-> B = C ) )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1330   = wceq 1332   e. wcel 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133

This theorem is referenced by:  eqeq1i  2148  eqeq1d  2149  eqeq2  2150  eqeq12  2153  eqtr  2158  eqsb3lem  2243  clelab  2266  neeq1  2322  pm13.18  2390  issetf  2696  sbhypf  2738  vtoclgft  2739  eqvincf  2814  pm13.183  2826  eueq  2859  mob  2870  euind  2875  reuind  2893  eqsbc3  2952  csbhypf  3043  uniiunlem  3190  snjust  3537  elsng  3547  elprg  3552  rabrsndc  3599  sneqrg  3697  preq12bg  3708  intab  3808  dfiin2g  3854  exmidsssnc  4134  opthg  4168  copsexg  4174  euotd  4184  elopab  4188  snnex  4377  uniuni  4380  eusv1  4381  reusv3  4389  ordtriexmid  4445  onsucelsucexmidlem1  4451  onsucelsucexmid  4453  regexmidlemm  4455  regexmidlem1  4456  reg2exmidlema  4457  wetriext  4499  nn0suc  4526  nndceq0  4539  0elnn  4540  elxpi  4563  opbrop  4626  relop  4697  ideqg  4698  elrnmpt  4796  elrnmpt1  4798  elrnmptg  4799  cnveqb  5002  relcoi1  5078  funopg  5165  funcnvuni  5200  f0rn0  5325  fun11iun  5396  fvelrnb  5477  fvmptg  5505  fndmin  5535  eldmrexrn  5569  fmptco  5594  foco2  5663  elabrex  5667  abrexco  5668  f1veqaeq  5678  f1oiso  5735  eusvobj2  5768  acexmidlema  5773  acexmidlemb  5774  acexmidlem2  5779  acexmidlemv  5780  oprabid  5811  mpofun  5881  elrnmpog  5891  elrnmpo  5892  ralrnmpo  5893  rexrnmpo  5894  ovi3  5915  ov6g  5916  ovelrn  5927  caovcang  5940  caovcan  5943  eloprabi  6102  dftpos4  6168  tfr1onlemaccex  6253  tfrcllemaccex  6266  elqsg  6487  qsel  6514  brecop  6527  eroveu  6528  erovlem  6529  th3qlem1  6539  th3q  6542  elixpsn  6637  ixpsnf1o  6638  2dom  6707  fundmen  6708  xpf1o  6746  nneneq  6759  tridc  6801  fisseneq  6828  fidcenumlemrks  6849  elfi  6867  supsnti  6900  isotilem  6901  updjudhcoinrg  6974  updjud  6975  omp1eom  6988  difinfsn  6993  ctmlemr  7001  ismkvnex  7037  omniwomnimkv  7049  exmidaclem  7081  exmidac  7082  indpi  7174  nqtri3or  7228  enq0sym  7264  enq0ref  7265  enq0tr  7266  enq0breq  7268  addnq0mo  7279  mulnq0mo  7280  mulnnnq0  7282  genipv  7341  genpelvl  7344  genpelvu  7345  addsrmo  7575  mulsrmo  7576  aptisr  7611  ltresr  7671  axcnre  7713  axpre-apti  7717  ltordlem  8268  apreap  8373  apreim  8389  aprcl  8432  sup3exmid  8739  creur  8741  creui  8742  nn1m1nn  8762  nn1gt1  8778  elz  9080  nn0ind-raph  9192  nltpnft  9627  xnegeq  9640  xrpnfdc  9655  xrmnfdc  9656  xleaddadd  9700  flqeqceilz  10122  1tonninf  10244  iseqf1olemqval  10291  iseqf1olemqk  10298  seq3f1olemqsum  10304  exp3val  10326  shftfvalg  10622  shftfval  10625  summodc  11184  fsum3  11188  telfsumo  11267  mertenslemub  11335  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  prodmodc  11379  fprodseq  11384  ndvdssub  11663  gcdval  11684  bezoutlemnewy  11720  bezoutlema  11723  bezoutlemb  11724  lcmval  11780  coprmgcdb  11805  coprmdvds1  11808  divgcdcoprmex  11819  dvdsprime  11839  nprm  11840  dvdsprm  11853  coprm  11858  qnumval  11899  qdenval  11900  ennnfonelemj0  11950  ennnfonelemjn  11951  ennnfonelem0  11954  ennnfonelemp1  11955  ennnfonelemnn0  11971  ennnfonelemim  11973  unct  11991  istopon  12219  toponsspwpwg  12228  epttop  12298  txuni2  12464  xmeteq0  12567  comet  12707  bj-nn0suc0  13319  bj-inf2vnlem1  13339  bj-inf2vnlem2  13340  bj-nn0sucALT  13347  exmid1stab  13368  subctctexmid  13369  pw1nct  13371  nnsf  13374  peano3nninf  13376  nninfall  13379  exmidsbthr  13393  trilpo  13411  trirec0  13412  redcwlpo  13422  dceqnconst  13423