Theorem eleq1d 2274

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 2268	. 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 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eleq12d  2276  eqeltrd  2282  eqneltrd  2301  eqneltrrd  2302  rspcimdv  2878  rspcimedv  2879  reuind  2978  sbcel2g  3114  sbccsb2g  3123  breq1  4048  breq2  4049  inex1g  4181  intexr  4195  pwexg  4225  prexg  4256  opelopabsb  4307  pofun  4360  seex  4383  uniex  4485  uniexg  4487  unexb  4490  abnexg  4494  reusv3  4508  rabxfrd  4517  onun2  4539  onsucelsucexmid  4579  ordsucunielexmid  4580  dcextest  4630  tfisi  4636  peano2  4644  seinxp  4747  opabid2  4810  opeliunxp2  4819  elrn2g  4869  opeldm  4882  opeldmg  4884  elreldm  4905  elrn2  4921  opelresg  4967  elsnres  4997  iss  5006  elimasng  5051  issref  5066  rnxpid  5118  unielrel  5211  dffun5r  5284  funopg  5306  brprcneu  5571  tz6.12f  5607  fvelrnb  5628  ssimaex  5642  dmfco  5649  fvmpt3  5660  mptfvex  5667  fvmptf  5674  respreima  5710  fvelrn  5713  ffnfvf  5741  ffvresb  5745  fmptco  5748  fmptcof  5749  fsn  5754  fressnfv  5773  fnex  5808  funfvima  5818  funfvima3  5820  f1mpt  5842  fliftfuns  5869  isoselem  5891  ovrspc2v  5972  ffnov  6051  fovcld  6052  ovmpos  6071  ov2gf  6072  ovg  6087  funimassov  6098  caovclg  6101  elovmpo  6147  off  6173  caofdig  6194  fnexALT  6198  focdmex  6202  f1stres  6247  f2ndres  6248  xp1st  6253  xp2nd  6254  elxp6  6257  oprssdmm  6259  unielxp  6262  fmpox  6288  mpofvex  6293  opeliunxp2f  6326  dftpos4  6351  smoel  6388  tfrlem3-2d  6400  tfrlem8  6406  tfrlem9  6407  tfrlemibxssdm  6415  tfrlemi1  6420  tfrexlem  6422  tfr1onlemsucfn  6428  tfr1onlemsucaccv  6429  tfr1onlembxssdm  6431  tfr1onlembfn  6432  tfr1onlemaccex  6436  tfr1onlemres  6437  tfri1dALT  6439  tfrcllemsucfn  6441  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllembfn  6445  tfrcllemaccex  6449  tfrcllemres  6450  tfrcl  6452  rdgtfr  6462  rdgon  6474  frecabex  6486  frecabcl  6487  frecfcllem  6492  frecsuclem  6494  nnacl  6568  nnmcl  6569  nnmordi  6604  nnaordex  6616  nnm00  6618  erexb  6647  qliftfuns  6708  ixpsnval  6790  elixp2  6791  resixp  6822  mptelixpg  6823  elixpsn  6824  fundmen  6900  fopwdom  6935  xpf1o  6943  dif1en  6978  diffitest  6986  diffifi  6993  inffiexmid  7005  unfiexmid  7017  unfidisj  7021  prfidceq  7027  fiintim  7030  xpfi  7031  ssfirab  7035  fnfi  7040  iunfidisj  7050  snexxph  7054  fidcenumlemr  7059  elfi2  7076  ctssdccl  7215  isnumi  7291  cc2lem  7380  cc3  7382  addnidpig  7451  indpi  7457  dfplpq2  7469  addclnq  7490  mulclnq  7491  nnnq0lem1  7561  addclnq0  7566  mulclnq0  7567  nqpnq0nq  7568  distrnq0  7574  prloc  7606  prarloclemlo  7609  prarloclem3  7612  prarloclem5  7615  genpml  7632  genpmu  7633  addnqprl  7644  addnqpru  7645  mulnqprl  7683  mulnqpru  7684  ltexprlemell  7713  ltexprlemelu  7714  ltexprlemdisj  7721  ltexprlemloc  7722  ltexprlemrl  7725  ltexprlemru  7727  ltexpri  7728  recexprlemm  7739  recexprlemdisj  7745  recexprlemloc  7746  recexprlem1ssl  7748  recexprlem1ssu  7749  recexpr  7753  addclsr  7868  mulclsr  7869  suplocsrlemb  7921  suplocsrlempr  7922  suplocsrlem  7923  suplocsr  7924  pitonn  7963  peano2nnnn  7968  axaddrcl  7980  axmulrcl  7982  peano5nnnn  8007  axpre-suploclemres  8016  negreb  8339  negf1o  8456  eqord1  8558  eqord2  8559  cju  9036  peano2nn  9050  nn1m1nn  9056  nnaddcl  9058  nnmulcl  9059  nnsub  9077  nndivtr  9080  un0addcl  9330  un0mulcl  9331  elnnnn0  9340  elz  9376  nnnegz  9377  znegclb  9407  zaddcllempos  9411  zaddcllemneg  9413  zaddcl  9414  nzadd  9427  zmulcl  9428  elz2  9446  zneo  9476  nneoor  9477  zeo  9480  peano5uzti  9483  zindd  9493  uzp1  9684  uzaddcl  9709  supinfneg  9718  infsupneg  9719  supminfex  9720  ublbneg  9736  eqreznegel  9737  negm  9738  qmulz  9746  qnegcl  9759  irradd  9769  irrmul  9770  fzrev2  10209  infssuzex  10378  infssuzcldc  10380  zsupssdc  10383  negqmod0  10478  frec2uzuzd  10549  frecuzrdgrrn  10555  frec2uzrdg  10556  frecuzrdgrcl  10557  frecuzrdgsuc  10561  frecuzrdgrclt  10562  frecuzrdgg  10563  frecuzrdgsuctlem  10570  xnn0nnen  10584  iseqovex  10605  seq3val  10607  seqvalcd  10608  seq3-1  10609  seqf  10611  seq3p1  10612  seqovcd  10614  seqp1cd  10617  seq3clss  10618  monoord  10632  monoord2  10633  ser3mono  10634  seq3split  10635  seqsplitg  10636  seq3caopr3  10638  seq3caopr2  10640  seqcaopr2g  10641  iseqf1olemjpcl  10655  iseqf1olemqpcl  10656  iseqf1olemfvp  10657  seq3f1olemqsumkj  10658  seq3f1olemqsum  10660  seq3f1oleml  10663  seq3f1o  10664  seqf1og  10668  seq3homo  10674  seq3z  10675  seqhomog  10677  seqfeq4g  10678  seq3distr  10679  ser3ge0  10683  expp1  10693  expcllem  10697  expcl2lemap  10698  m1expcl2  10708  facnn  10874  fac0  10875  fac1  10876  faccl  10882  facdiv  10885  facndiv  10886  bccmpl  10901  bcn2  10911  bccl  10914  fihasheqf1oi  10934  seq3coll  10989  shftlem  11160  shftf  11174  seq3shft  11182  cjval  11189  cjth  11190  remim  11204  uzin2  11331  caubnd2  11461  negfi  11572  xrmaxltsup  11602  clim  11625  clim2  11627  climshftlemg  11646  climcn1  11652  climcn2  11653  iserex  11683  climub  11688  climserle  11689  climcau  11691  serf0  11696  sumfct  11718  sumrbdclem  11721  fsum3cvg  11722  summodclem3  11724  summodclem2a  11725  zsumdc  11728  fsumgcl  11730  fsum3  11731  fsumf1o  11734  isumss  11735  isumss2  11737  fsum3cvg2  11738  fsum3ser  11741  fsumcl2lem  11742  fsumsplitf  11752  sumpr  11757  sumtp  11758  fsumm1  11760  fsum1p  11762  isummulc2  11770  fsum2dlemstep  11778  fisumcom2  11782  fsumshftm  11789  fisum0diag2  11791  fsummulc2  11792  fsumge1  11805  fsum00  11806  fsumabs  11809  telfsumo  11810  telfsumo2  11811  fsumparts  11814  fsumrelem  11815  fsumiun  11821  binomlem  11827  isumshft  11834  isum1p  11836  isumrpcl  11838  cvgratnnlemnexp  11868  cvgratnnlemmn  11869  cvgratnnlemseq  11870  cvgratnnlemabsle  11871  cvgratnnlemfm  11873  cvgratnnlemrate  11874  cvgratnn  11875  cvgratz  11876  mertenslem2  11880  mertensabs  11881  clim2prod  11883  prodfap0  11889  prodfrecap  11890  prodfdivap  11891  prodrbdclem  11915  fproddccvg  11916  prodmodclem3  11919  prodmodclem2a  11920  zproddc  11923  fprodseq  11927  prodfct  11931  fprodf1o  11932  prodssdc  11933  fprodssdc  11934  fprodmul  11935  fprodm1  11942  fprod1p  11943  fprodm1s  11945  fprodp1s  11946  fprodcl2lem  11949  fprodabs  11960  fprod2dlemstep  11966  fprodcnv  11969  fprodcom2fi  11970  fprodrec  11973  fproddivapf  11975  fprodsplitf  11976  fprodsplit1f  11978  fprodle  11984  zeo3  12212  mulsucdiv2z  12229  zob  12235  nn0o1gt2  12249  nno  12250  nn0o  12251  uzwodc  12391  qnumdencl  12542  pcqcl  12662  pcxnn0cl  12666  pcxcl  12667  pcgcd1  12684  dvdsprmpweqle  12693  pcmpt  12699  pcmpt2  12700  pcmptdvds  12701  infpnlem2  12716  1arith  12723  elgz  12727  mul4sq  12750  4sqlem13m  12759  4sqlem17  12763  4sqlem18  12764  4sqlem19  12765  znnen  12802  ennnfonelemj0  12805  ennnfonelemg  12807  ennnfonelemom  12812  ctinfom  12832  ctiunctlemu1st  12838  ctiunctlemu2nd  12839  ctiunctlemudc  12841  ctiunctlemfo  12843  ssnnctlemct  12850  infpn2  12860  isstruct2im  12875  isstruct2r  12876  imasaddfnlemg  13179  ercpbl  13196  xpsfrnel2  13211  mgmsscl  13226  mgm1  13235  sgrppropd  13278  mndpropd  13305  issubm  13337  0subm  13349  insubm  13350  mhmima  13356  mulgsubcl  13505  issubg  13542  subgex  13545  issubg2m  13558  issubg4m  13562  0subg  13568  isnsg  13571  isnsg2  13572  nsgbi  13573  isnsg3  13576  elnmz  13577  nmzbi  13578  nmzsubg  13579  nmznsg  13582  releqgg  13589  eqgex  13590  eqgval  13592  eqgid  13595  ghmrn  13626  ghmnsgima  13637  eqgabl  13699  ablnsg  13703  gsumfzmhm2  13713  isrng  13729  issrg  13760  srgfcl  13768  isring  13795  iscrng  13798  dvdsrd  13889  unitsubm  13914  isrim0  13956  issubrng  13994  subrngringnsg  14000  issubrng2  14005  opprsubrngg  14006  issubrg  14016  subrgsubm  14029  subrgugrp  14035  issubrg2  14036  issubrg3  14042  subrgpropd  14048  aprval  14077  aprsym  14079  islmod  14086  lmodlema  14087  islmodd  14088  lmodprop2d  14143  rmodislmodlem  14145  rmodislmod  14146  lsssetm  14151  islssmd  14154  lssclg  14159  lsslss  14176  lsspropdg  14226  islidlm  14274  rnglidlmcl  14275  isridlrng  14277  rnglidlmmgm  14291  isridl  14299  gsumfzfsumlemm  14382  psrbag  14464  psr1clfi  14483  uniopn  14506  inopn  14508  fiinopn  14509  iscld  14608  iuncld  14620  tgrest  14674  iscn  14702  cnpval  14703  iscnp  14704  tgcn  14713  ssidcn  14715  lmbrf  14720  cnpnei  14724  cnima  14725  cnconst2  14738  cnrest2  14741  cnptopresti  14743  cnptoprest  14744  lmres  14753  lmtopcnp  14755  txbasval  14772  tx1cn  14774  tx2cn  14775  txcnp  14776  txcnmpt  14778  txdis1cn  14783  txlm  14784  cnmpt11  14788  cnmpt12  14792  cnmpt21  14796  cnmpt22  14799  ishmeo  14809  hmeoopn  14816  hmeocld  14817  qtopbasss  15026  fsumcncntop  15072  expcn  15074  expcncf  15114  ivthinclemlopn  15141  ivthinclemlr  15142  ivthinclemuopn  15143  ivthinclemur  15144  ivthinclemdisj  15145  ivthinclemloc  15146  ivthinc  15148  ivthdec  15149  limccl  15164  ellimc3apf  15165  cnmptlimc  15179  limccoap  15183  dvmptfsum  15230  plycolemc  15263  plycj  15266  2irrexpq  15481  2irrexpqap  15483  fsumdvdsmul  15496  perfect  15506  lgsval  15514  lgsval2lem  15520  lgsdir2lem4  15541  lgsdir2  15543  m1lgs  15595  2lgs  15614  mul2sq  15626  2sqlem6  15630  bdinex1g  15874  bj-intexr  15881  bj-prexg  15884  bj-uniex  15890  bj-uniexg  15891  bdunexb  15893  bj-indsuc  15901  exmidsbthrlem  15998  qdencn  16003  iswomni0  16027