Theorem eleq1d 2256

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 2250	. 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 105   = wceq 1363   e. wcel 2158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183

This theorem is referenced by:  eleq12d  2258  eqeltrd  2264  eqneltrd  2283  eqneltrrd  2284  rspcimdv  2854  rspcimedv  2855  reuind  2954  sbcel2g  3090  sbccsb2g  3099  breq1  4018  breq2  4019  inex1g  4151  intexr  4162  pwexg  4192  prexg  4223  opelopabsb  4272  pofun  4324  seex  4347  uniex  4449  uniexg  4451  unexb  4454  abnexg  4458  reusv3  4472  rabxfrd  4481  onun2  4501  onsucelsucexmid  4541  ordsucunielexmid  4542  dcextest  4592  tfisi  4598  peano2  4606  seinxp  4709  opabid2  4770  opeliunxp2  4779  elrn2g  4829  opeldm  4842  opeldmg  4844  elreldm  4865  elrn2  4881  opelresg  4926  elsnres  4956  iss  4965  elimasng  5008  issref  5023  rnxpid  5075  unielrel  5168  dffun5r  5240  funopg  5262  brprcneu  5520  tz6.12f  5556  fvelrnb  5576  ssimaex  5590  dmfco  5597  fvmpt3  5608  mptfvex  5614  fvmptf  5621  respreima  5657  fvelrn  5660  ffnfvf  5688  ffvresb  5692  fmptco  5695  fmptcof  5696  fsn  5701  fressnfv  5716  fnex  5751  funfvima  5761  funfvima3  5763  f1mpt  5785  fliftfuns  5812  isoselem  5834  ovrspc2v  5914  ffnov  5992  fovcld  5993  ovmpos  6012  ov2gf  6013  ovg  6027  funimassov  6038  caovclg  6041  elovmpo  6086  off  6109  fnexALT  6126  focdmex  6130  f1stres  6174  f2ndres  6175  xp1st  6180  xp2nd  6181  elxp6  6184  oprssdmm  6186  unielxp  6189  fmpox  6215  mpofvex  6218  opeliunxp2f  6253  dftpos4  6278  smoel  6315  tfrlem3-2d  6327  tfrlem8  6333  tfrlem9  6334  tfrlemibxssdm  6342  tfrlemi1  6347  tfrexlem  6349  tfr1onlemsucfn  6355  tfr1onlemsucaccv  6356  tfr1onlembxssdm  6358  tfr1onlembfn  6359  tfr1onlemaccex  6363  tfr1onlemres  6364  tfri1dALT  6366  tfrcllemsucfn  6368  tfrcllemsucaccv  6369  tfrcllembxssdm  6371  tfrcllembfn  6372  tfrcllemaccex  6376  tfrcllemres  6377  tfrcl  6379  rdgtfr  6389  rdgon  6401  frecabex  6413  frecabcl  6414  frecfcllem  6419  frecsuclem  6421  nnacl  6495  nnmcl  6496  nnmordi  6531  nnaordex  6543  nnm00  6545  erexb  6574  qliftfuns  6633  ixpsnval  6715  elixp2  6716  resixp  6747  mptelixpg  6748  elixpsn  6749  fundmen  6820  fopwdom  6850  xpf1o  6858  dif1en  6893  diffitest  6901  diffifi  6908  inffiexmid  6920  unfiexmid  6931  unfidisj  6935  fiintim  6942  xpfi  6943  ssfirab  6947  fnfi  6950  iunfidisj  6959  snexxph  6963  fidcenumlemr  6968  elfi2  6985  ctssdccl  7124  isnumi  7195  cc2lem  7279  cc3  7281  addnidpig  7349  indpi  7355  dfplpq2  7367  addclnq  7388  mulclnq  7389  nnnq0lem1  7459  addclnq0  7464  mulclnq0  7465  nqpnq0nq  7466  distrnq0  7472  prloc  7504  prarloclemlo  7507  prarloclem3  7510  prarloclem5  7513  genpml  7530  genpmu  7531  addnqprl  7542  addnqpru  7543  mulnqprl  7581  mulnqpru  7582  ltexprlemell  7611  ltexprlemelu  7612  ltexprlemdisj  7619  ltexprlemloc  7620  ltexprlemrl  7623  ltexprlemru  7625  ltexpri  7626  recexprlemm  7637  recexprlemdisj  7643  recexprlemloc  7644  recexprlem1ssl  7646  recexprlem1ssu  7647  recexpr  7651  addclsr  7766  mulclsr  7767  suplocsrlemb  7819  suplocsrlempr  7820  suplocsrlem  7821  suplocsr  7822  pitonn  7861  peano2nnnn  7866  axaddrcl  7878  axmulrcl  7880  peano5nnnn  7905  axpre-suploclemres  7914  negreb  8236  negf1o  8353  eqord1  8454  eqord2  8455  cju  8932  peano2nn  8945  nn1m1nn  8951  nnaddcl  8953  nnmulcl  8954  nnsub  8972  nndivtr  8975  un0addcl  9223  un0mulcl  9224  elnnnn0  9233  elz  9269  nnnegz  9270  znegclb  9300  zaddcllempos  9304  zaddcllemneg  9306  zaddcl  9307  nzadd  9319  zmulcl  9320  elz2  9338  zneo  9368  nneoor  9369  zeo  9372  peano5uzti  9375  zindd  9385  uzp1  9575  uzaddcl  9600  supinfneg  9609  infsupneg  9610  supminfex  9611  ublbneg  9627  eqreznegel  9628  negm  9629  qmulz  9637  qnegcl  9650  irradd  9660  irrmul  9661  fzrev2  10099  negqmod0  10345  frec2uzuzd  10416  frecuzrdgrrn  10422  frec2uzrdg  10423  frecuzrdgrcl  10424  frecuzrdgsuc  10428  frecuzrdgrclt  10429  frecuzrdgg  10430  frecuzrdgsuctlem  10437  iseqovex  10470  seq3val  10472  seqvalcd  10473  seq3-1  10474  seqf  10475  seq3p1  10476  seqovcd  10477  seqp1cd  10480  seq3clss  10481  monoord  10490  monoord2  10491  ser3mono  10492  seq3split  10493  seq3caopr3  10495  seq3caopr2  10496  iseqf1olemjpcl  10509  iseqf1olemqpcl  10510  iseqf1olemfvp  10511  seq3f1olemqsumkj  10512  seq3f1olemqsum  10514  seq3f1oleml  10517  seq3f1o  10518  seq3homo  10524  seq3z  10525  seq3distr  10527  ser3ge0  10531  expp1  10541  expcllem  10545  expcl2lemap  10546  m1expcl2  10556  facnn  10721  fac0  10722  fac1  10723  faccl  10729  facdiv  10732  facndiv  10733  bccmpl  10748  bcn2  10758  bccl  10761  fihasheqf1oi  10781  seq3coll  10836  shftlem  10839  shftf  10853  seq3shft  10861  cjval  10868  cjth  10869  remim  10883  uzin2  11010  caubnd2  11140  negfi  11250  xrmaxltsup  11280  clim  11303  clim2  11305  climshftlemg  11324  climcn1  11330  climcn2  11331  iserex  11361  climub  11366  climserle  11367  climcau  11369  serf0  11374  sumfct  11396  sumrbdclem  11399  fsum3cvg  11400  summodclem3  11402  summodclem2a  11403  zsumdc  11406  fsumgcl  11408  fsum3  11409  fsumf1o  11412  isumss  11413  isumss2  11415  fsum3cvg2  11416  fsum3ser  11419  fsumcl2lem  11420  fsumsplitf  11430  sumpr  11435  sumtp  11436  fsumm1  11438  fsum1p  11440  isummulc2  11448  fsum2dlemstep  11456  fisumcom2  11460  fsumshftm  11467  fisum0diag2  11469  fsummulc2  11470  fsumge1  11483  fsum00  11484  fsumabs  11487  telfsumo  11488  telfsumo2  11489  fsumparts  11492  fsumrelem  11493  fsumiun  11499  binomlem  11505  isumshft  11512  isum1p  11514  isumrpcl  11516  cvgratnnlemnexp  11546  cvgratnnlemmn  11547  cvgratnnlemseq  11548  cvgratnnlemabsle  11549  cvgratnnlemfm  11551  cvgratnnlemrate  11552  cvgratnn  11553  cvgratz  11554  mertenslem2  11558  mertensabs  11559  clim2prod  11561  prodfap0  11567  prodfrecap  11568  prodfdivap  11569  prodrbdclem  11593  fproddccvg  11594  prodmodclem3  11597  prodmodclem2a  11598  zproddc  11601  fprodseq  11605  prodfct  11609  fprodf1o  11610  prodssdc  11611  fprodssdc  11612  fprodmul  11613  fprodm1  11620  fprod1p  11621  fprodm1s  11623  fprodp1s  11624  fprodcl2lem  11627  fprodabs  11638  fprod2dlemstep  11644  fprodcnv  11647  fprodcom2fi  11648  fprodrec  11651  fproddivapf  11653  fprodsplitf  11654  fprodsplit1f  11656  fprodle  11662  zeo3  11887  mulsucdiv2z  11904  zob  11910  nn0o1gt2  11924  nno  11925  nn0o  11926  infssuzex  11964  infssuzcldc  11966  zsupssdc  11969  uzwodc  12052  qnumdencl  12201  pcqcl  12320  pcxnn0cl  12324  pcxcl  12325  pcgcd1  12341  dvdsprmpweqle  12350  pcmpt  12355  pcmpt2  12356  pcmptdvds  12357  infpnlem2  12372  1arith  12379  elgz  12383  mul4sq  12406  znnen  12413  ennnfonelemj0  12416  ennnfonelemg  12418  ennnfonelemom  12423  ctinfom  12443  ctiunctlemu1st  12449  ctiunctlemu2nd  12450  ctiunctlemudc  12452  ctiunctlemfo  12454  ssnnctlemct  12461  infpn2  12471  isstruct2im  12486  isstruct2r  12487  imasaddfnlemg  12753  ercpbl  12769  xpsfrnel2  12784  mgmsscl  12799  mgm1  12808  sgrppropd  12838  mndpropd  12863  issubm  12885  0subm  12897  insubm  12898  mhmima  12904  mulgsubcl  13037  issubg  13073  subgex  13076  issubg2m  13089  issubg4m  13093  0subg  13099  isnsg  13102  isnsg2  13103  nsgbi  13104  isnsg3  13107  elnmz  13108  nmzbi  13109  nmzsubg  13110  nmznsg  13113  releqgg  13120  eqgex  13121  eqgval  13123  eqgid  13126  ghmrn  13151  ghmnsgima  13162  eqgabl  13222  ablnsg  13226  isrng  13243  issrg  13274  srgfcl  13282  isring  13309  iscrng  13312  dvdsrd  13399  unitsubm  13424  issubrng  13476  subrngringnsg  13482  issubrng2  13487  opprsubrngg  13488  issubrg  13498  subrgsubm  13511  subrgugrp  13517  issubrg2  13518  issubrg3  13524  subrgpropd  13525  aprval  13528  aprsym  13530  islmod  13537  lmodlema  13538  islmodd  13539  lmodprop2d  13594  rmodislmodlem  13596  rmodislmod  13597  lsssetm  13602  islssmd  13605  lssclg  13610  lsslss  13627  lsspropdg  13677  islidlm  13725  rnglidlmcl  13726  isridlrng  13728  rnglidlmmgm  13742  isridl  13749  uniopn  13854  inopn  13856  fiinopn  13857  iscld  13956  iuncld  13968  tgrest  14022  iscn  14050  cnpval  14051  iscnp  14052  tgcn  14061  ssidcn  14063  lmbrf  14068  cnpnei  14072  cnima  14073  cnconst2  14086  cnrest2  14089  cnptopresti  14091  cnptoprest  14092  lmres  14101  lmtopcnp  14103  txbasval  14120  tx1cn  14122  tx2cn  14123  txcnp  14124  txcnmpt  14126  txdis1cn  14131  txlm  14132  cnmpt11  14136  cnmpt12  14140  cnmpt21  14144  cnmpt22  14147  ishmeo  14157  hmeoopn  14164  hmeocld  14165  qtopbasss  14374  fsumcncntop  14409  expcncf  14445  ivthinclemlopn  14467  ivthinclemlr  14468  ivthinclemuopn  14469  ivthinclemur  14470  ivthinclemdisj  14471  ivthinclemloc  14472  ivthinc  14474  ivthdec  14475  limccl  14481  ellimc3apf  14482  cnmptlimc  14496  limccoap  14500  2irrexpq  14747  2irrexpqap  14749  lgsval  14758  lgsval2lem  14764  lgsdir2lem4  14785  lgsdir2  14787  m1lgs  14805  mul2sq  14816  2sqlem6  14820  bdinex1g  15006  bj-intexr  15013  bj-prexg  15016  bj-uniex  15022  bj-uniexg  15023  bdunexb  15025  bj-indsuc  15033  exmidsbthrlem  15124  qdencn  15129  iswomni0  15153