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

Theorem eleq1d 2103
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 2097 . 2 (A = B → (A 𝐶B 𝐶))
31, 2syl 14 1 (φ → (A 𝐶B 𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1242   wcel 1390
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-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033
This theorem is referenced by:  eleq12d  2105  eqeltrd  2111  eqneltrd  2130  eqneltrrd  2131  rspcimdv  2651  rspcimedv  2652  reuind  2738  sbcel2g  2865  sbccsb2g  2873  breq1  3758  breq2  3759  inex1g  3884  intexr  3895  pwex  3923  pwexg  3924  prexgOLD  3937  prexg  3938  opelopabsb  3988  pofun  4040  seex  4057  uniex  4140  uniexg  4141  unexb  4143  reusv3  4158  rabxfrd  4167  onun2  4182  onsucelsucexmid  4215  ordsucunielexmid  4216  tfisi  4253  peano2  4261  seinxp  4354  opabid2  4410  opeliunxp2  4419  elrn2g  4468  opeldm  4481  opeldmg  4483  elreldm  4503  elrn2  4519  opelresg  4562  elsnres  4590  iss  4597  elimasng  4636  issref  4650  rnxpid  4698  unielrel  4788  dffun5r  4857  funopg  4877  brprcneu  5114  tz6.12f  5145  fvelrnb  5164  ssimaex  5177  dmfco  5184  fvmpt3  5194  mptfvex  5199  fvmptf  5206  respreima  5238  fvelrn  5241  ffnfvf  5267  ffvresb  5271  fmptco  5273  fmptcof  5274  fsn  5278  fressnfv  5293  fnex  5326  funfvima  5333  funfvima3  5335  f1mpt  5353  fliftfuns  5381  isoselem  5402  ffnov  5547  fovcl  5548  ovmpt2s  5566  ov2gf  5567  ovg  5581  funimassov  5592  caovclg  5595  elovmpt2  5643  fnofval  5663  off  5666  fnexALT  5682  fornex  5684  f1stres  5728  f2ndres  5729  xp1st  5734  xp2nd  5735  elxp6  5738  unielxp  5742  fmpt2x  5768  mpt2fvex  5771  dftpos4  5819  smoel  5856  tfrlem3-2  5868  tfrlem3-2d  5869  tfrlem8  5875  tfrlem9  5876  tfrlemibxssdm  5882  tfrlemi1  5887  tfrexlem  5889  rdgtfr  5901  rdgon  5913  frecabex  5923  freccl  5932  nnacl  5998  nnmcl  5999  nnmordi  6025  nnaordex  6036  nnm00  6038  erexb  6067  qliftfuns  6126  fundmen  6222  fopwdom  6246  addnidpig  6320  indpi  6326  dfplpq2  6338  addclnq  6359  mulclnq  6360  nnnq0lem1  6428  addclnq0  6433  mulclnq0  6434  nqpnq0nq  6435  distrnq0  6441  prloc  6473  prarloclemlo  6476  prarloclem3  6479  prarloclem5  6482  genpml  6499  genpmu  6500  addnqprl  6511  addnqpru  6512  mulnqprl  6548  mulnqpru  6549  ltexprlemell  6571  ltexprlemelu  6572  ltexprlemdisj  6579  ltexprlemloc  6580  ltexprlemrl  6583  ltexprlemru  6585  ltexpri  6586  recexprlemm  6595  recexprlemdisj  6601  recexprlemloc  6602  recexprlem1ssl  6604  recexprlem1ssu  6605  recexpr  6609  addclsr  6661  mulclsr  6662  pitonn  6724  axaddrcl  6731  axmulrcl  6733  negreb  7052  cju  7674  peano2nn  7687  nn1m1nn  7693  nnaddcl  7695  nnmulcl  7696  nnsub  7713  nndivtr  7716  un0addcl  7971  un0mulcl  7972  elnnnn0  7981  elz  8003  nnnegz  8004  znegclb  8034  zaddcllempos  8038  zaddcllemneg  8040  zaddcl  8041  zmulcl  8053  elz2  8068  zneo  8095  nneoor  8096  zeo  8099  peano5uzti  8102  zindd  8112  uzp1  8262  uzaddcl  8285  ublbneg  8304  eqreznegel  8305  negm  8306  qmulz  8314  qnegcl  8327  irradd  8335  irrmul  8336  fzrev2  8697  frec2uzzd  8847  frec2uzuzd  8849  frecuzrdgrrn  8855  iseqovex  8879  iseqval  8880  iseqfn  8881  iseq1  8882  iseqcl  8883  iseqp1  8884  expival  8891  expp1  8896  expcllem  8900  expcl2lemap  8901  m1expcl2  8911  cjval  9053  cjth  9054  remim  9068  bdinex1g  9332  bj-intexr  9339  bj-prexg  9342  bj-uniex  9348  bj-uniexg  9349  bdunexb  9351  bj-indsuc  9363
  Copyright terms: Public domain W3C validator