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

Theorem eqeq1 2088
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 2076 . . . . . 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 1491 . . . 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 1746 . 2  |-  ( A  =  B  ->  ( A. x ( x  e.  A  <->  x  e.  C
)  <->  A. x ( x  e.  B  <->  x  e.  C ) ) )
6 dfcleq 2076 . 2  |-  ( A  =  C  <->  A. x
( x  e.  A  <->  x  e.  C ) )
7 dfcleq 2076 . 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 1283    = wceq 1285    e. wcel 1434
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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  eqeq1i  2089  eqeq1d  2090  eqeq2  2091  eqeq12  2094  eqtr  2099  eqsb3lem  2182  clelab  2204  neeq1  2259  pm13.18  2327  issetf  2607  sbhypf  2649  vtoclgft  2650  eqvincf  2721  pm13.183  2733  eueq  2764  mob  2775  euind  2780  reuind  2796  eqsbc3  2854  csbhypf  2942  uniiunlem  3083  snjust  3411  elsng  3421  elprg  3426  rabrsndc  3468  sneqrg  3562  preq12bg  3573  intab  3673  dfiin2g  3719  opthg  4001  copsexg  4007  euotd  4017  elopab  4021  snnex  4207  uniuni  4209  eusv1  4210  reusv3  4218  ordtriexmid  4273  onsucelsucexmidlem1  4279  onsucelsucexmid  4281  regexmidlemm  4283  regexmidlem1  4284  reg2exmidlema  4285  wetriext  4327  nn0suc  4353  nndceq0  4365  0elnn  4366  elxpi  4387  opbrop  4445  relop  4514  ideqg  4515  elrnmpt  4611  elrnmpt1  4613  elrnmptg  4614  cnveqb  4806  relcoi1  4879  funopg  4964  funcnvuni  4999  fun11iun  5178  fvelrnb  5253  fvmptg  5280  fndmin  5306  eldmrexrn  5340  foelrn  5349  foco2  5350  fmptco  5362  elabrex  5429  abrexco  5430  f1veqaeq  5440  f1oiso  5496  eusvobj2  5529  acexmidlema  5534  acexmidlemb  5535  acexmidlem2  5540  acexmidlemv  5541  oprabid  5568  mpt2fun  5634  elrnmpt2g  5644  elrnmpt2  5645  ralrnmpt2  5646  rexrnmpt2  5647  ovi3  5668  ov6g  5669  ovelrn  5680  caovcang  5693  caovcan  5696  eloprabi  5853  dftpos4  5912  tfr1onlemaccex  5997  tfrcllemaccex  6010  elqsg  6222  qsel  6249  brecop  6262  eroveu  6263  erovlem  6264  th3qlem1  6274  th3q  6277  2dom  6352  fundmen  6353  xpf1o  6385  nneneq  6392  supsnti  6477  isotilem  6478  indpi  6594  nqtri3or  6648  enq0sym  6684  enq0ref  6685  enq0tr  6686  enq0breq  6688  addnq0mo  6699  mulnq0mo  6700  mulnnnq0  6702  genipv  6761  genpelvl  6764  genpelvu  6765  addsrmo  6982  mulsrmo  6983  aptisr  7017  ltresr  7069  axcnre  7109  axpre-apti  7113  apreap  7754  apreim  7770  creur  8103  creui  8104  nn1m1nn  8124  nn1gt1  8139  elz  8434  nn0ind-raph  8545  nltpnft  8960  xnegeq  8970  flqeqceilz  9400  expival  9575  shftfvalg  9844  shftfval  9847  ndvdssub  10474  gcdval  10495  bezoutlemnewy  10529  bezoutlema  10532  bezoutlemb  10533  lcmval  10589  coprmgcdb  10614  coprmdvds1  10617  divgcdcoprmex  10628  dvdsprime  10648  nprm  10649  dvdsprm  10662  coprm  10667  bj-nn0suc0  10903  bj-inf2vnlem1  10923  bj-inf2vnlem2  10924  bj-nn0sucALT  10931
  Copyright terms: Public domain W3C validator