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

Theorem eqeq1 2028
Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eqeq1  C  C

Proof of Theorem eqeq1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2016 . . . . . 6
21biimpi 113 . . . . 5
3219.21bi 1432 . . . 4
43bibi1d 222 . . 3  C  C
54albidv 1687 . 2  C  C
6 dfcleq 2016 . 2  C  C
7 dfcleq 2016 . 2  C  C
85, 6, 73bitr4g 212 1  C  C
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98  wal 1226   wceq 1228   wcel 1374
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-4 1381  ax-17 1400  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  eqeq1i  2029  eqeq1d  2030  eqeq2  2031  eqeq12  2034  eqtr  2039  eqsb3lem  2122  clelab  2144  neeq1  2197  pm13.18  2264  issetf  2540  sbhypf  2580  vtoclgft  2581  eqvincf  2646  pm13.183  2658  eueq  2689  mob  2700  euind  2705  reuind  2721  eqsbc3  2779  csbhypf  2862  uniiunlem  3005  snjust  3355  elprg  3367  elsncg  3372  rabrsndc  3412  sneqrg  3507  preq12bg  3518  intab  3618  dfiin2g  3664  opthg  3949  copsexg  3955  euotd  3965  elopab  3969  snnex  4131  uniuni  4133  eusv1  4134  reusv3  4142  ordtriexmid  4194  onsucelsucexmidlem1  4197  onsucelsucexmid  4199  regexmidlemm  4201  regexmidlem1  4202  nn0suc  4254  nndceq0  4266  0elnn  4267  elxpi  4288  opbrop  4346  relop  4413  ideqg  4414  elrnmpt  4510  elrnmpt1  4512  elrnmptg  4513  cnveqb  4703  relcoi1  4776  funopg  4860  funcnvuni  4894  fun11iun  5072  fvelrnb  5146  fvmptg  5173  fndmin  5199  eldmrexrn  5233  foelrn  5242  foco2  5243  fmptco  5255  elabrex  5322  abrexco  5323  f1veqaeq  5333  f1oiso  5390  eusvobj2  5422  acexmidlema  5427  acexmidlemb  5428  acexmidlem2  5433  acexmidlemv  5434  oprabid  5461  mpt2fun  5526  elrnmpt2g  5536  elrnmpt2  5537  ralrnmpt2  5538  rexrnmpt2  5539  ovi3  5560  ov6g  5561  ovelrn  5572  caovcang  5585  caovcan  5588  eloprabi  5745  dftpos4  5800  elqsg  6067  qsel  6094  brecop  6107  eroveu  6108  erovlem  6109  th3qlem1  6119  th3q  6122  nqtri3or  6255  enq0sym  6287  enq0ref  6288  enq0tr  6289  enq0breq  6291  addnq0mo  6302  mulnq0mo  6303  mulnnnq0  6305  genipv  6363  genpelvl  6366  genpelvu  6367  addsrmo  6490  mulsrmo  6491  ltresr  6550  axcnre  6575  bj-nn0suc0  7172  bj-inf2vnlem1  7188  bj-inf2vnlem2  7189  bj-nn0sucALT  7196
  Copyright terms: Public domain W3C validator