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

Theorem eleq1d 2106
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eleq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
eleq1d  |-  ( ph  ->  ( A  e.  C  <->  B  e.  C ) )

Proof of Theorem eleq1d
StepHypRef Expression
1 eleq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 eleq1 2100 . 2  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
31, 2syl 14 1  |-  ( ph  ->  ( A  e.  C  <->  B  e.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 98    = wceq 1243    e. wcel 1393
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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036
This theorem is referenced by:  eleq12d  2108  eqeltrd  2114  eqneltrd  2133  eqneltrrd  2134  rspcimdv  2654  rspcimedv  2655  reuind  2741  sbcel2g  2868  sbccsb2g  2876  breq1  3764  breq2  3765  inex1g  3890  intexr  3901  pwex  3929  pwexg  3930  prexgOLD  3943  prexg  3944  opelopabsb  3994  pofun  4046  seex  4069  uniex  4170  uniexg  4171  unexb  4173  reusv3  4188  rabxfrd  4197  onun2  4212  onsucelsucexmid  4251  ordsucunielexmid  4252  tfisi  4297  peano2  4305  seinxp  4398  opabid2  4454  opeliunxp2  4463  elrn2g  4512  opeldm  4525  opeldmg  4527  elreldm  4547  elrn2  4563  opelresg  4606  elsnres  4634  iss  4641  elimasng  4680  issref  4694  rnxpid  4742  unielrel  4832  dffun5r  4901  funopg  4921  brprcneu  5158  tz6.12f  5189  fvelrnb  5208  ssimaex  5221  dmfco  5228  fvmpt3  5238  mptfvex  5243  fvmptf  5250  respreima  5282  fvelrn  5285  ffnfvf  5311  ffvresb  5315  fmptco  5317  fmptcof  5318  fsn  5322  fressnfv  5337  fnex  5370  funfvima  5377  funfvima3  5379  f1mpt  5397  fliftfuns  5425  isoselem  5446  ffnov  5592  fovcl  5593  ovmpt2s  5611  ov2gf  5612  ovg  5626  funimassov  5637  caovclg  5640  elovmpt2  5688  fnofval  5708  off  5711  fnexALT  5727  fornex  5729  f1stres  5773  f2ndres  5774  xp1st  5779  xp2nd  5780  elxp6  5783  unielxp  5787  fmpt2x  5813  mpt2fvex  5816  dftpos4  5865  smoel  5902  tfrlem3-2  5914  tfrlem3-2d  5915  tfrlem8  5921  tfrlem9  5922  tfrlemibxssdm  5928  tfrlemi1  5933  tfrexlem  5935  rdgtfr  5948  rdgon  5960  frecabex  5971  freccl  5980  nnacl  6046  nnmcl  6047  nnmordi  6076  nnaordex  6087  nnm00  6089  erexb  6118  qliftfuns  6177  fundmen  6273  fopwdom  6297  dif1en  6324  diffitest  6330  diffifi  6337  isnumi  6343  addnidpig  6415  indpi  6421  dfplpq2  6433  addclnq  6454  mulclnq  6455  nnnq0lem1  6525  addclnq0  6530  mulclnq0  6531  nqpnq0nq  6532  distrnq0  6538  prloc  6570  prarloclemlo  6573  prarloclem3  6576  prarloclem5  6579  genpml  6596  genpmu  6597  addnqprl  6608  addnqpru  6609  mulnqprl  6647  mulnqpru  6648  ltexprlemell  6677  ltexprlemelu  6678  ltexprlemdisj  6685  ltexprlemloc  6686  ltexprlemrl  6689  ltexprlemru  6691  ltexpri  6692  recexprlemm  6703  recexprlemdisj  6709  recexprlemloc  6710  recexprlem1ssl  6712  recexprlem1ssu  6713  recexpr  6717  addclsr  6819  mulclsr  6820  pitonn  6905  peano2nnnn  6910  axaddrcl  6922  axmulrcl  6924  peano5nnnn  6947  negreb  7255  cju  7889  peano2nn  7902  nn1m1nn  7908  nnaddcl  7910  nnmulcl  7911  nnsub  7928  nndivtr  7931  un0addcl  8187  un0mulcl  8188  elnnnn0  8197  elz  8219  nnnegz  8220  znegclb  8250  zaddcllempos  8254  zaddcllemneg  8256  zaddcl  8257  zmulcl  8269  elz2  8284  zneo  8311  nneoor  8312  zeo  8315  peano5uzti  8318  zindd  8328  uzp1  8478  uzaddcl  8501  ublbneg  8520  eqreznegel  8521  negm  8522  qmulz  8530  qnegcl  8543  irradd  8551  irrmul  8552  fzrev2  8914  frec2uzzd  9064  frec2uzuzd  9066  frecuzrdgrrn  9072  iseqovex  9097  iseqval  9098  iseqfn  9099  iseq1  9100  iseqcl  9101  iseqp1  9103  monoord  9113  monoord2  9114  isermono  9115  iseqsplit  9116  iseqcaopr3  9118  iseqcaopr2  9119  iseqid3  9123  iseqhomo  9126  iseqdistr  9127  expival  9135  expp1  9140  expcllem  9144  expcl2lemap  9145  m1expcl2  9155  shftlem  9295  shftf  9309  cjval  9323  cjth  9324  remim  9338  uzin2  9464  caubnd2  9591  clim  9679  clim2  9681  climshftlemg  9700  climcn1  9706  climcn2  9707  iiserex  9736  climub  9741  climserile  9742  climcau  9743  serif0  9748  bdinex1g  9894  bj-intexr  9901  bj-prexg  9904  bj-uniex  9910  bj-uniexg  9911  bdunexb  9913  bj-indsuc  9925
  Copyright terms: Public domain W3C validator