ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqeq1 Unicode version

Theorem eqeq1 2094
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.
StepHypRef Expression
1 dfcleq 2082 . . . . . 6  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
21biimpi 118 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1495 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
43bibi1d 231 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  <->  x  e.  C )  <->  ( x  e.  B  <->  x  e.  C
) ) )
54albidv 1752 . 2  |-  ( A  =  B  ->  ( A. x ( x  e.  A  <->  x  e.  C
)  <->  A. x ( x  e.  B  <->  x  e.  C ) ) )
6 dfcleq 2082 . 2  |-  ( A  =  C  <->  A. x
( x  e.  A  <->  x  e.  C ) )
7 dfcleq 2082 . 2  |-  ( B  =  C  <->  A. x
( x  e.  B  <->  x  e.  C ) )
85, 6, 73bitr4g 221 1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   A.wal 1287    = wceq 1289    e. wcel 1438
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081
This theorem is referenced by:  eqeq1i  2095  eqeq1d  2096  eqeq2  2097  eqeq12  2100  eqtr  2105  eqsb3lem  2190  clelab  2212  neeq1  2268  pm13.18  2336  issetf  2626  sbhypf  2668  vtoclgft  2669  eqvincf  2742  pm13.183  2754  eueq  2786  mob  2797  euind  2802  reuind  2820  eqsbc3  2878  csbhypf  2966  uniiunlem  3109  snjust  3451  elsng  3461  elprg  3466  rabrsndc  3510  sneqrg  3606  preq12bg  3617  intab  3717  dfiin2g  3763  opthg  4065  copsexg  4071  euotd  4081  elopab  4085  snnex  4271  uniuni  4273  eusv1  4274  reusv3  4282  ordtriexmid  4338  onsucelsucexmidlem1  4344  onsucelsucexmid  4346  regexmidlemm  4348  regexmidlem1  4349  reg2exmidlema  4350  wetriext  4392  nn0suc  4419  nndceq0  4431  0elnn  4432  elxpi  4454  opbrop  4517  relop  4586  ideqg  4587  elrnmpt  4684  elrnmpt1  4686  elrnmptg  4687  cnveqb  4886  relcoi1  4962  funopg  5048  funcnvuni  5083  f0rn0  5205  fun11iun  5274  fvelrnb  5352  fvmptg  5380  fndmin  5406  eldmrexrn  5440  fmptco  5464  foelrnOLD  5532  foco2  5533  elabrex  5537  abrexco  5538  f1veqaeq  5548  f1oiso  5605  eusvobj2  5638  acexmidlema  5643  acexmidlemb  5644  acexmidlem2  5649  acexmidlemv  5650  oprabid  5681  mpt2fun  5747  elrnmpt2g  5757  elrnmpt2  5758  ralrnmpt2  5759  rexrnmpt2  5760  ovi3  5781  ov6g  5782  ovelrn  5793  caovcang  5806  caovcan  5809  eloprabi  5966  dftpos4  6028  tfr1onlemaccex  6113  tfrcllemaccex  6126  elqsg  6342  qsel  6369  brecop  6382  eroveu  6383  erovlem  6384  th3qlem1  6394  th3q  6397  2dom  6522  fundmen  6523  xpf1o  6560  nneneq  6573  tridc  6615  fisseneq  6642  fidcenumlemrks  6662  supsnti  6700  isotilem  6701  updjudhcoinrg  6772  updjud  6773  indpi  6901  nqtri3or  6955  enq0sym  6991  enq0ref  6992  enq0tr  6993  enq0breq  6995  addnq0mo  7006  mulnq0mo  7007  mulnnnq0  7009  genipv  7068  genpelvl  7071  genpelvu  7072  addsrmo  7289  mulsrmo  7290  aptisr  7324  ltresr  7376  axcnre  7416  axpre-apti  7420  ltordlem  7960  apreap  8064  apreim  8080  creur  8419  creui  8420  nn1m1nn  8440  nn1gt1  8456  elz  8752  nn0ind-raph  8863  nltpnft  9279  xnegeq  9289  flqeqceilz  9725  1tonninf  9846  iseqf1olemqval  9916  iseqf1olemqk  9923  seq3f1olemqsum  9929  exp3val  9957  shftfvalg  10252  shftfval  10255  isummo  10773  fisum  10778  telfsumo  10860  mertenslemub  10928  mertenslemi1  10929  mertenslem2  10930  mertensabs  10931  ndvdssub  11208  gcdval  11229  bezoutlemnewy  11263  bezoutlema  11266  bezoutlemb  11267  lcmval  11323  coprmgcdb  11348  coprmdvds1  11351  divgcdcoprmex  11362  dvdsprime  11382  nprm  11383  dvdsprm  11396  coprm  11401  qnumval  11441  qdenval  11442  istopon  11610  toponsspwpwg  11618  bj-nn0suc0  11845  bj-inf2vnlem1  11865  bj-inf2vnlem2  11866  bj-nn0sucALT  11873  nnsf  11895  peano3nninf  11897  nninfall  11900  exmidsbthr  11913
  Copyright terms: Public domain W3C validator