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

Theorem eleq1d 2088
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eleq1d.1 (φA = B)
Assertion
Ref Expression
eleq1d (φ → (A 𝐶B 𝐶))

Proof of Theorem eleq1d
StepHypRef Expression
1 eleq1d.1 . 2 (φA = B)
2 eleq1 2082 . 2 (A = B → (A 𝐶B 𝐶))
31, 2syl 14 1 (φ → (A 𝐶B 𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = 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-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015  df-clel 2018
This theorem is referenced by:  eleq12d  2090  eqeltrd  2096  eqneltrd  2115  eqneltrrd  2116  rspcimdv  2634  rspcimedv  2635  reuind  2721  sbcel2g  2848  sbccsb2g  2856  breq1  3741  breq2  3742  inex1g  3867  intexr  3878  pwex  3906  pwexg  3907  prexgOLD  3920  prexg  3921  opelopabsb  3971  pofun  4023  seex  4040  uniex  4124  uniexg  4125  unexb  4127  reusv3  4142  rabxfrd  4151  onun2  4166  onsucelsucexmid  4199  ordsucunielexmid  4200  tfisi  4237  peano2  4245  seinxp  4338  opabid2  4394  opeliunxp2  4403  elrn2g  4452  opeldm  4465  opeldmg  4467  elreldm  4487  elrn2  4503  opelresg  4546  elsnres  4574  iss  4581  elimasng  4620  issref  4634  rnxpid  4682  unielrel  4772  funopg  4860  brprcneu  5096  tz6.12f  5127  fvelrnb  5146  ssimaex  5159  dmfco  5166  fvmpt3  5176  mptfvex  5181  fvmptf  5188  respreima  5220  fvelrn  5223  ffnfvf  5249  ffvresb  5253  fmptco  5255  fmptcof  5256  fsn  5260  fressnfv  5275  fnex  5308  funfvima  5315  funfvima3  5317  f1mpt  5335  fliftfuns  5363  isoselem  5384  ffnov  5528  fovcl  5529  ovmpt2s  5547  ov2gf  5548  ovg  5562  funimassov  5573  caovclg  5576  elovmpt2  5624  fnofval  5644  off  5647  fnexALT  5663  fornex  5665  f1stres  5709  f2ndres  5710  xp1st  5715  xp2nd  5716  elxp6  5719  unielxp  5723  fmpt2x  5749  mpt2fvex  5752  dftpos4  5800  smoel  5837  tfrlem3-2  5849  tfrlem3-2d  5850  tfrlem8  5856  tfrlem9  5857  tfrlemibxssdm  5862  tfrlemi1  5867  tfrexlem  5870  rdgon  5893  nnacl  5974  nnmcl  5975  nnmordi  6000  nnaordex  6011  nnm00  6013  erexb  6042  qliftfuns  6101  addnidpig  6196  dfplpq2  6213  addclnq  6234  mulclnq  6235  nnnq0lem1  6301  addclnq0  6306  mulclnq0  6307  nqpnq0nq  6308  distrnq0  6314  prloc  6345  prarloclemlo  6348  prarloclem3  6351  prarloclem5  6354  genpml  6372  genpmu  6373  addnqprl  6384  addnqpru  6385  mulnqprl  6412  mulnqpru  6413  ltexprlemell  6435  ltexprlemelu  6436  ltexprlemdisj  6443  ltexprlemloc  6444  ltexprlemrl  6447  ltexprlemru  6449  ltexpri  6450  recexprlemm  6458  recexprlemdisj  6464  recexprlemloc  6465  recexprlem1ssl  6467  recexprlem1ssu  6468  recexpr  6472  addclsr  6500  mulclsr  6501  axaddrcl  6561  axmulrcl  6563  negreb  6862  bdinex1g  7124  bj-intexr  7131  bj-prexg  7134  bj-uniex  7140  bj-uniexg  7141  bdunexb  7143  bj-indsuc  7151
  Copyright terms: Public domain W3C validator