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

Theorem eqeq2d 2048
Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
Hypothesis
Ref Expression
eqeq2d.1
Assertion
Ref Expression
eqeq2d  C  C

Proof of Theorem eqeq2d
StepHypRef Expression
1 eqeq2d.1 . 2
2 eqeq2 2046 . 2  C  C
31, 2syl 14 1  C  C
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98   wceq 1242
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 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  eqtrd  2069  eq2tri  2096  sbceq1g  2864  euabsn  3431  absneu  3433  preq12bg  3535  cbvopab  3819  cbvopab1  3821  cbvopab2  3822  cbvopab1s  3823  cbvopab2v  3825  mpteq12f  3828  cbvmpt  3842  opth  3965  eqvinop  3971  moop2  3979  euotd  3982  eusvnf  4151  reusv3i  4157  nlimsucg  4242  nn0suc  4270  opelxp  4317  elvvv  4346  relop  4429  elrnmpt1s  4527  elrnmpt1  4528  elsnres  4590  elxp4  4751  elxp5  4752  relresfld  4790  iotajust  4809  iota1  4824  iota2df  4834  funopg  4877  funcnvuni  4911  fun11iun  5090  funcocnv2  5094  nfvres  5149  ssimaex  5177  fvmptg  5191  fvmptdf  5201  fvopab6  5207  foco2  5261  fmptco  5273  fsng  5279  elabrex  5340  abrexco  5341  f1veqaeq  5351  dff13f  5352  f1ocnvfv  5362  f1ocnvfvb  5363  fcofo  5367  fliftfun  5379  fliftval  5383  f1oiso2  5409  riota5f  5435  oprabid  5480  rspceov  5489  dfoprab2  5494  mpt2eq123dva  5508  mpt2eq3dva  5511  cbvoprab1  5518  cbvoprab2  5519  cbvoprab12  5520  cbvmpt2x  5524  mpt2mptx  5537  ovmpt2s  5566  ovmpt2df  5574  ovmpt2dv2  5576  ovi3  5579  ov6g  5580  fnrnov  5588  foov  5589  caovcang  5604  caovcan  5607  f1opw2  5648  opabex3d  5690  opabex3  5691  fo1st  5726  fo2nd  5727  elxp6  5738  op1steq  5747  dfoprab4f  5761  fmpt2x  5768  df1st2  5782  df2nd2  5783  xporderlem  5793  brtpos2  5807  dftpos4  5819  tposfn2  5822  recseq  5862  frecsuc  5930  nna0r  5996  eqerlem  6073  qseq2  6091  ecelqsg  6095  snec  6103  qsinxp  6118  ecoptocl  6129  eroveu  6133  th3qlem1  6144  th3qlem2  6145  th3q  6147  en1  6215  xpsnen  6231  xpassen  6240  dfplpq2  6338  dfmpq2  6339  enqbreq2  6341  enq0sym  6415  enq0ref  6416  enq0tr  6417  addnq0mo  6430  mulnq0mo  6431  addnnnq0  6432  mulnnnq0  6433  nqnq0a  6437  nqnq0m  6438  nq0a0  6440  prarloclemcalc  6485  genipv  6492  genpassl  6507  genpassu  6508  addcomprg  6554  mulcomprg  6556  distrlem1prl  6558  distrlem1pru  6559  distrlem5prl  6562  distrlem5pru  6563  1idprl  6566  1idpru  6567  recexprlem1ssl  6605  recexprlem1ssu  6606  addsrmo  6671  mulsrmo  6672  addsrpr  6673  mulsrpr  6674  elreal  6727  axcnre  6765  negeu  6999  subeq0  7033  apreap  7371  apreim  7387  divmulap3  7438  diveqap0  7443  diveqap1  7464  nn0ind-raph  8131  elq  8333  zq  8337  cnref1o  8357  iccf1o  8642  fzen  8677  fseq1m1p1  8727  fzm1  8732  nn0ennn  8890  bj-nn0suc0  9408  bj-inf2vnlem1  9424  bj-nn0sucALT  9432
  Copyright terms: Public domain W3C validator