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

Theorem eleq1d 2122
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 2116 . 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 102    = wceq 1259    e. wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052
This theorem is referenced by:  eleq12d  2124  eqeltrd  2130  eqneltrd  2149  eqneltrrd  2150  rspcimdv  2674  rspcimedv  2675  reuind  2767  sbcel2g  2899  sbccsb2g  2907  breq1  3795  breq2  3796  inex1g  3921  intexr  3932  pwex  3960  pwexg  3961  prexgOLD  3974  prexg  3975  opelopabsb  4025  pofun  4077  seex  4100  uniex  4202  uniexg  4203  unexb  4205  reusv3  4220  rabxfrd  4229  onun2  4244  onsucelsucexmid  4283  ordsucunielexmid  4284  tfisi  4338  peano2  4346  seinxp  4439  opabid2  4495  opeliunxp2  4504  elrn2g  4553  opeldm  4566  opeldmg  4568  elreldm  4588  elrn2  4604  opelresg  4647  elsnres  4675  iss  4682  elimasng  4721  issref  4735  rnxpid  4783  unielrel  4873  dffun5r  4942  funopg  4962  brprcneu  5199  tz6.12f  5230  fvelrnb  5249  ssimaex  5262  dmfco  5269  fvmpt3  5279  mptfvex  5284  fvmptf  5291  respreima  5323  fvelrn  5326  ffnfvf  5352  ffvresb  5356  fmptco  5358  fmptcof  5359  fsn  5363  fressnfv  5378  fnex  5411  funfvima  5418  funfvima3  5420  f1mpt  5438  fliftfuns  5466  isoselem  5487  ffnov  5633  fovcl  5634  ovmpt2s  5652  ov2gf  5653  ovg  5667  funimassov  5678  caovclg  5681  elovmpt2  5729  fnofval  5749  off  5752  fnexALT  5768  fornex  5770  f1stres  5814  f2ndres  5815  xp1st  5820  xp2nd  5821  elxp6  5824  unielxp  5828  fmpt2x  5854  mpt2fvex  5857  dftpos4  5909  smoel  5946  tfrlem3-2  5958  tfrlem3-2d  5959  tfrlem8  5965  tfrlem9  5966  tfrlemibxssdm  5972  tfrlemi1  5977  tfrexlem  5979  rdgtfr  5992  rdgon  6004  frecabex  6015  freccl  6024  nnacl  6090  nnmcl  6091  nnmordi  6120  nnaordex  6131  nnm00  6133  erexb  6162  qliftfuns  6221  fundmen  6317  fopwdom  6341  dif1en  6368  diffitest  6375  diffifi  6382  isnumi  6420  addnidpig  6492  indpi  6498  dfplpq2  6510  addclnq  6531  mulclnq  6532  nnnq0lem1  6602  addclnq0  6607  mulclnq0  6608  nqpnq0nq  6609  distrnq0  6615  prloc  6647  prarloclemlo  6650  prarloclem3  6653  prarloclem5  6656  genpml  6673  genpmu  6674  addnqprl  6685  addnqpru  6686  mulnqprl  6724  mulnqpru  6725  ltexprlemell  6754  ltexprlemelu  6755  ltexprlemdisj  6762  ltexprlemloc  6763  ltexprlemrl  6766  ltexprlemru  6768  ltexpri  6769  recexprlemm  6780  recexprlemdisj  6786  recexprlemloc  6787  recexprlem1ssl  6789  recexprlem1ssu  6790  recexpr  6794  addclsr  6896  mulclsr  6897  pitonn  6982  peano2nnnn  6987  axaddrcl  6999  axmulrcl  7001  peano5nnnn  7024  negreb  7339  cju  7989  peano2nn  8002  nn1m1nn  8008  nnaddcl  8010  nnmulcl  8011  nnsub  8028  nndivtr  8031  un0addcl  8272  un0mulcl  8273  elnnnn0  8282  elz  8304  nnnegz  8305  znegclb  8335  zaddcllempos  8339  zaddcllemneg  8341  zaddcl  8342  nzadd  8354  zmulcl  8355  elz2  8370  zneo  8398  nneoor  8399  zeo  8402  peano5uzti  8405  zindd  8415  uzp1  8602  uzaddcl  8625  ublbneg  8645  eqreznegel  8646  negm  8647  qmulz  8655  qnegcl  8668  irradd  8678  irrmul  8679  fzrev2  9049  negqmod0  9281  frec2uzzd  9350  frec2uzuzd  9352  frecuzrdgrrn  9358  iseqovex  9383  iseqval  9384  iseqfn  9385  iseq1  9386  iseqcl  9387  iseqp1  9389  monoord  9399  monoord2  9400  isermono  9401  iseqsplit  9402  iseqcaopr3  9404  iseqcaopr2  9405  iseqid3  9409  iseqhomo  9412  iseqz  9413  iseqdistr  9414  expival  9422  expp1  9427  expcllem  9431  expcl2lemap  9432  m1expcl2  9442  facnn  9595  fac0  9596  fac1  9597  faccl  9603  facdiv  9606  facndiv  9607  bccmpl  9622  bcn2  9632  bccl  9635  shftlem  9645  shftf  9659  cjval  9673  cjth  9674  remim  9688  uzin2  9814  caubnd2  9944  clim  10033  clim2  10035  climshftlemg  10054  climcn1  10060  climcn2  10061  iiserex  10090  climub  10095  climserile  10096  climcau  10097  serif0  10102  zeo3  10179  mulsucdiv2z  10197  zob  10203  nn0o1gt2  10217  nno  10218  nn0o  10219  bdinex1g  10408  bj-intexr  10415  bj-prexg  10418  bj-uniex  10424  bj-uniexg  10425  bdunexb  10427  bj-indsuc  10439  qdencn  10511
  Copyright terms: Public domain W3C validator