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

Theorem eleq1d 2156
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 2150 . 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 103    = wceq 1289    e. wcel 1438
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084
This theorem is referenced by:  eleq12d  2158  eqeltrd  2164  eqneltrd  2183  eqneltrrd  2184  rspcimdv  2723  rspcimedv  2724  reuind  2820  sbcel2g  2952  sbccsb2g  2960  breq1  3848  breq2  3849  inex1g  3975  intexr  3986  pwexg  4015  prexg  4038  opelopabsb  4087  pofun  4139  seex  4162  uniex  4264  uniexg  4265  unexb  4267  reusv3  4282  rabxfrd  4291  onun2  4307  onsucelsucexmid  4346  ordsucunielexmid  4347  dcextest  4396  tfisi  4402  peano2  4410  seinxp  4509  opabid2  4567  opeliunxp2  4576  elrn2g  4626  opeldm  4639  opeldmg  4641  elreldm  4661  elrn2  4677  opelresg  4720  elsnres  4749  iss  4758  elimasng  4800  issref  4814  rnxpid  4865  unielrel  4958  dffun5r  5027  funopg  5048  brprcneu  5298  tz6.12f  5333  fvelrnb  5352  ssimaex  5365  dmfco  5372  fvmpt3  5383  mptfvex  5388  fvmptf  5395  respreima  5427  fvelrn  5430  ffnfvf  5457  ffvresb  5461  fmptco  5464  fmptcof  5465  fsn  5469  fressnfv  5484  fnex  5519  funfvima  5526  funfvima3  5528  f1mpt  5550  fliftfuns  5577  isoselem  5599  ffnov  5749  fovcl  5750  ovmpt2s  5768  ov2gf  5769  ovg  5783  funimassov  5794  caovclg  5797  elovmpt2  5845  fnofval  5865  off  5868  fnexALT  5884  fornex  5886  f1stres  5930  f2ndres  5931  xp1st  5936  xp2nd  5937  elxp6  5940  unielxp  5944  fmpt2x  5970  mpt2fvex  5973  opeliunxp2f  6003  dftpos4  6028  smoel  6065  tfrlem3-2d  6077  tfrlem8  6083  tfrlem9  6084  tfrlemibxssdm  6092  tfrlemi1  6097  tfrexlem  6099  tfr1onlemsucfn  6105  tfr1onlemsucaccv  6106  tfr1onlembxssdm  6108  tfr1onlembfn  6109  tfr1onlemaccex  6113  tfr1onlemres  6114  tfri1dALT  6116  tfrcllemsucfn  6118  tfrcllemsucaccv  6119  tfrcllembxssdm  6121  tfrcllembfn  6122  tfrcllemaccex  6126  tfrcllemres  6127  tfrcl  6129  rdgtfr  6139  rdgon  6151  frecabex  6163  frecabcl  6164  frecfcllem  6169  frecsuclem  6171  nnacl  6241  nnmcl  6242  nnmordi  6275  nnaordex  6286  nnm00  6288  erexb  6317  qliftfuns  6376  fundmen  6523  fopwdom  6552  xpf1o  6560  dif1en  6595  diffitest  6603  diffifi  6610  inffiexmid  6622  unfiexmid  6628  unfidisj  6632  fiintim  6639  xpfi  6640  ssfirab  6643  fnfi  6646  iunfidisj  6655  snexxph  6659  fidcenumlemr  6664  isnumi  6810  addnidpig  6895  indpi  6901  dfplpq2  6913  addclnq  6934  mulclnq  6935  nnnq0lem1  7005  addclnq0  7010  mulclnq0  7011  nqpnq0nq  7012  distrnq0  7018  prloc  7050  prarloclemlo  7053  prarloclem3  7056  prarloclem5  7059  genpml  7076  genpmu  7077  addnqprl  7088  addnqpru  7089  mulnqprl  7127  mulnqpru  7128  ltexprlemell  7157  ltexprlemelu  7158  ltexprlemdisj  7165  ltexprlemloc  7166  ltexprlemrl  7169  ltexprlemru  7171  ltexpri  7172  recexprlemm  7183  recexprlemdisj  7189  recexprlemloc  7190  recexprlem1ssl  7192  recexprlem1ssu  7193  recexpr  7197  addclsr  7299  mulclsr  7300  pitonn  7385  peano2nnnn  7390  axaddrcl  7402  axmulrcl  7404  peano5nnnn  7427  negreb  7747  negf1o  7860  eqord1  7961  eqord2  7962  cju  8421  peano2nn  8434  nn1m1nn  8440  nnaddcl  8442  nnmulcl  8443  nnsub  8461  nndivtr  8464  un0addcl  8706  un0mulcl  8707  elnnnn0  8716  elz  8752  nnnegz  8753  znegclb  8783  zaddcllempos  8787  zaddcllemneg  8789  zaddcl  8790  nzadd  8802  zmulcl  8803  elz2  8818  zneo  8847  nneoor  8848  zeo  8851  peano5uzti  8854  zindd  8864  uzp1  9052  uzaddcl  9074  supinfneg  9083  infsupneg  9084  supminfex  9085  ublbneg  9098  eqreznegel  9099  negm  9100  qmulz  9108  qnegcl  9121  irradd  9131  irrmul  9132  fzrev2  9499  negqmod0  9738  frec2uzuzd  9809  frecuzrdgrrn  9815  frec2uzrdg  9816  frecuzrdgrcl  9817  frecuzrdgsuc  9821  frecuzrdgrclt  9822  frecuzrdgg  9823  frecuzrdgsuctlem  9830  iseqovex  9870  iseqval  9871  iseqvalt  9873  seq3val  9874  iseq1  9875  iseq1t  9876  seq3-1  9877  iseqfcl  9878  iseqfclt  9879  seqf  9880  iseqcl  9881  iseqp1  9882  iseqp1t  9883  seq3p1  9884  iseqoveq  9885  seq3clss  9887  monoord  9904  monoord2  9905  isermono  9906  seq3split  9907  iseqsplit  9908  iseqcaopr3  9910  iseqcaopr2  9911  iseqf1olemjpcl  9924  iseqf1olemqpcl  9925  iseqf1olemfvp  9926  seq3f1olemqsumkj  9927  seq3f1olemqsum  9929  seq3f1oleml  9932  seq3f1o  9933  iseqid3  9937  iseqhomo  9942  iseqz  9943  seq3homo  9944  iseqdistr  9945  seq3distr  9946  ser3ge0  9952  expp1  9962  expcllem  9966  expcl2lemap  9967  m1expcl2  9977  facnn  10135  fac0  10136  fac1  10137  faccl  10143  facdiv  10146  facndiv  10147  bccmpl  10162  bcn2  10172  bccl  10175  focdmex  10195  fihasheqf1oi  10196  iseqcoll  10247  shftlem  10250  shftf  10264  seq3shft  10272  cjval  10279  cjth  10280  remim  10294  uzin2  10420  caubnd2  10550  negfi  10659  clim  10669  clim2  10671  climshftlemg  10690  climcn1  10697  climcn2  10698  iserex  10727  climub  10733  climserle  10734  climcau  10736  serf0  10741  sumfct  10763  isumrblem  10765  fisumcvg  10766  fsum3cvg  10767  isummolem3  10770  isummolem2a  10771  zisum  10774  fsumgcl  10777  fisum  10778  fsum3  10779  fsumf1o  10782  isumss  10783  isumss2  10785  fisumcvg2  10786  fsum3cvg2  10787  fisumser  10790  fsumcl2lem  10792  fsumsplitf  10802  sumpr  10807  sumtp  10808  fsumm1  10810  fsum1p  10812  isummulc2  10820  fsum2dlemstep  10828  fisumcom2  10832  fsumshftm  10839  fisum0diag2  10841  fsummulc2  10842  fsumge1  10855  fsum00  10856  fsumabs  10859  telfsumo  10860  telfsumo2  10861  fsumparts  10864  fsumrelem  10865  fsumiun  10871  binomlem  10877  isumshft  10884  isum1p  10886  isumrpcl  10888  cvgratnnlemnexp  10918  cvgratnnlemmn  10919  cvgratnnlemseq  10920  cvgratnnlemabsle  10921  cvgratnnlemfm  10923  cvgratnnlemrate  10924  cvgratnn  10925  cvgratz  10926  mertenslem2  10930  mertensabs  10931  zeo3  11146  mulsucdiv2z  11163  zob  11169  nn0o1gt2  11183  nno  11184  nn0o  11185  infssuzex  11223  infssuzcldc  11225  qnumdencl  11443  znnen  11489  isstruct2im  11504  isstruct2r  11505  uniopn  11598  inopn  11600  fiinopn  11601  bdinex1g  11792  bj-intexr  11799  bj-prexg  11802  bj-uniex  11808  bj-uniexg  11809  bdunexb  11811  bj-indsuc  11823  exmidsbthrlem  11912  qdencn  11915
  Copyright terms: Public domain W3C validator