Theorem eleq1d 2147

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

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 |- ( ph -> A = B )
2		eleq1 2141	. 2 |- ( A = B -> ( A e. C <-> B e. C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A e. C <-> B e. C ) )

Syntax hints:   -> wi 4   <-> wb 103   = wceq 1284   e. wcel 1433

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077

This theorem is referenced by:  eleq12d  2149  eqeltrd  2155  eqneltrd  2174  eqneltrrd  2175  rspcimdv  2702  rspcimedv  2703  reuind  2795  sbcel2g  2927  sbccsb2g  2935  breq1  3788  breq2  3789  inex1g  3914  intexr  3925  pwex  3953  pwexg  3954  prexg  3966  opelopabsb  4015  pofun  4067  seex  4090  uniex  4192  uniexg  4193  unexb  4195  reusv3  4210  rabxfrd  4219  onun2  4234  onsucelsucexmid  4273  ordsucunielexmid  4274  tfisi  4328  peano2  4336  seinxp  4429  opabid2  4485  opeliunxp2  4494  elrn2g  4543  opeldm  4556  opeldmg  4558  elreldm  4578  elrn2  4594  opelresg  4637  elsnres  4665  iss  4674  elimasng  4713  issref  4727  rnxpid  4775  unielrel  4865  dffun5r  4934  funopg  4954  brprcneu  5191  tz6.12f  5223  fvelrnb  5242  ssimaex  5255  dmfco  5262  fvmpt3  5272  mptfvex  5277  fvmptf  5284  respreima  5316  fvelrn  5319  ffnfvf  5345  ffvresb  5349  fmptco  5351  fmptcof  5352  fsn  5356  fressnfv  5371  fnex  5404  funfvima  5411  funfvima3  5413  f1mpt  5431  fliftfuns  5458  isoselem  5479  ffnov  5625  fovcl  5626  ovmpt2s  5644  ov2gf  5645  ovg  5659  funimassov  5670  caovclg  5673  elovmpt2  5721  fnofval  5741  off  5744  fnexALT  5760  fornex  5762  f1stres  5806  f2ndres  5807  xp1st  5812  xp2nd  5813  elxp6  5816  unielxp  5820  fmpt2x  5846  mpt2fvex  5849  dftpos4  5901  smoel  5938  tfrlem3-2  5950  tfrlem3-2d  5951  tfrlem8  5957  tfrlem9  5958  tfrlemibxssdm  5964  tfrlemi1  5969  tfrexlem  5971  rdgtfr  5984  rdgon  5996  frecabex  6007  freccl  6016  nnacl  6082  nnmcl  6083  nnmordi  6112  nnaordex  6123  nnm00  6125  erexb  6154  qliftfuns  6213  fundmen  6309  fopwdom  6333  dif1en  6364  diffitest  6371  diffifi  6378  fnfi  6388  isnumi  6451  addnidpig  6526  indpi  6532  dfplpq2  6544  addclnq  6565  mulclnq  6566  nnnq0lem1  6636  addclnq0  6641  mulclnq0  6642  nqpnq0nq  6643  distrnq0  6649  prloc  6681  prarloclemlo  6684  prarloclem3  6687  prarloclem5  6690  genpml  6707  genpmu  6708  addnqprl  6719  addnqpru  6720  mulnqprl  6758  mulnqpru  6759  ltexprlemell  6788  ltexprlemelu  6789  ltexprlemdisj  6796  ltexprlemloc  6797  ltexprlemrl  6800  ltexprlemru  6802  ltexpri  6803  recexprlemm  6814  recexprlemdisj  6820  recexprlemloc  6821  recexprlem1ssl  6823  recexprlem1ssu  6824  recexpr  6828  addclsr  6930  mulclsr  6931  pitonn  7016  peano2nnnn  7021  axaddrcl  7033  axmulrcl  7035  peano5nnnn  7058  negreb  7373  negf1o  7486  cju  8038  peano2nn  8051  nn1m1nn  8057  nnaddcl  8059  nnmulcl  8060  nnsub  8077  nndivtr  8080  un0addcl  8321  un0mulcl  8322  elnnnn0  8331  elz  8353  nnnegz  8354  znegclb  8384  zaddcllempos  8388  zaddcllemneg  8390  zaddcl  8391  nzadd  8403  zmulcl  8404  elz2  8419  zneo  8448  nneoor  8449  zeo  8452  peano5uzti  8455  zindd  8465  uzp1  8652  uzaddcl  8674  supinfneg  8683  infsupneg  8684  supminfex  8685  ublbneg  8698  eqreznegel  8699  negm  8700  qmulz  8708  qnegcl  8721  irradd  8731  irrmul  8732  fzrev2  9102  negqmod0  9333  frec2uzzd  9402  frec2uzuzd  9404  frecuzrdgrrn  9410  iseqovex  9439  iseqval  9440  iseqfn  9441  iseq1  9442  iseqcl  9443  iseqp1  9445  monoord  9455  monoord2  9456  isermono  9457  iseqsplit  9458  iseqcaopr3  9460  iseqcaopr2  9461  iseqid3  9465  iseqhomo  9468  iseqz  9469  iseqdistr  9470  expival  9478  expp1  9483  expcllem  9487  expcl2lemap  9488  m1expcl2  9498  facnn  9654  fac0  9655  fac1  9656  faccl  9662  facdiv  9665  facndiv  9666  bccmpl  9681  bcn2  9691  bccl  9694  shftlem  9704  shftf  9718  cjval  9732  cjth  9733  remim  9747  uzin2  9873  caubnd2  10003  negfi  10110  clim  10120  clim2  10122  climshftlemg  10141  climcn1  10147  climcn2  10148  iiserex  10177  climub  10182  climserile  10183  climcau  10184  serif0  10189  zeo3  10267  mulsucdiv2z  10285  zob  10291  nn0o1gt2  10305  nno  10306  nn0o  10307  infssuzex  10345  infssuzcldc  10347  bdinex1g  10692  bj-intexr  10699  bj-prexg  10702  bj-uniex  10708  bj-uniexg  10709  bdunexb  10711  bj-indsuc  10723  qdencn  10785