Theorem eleq1d 2300

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 2294	. 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 1398   e. wcel 2202

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleq12d  2302  eqeltrd  2308  eqneltrd  2327  eqneltrrd  2328  rspcimdv  2912  rspcimedv  2913  reuind  3012  sbcel2g  3149  sbccsb2g  3158  breq1  4096  breq2  4097  inex1g  4230  intexr  4245  pwexg  4276  prexg  4307  opelopabsb  4360  pofun  4415  seex  4438  uniex  4540  uniexg  4542  unexb  4545  abnexg  4549  reusv3  4563  rabxfrd  4572  onun2  4594  onsucelsucexmid  4634  ordsucunielexmid  4635  dcextest  4685  tfisi  4691  peano2  4699  seinxp  4803  opabid2  4867  opeliunxp2  4876  elrn2g  4926  opeldm  4940  opeldmg  4942  elreldm  4964  elrn2  4980  opelresg  5026  elsnres  5056  iss  5065  xpexcnvm  5098  elimasng  5111  issref  5126  rnxpid  5178  unielrel  5271  dffun5r  5345  funopg  5367  brprcneu  5641  tz6.12f  5677  fvelrnb  5702  ssimaex  5716  dmfco  5723  fvmpt3  5734  mptfvex  5741  fvmptf  5748  respreima  5783  fvelrn  5786  ffnfvf  5814  ffvresb  5818  fmptco  5821  fmptcof  5822  fsn  5827  fsn2g  5830  fressnfv  5849  fnex  5884  funfvima  5896  funfvima3  5898  f1mpt  5922  fliftfuns  5949  isoselem  5971  ovrspc2v  6054  ffnov  6135  fovcld  6136  ovmpos  6155  ov2gf  6156  ovg  6171  funimassov  6182  caovclg  6185  elovmpo  6231  off  6257  caofdig  6278  fnexALT  6282  focdmex  6286  f1stres  6331  f2ndres  6332  xp1st  6337  xp2nd  6338  elxp6  6341  oprssdmm  6343  unielxp  6346  fmpox  6374  mpofvex  6379  elmpom  6412  suppofss1dcl  6442  suppofss2dcl  6443  opeliunxp2f  6447  dftpos4  6472  smoel  6509  tfrlem3-2d  6521  tfrlem8  6527  tfrlem9  6528  tfrlemibxssdm  6536  tfrlemi1  6541  tfrexlem  6543  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemaccex  6557  tfr1onlemres  6558  tfri1dALT  6560  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemaccex  6570  tfrcllemres  6571  tfrcl  6573  rdgtfr  6583  rdgon  6595  frecabex  6607  frecabcl  6608  frecfcllem  6613  frecsuclem  6615  nnacl  6691  nnmcl  6692  nnmordi  6727  nnaordex  6739  nnm00  6741  erexb  6770  qliftfuns  6831  ixpsnval  6913  elixp2  6914  resixp  6945  mptelixpg  6946  elixpsn  6947  fundmen  7024  fopwdom  7065  xpf1o  7073  dif1en  7111  diffitest  7119  diffifi  7126  inffiexmid  7141  unfiexmid  7153  unfidisj  7157  prfidceq  7163  fiintim  7166  xpfi  7167  ssfirab  7172  fnfi  7178  iunfidisj  7188  snexxph  7192  fidcenumlemr  7197  isfsupp  7214  ffsuppbi  7225  elfi2  7231  ctssdccl  7370  isnumi  7446  cc2lem  7545  cc3  7547  addnidpig  7616  indpi  7622  dfplpq2  7634  addclnq  7655  mulclnq  7656  nnnq0lem1  7726  addclnq0  7731  mulclnq0  7732  nqpnq0nq  7733  distrnq0  7739  prloc  7771  prarloclemlo  7774  prarloclem3  7777  prarloclem5  7780  genpml  7797  genpmu  7798  addnqprl  7809  addnqpru  7810  mulnqprl  7848  mulnqpru  7849  ltexprlemell  7878  ltexprlemelu  7879  ltexprlemdisj  7886  ltexprlemloc  7887  ltexprlemrl  7890  ltexprlemru  7892  ltexpri  7893  recexprlemm  7904  recexprlemdisj  7910  recexprlemloc  7911  recexprlem1ssl  7913  recexprlem1ssu  7914  recexpr  7918  addclsr  8033  mulclsr  8034  suplocsrlemb  8086  suplocsrlempr  8087  suplocsrlem  8088  suplocsr  8089  pitonn  8128  peano2nnnn  8133  axaddrcl  8145  axmulrcl  8147  peano5nnnn  8172  axpre-suploclemres  8181  negreb  8503  negf1o  8620  eqord1  8722  eqord2  8723  cju  9200  peano2nn  9214  nn1m1nn  9220  nnaddcl  9222  nnmulcl  9223  nnsub  9241  nndivtr  9244  un0addcl  9494  un0mulcl  9495  elnnnn0  9504  elz  9542  nnnegz  9543  znegclb  9573  zaddcllempos  9577  zaddcllemneg  9579  zaddcl  9580  nzadd  9593  zmulcl  9594  elz2  9612  zneo  9642  nneoor  9643  zeo  9646  peano5uzti  9649  zindd  9659  uzp1  9851  uzaddcl  9881  supinfneg  9890  infsupneg  9891  supminfex  9892  ublbneg  9908  eqreznegel  9909  negm  9910  qmulz  9918  qnegcl  9931  irradd  9941  irrmul  9942  fzrev2  10382  infssuzex  10556  infssuzcldc  10558  zsupssdc  10561  negqmod0  10656  frec2uzuzd  10727  frecuzrdgrrn  10733  frec2uzrdg  10734  frecuzrdgrcl  10735  frecuzrdgsuc  10739  frecuzrdgrclt  10740  frecuzrdgg  10741  frecuzrdgsuctlem  10748  xnn0nnen  10762  iseqovex  10783  seq3val  10785  seqvalcd  10786  seq3-1  10787  seqf  10789  seq3p1  10790  seqovcd  10792  seqp1cd  10795  seq3clss  10796  monoord  10810  monoord2  10811  ser3mono  10812  seq3split  10813  seqsplitg  10814  seq3caopr3  10816  seq3caopr2  10818  seqcaopr2g  10819  iseqf1olemjpcl  10833  iseqf1olemqpcl  10834  iseqf1olemfvp  10835  seq3f1olemqsumkj  10836  seq3f1olemqsum  10838  seq3f1oleml  10841  seq3f1o  10842  seqf1og  10846  seq3homo  10852  seq3z  10853  seqhomog  10855  seqfeq4g  10856  seq3distr  10857  ser3ge0  10861  expp1  10871  expcllem  10875  expcl2lemap  10876  m1expcl2  10886  facnn  11052  fac0  11053  fac1  11054  faccl  11060  facdiv  11063  facndiv  11064  bccmpl  11079  bcn2  11089  bccl  11092  fihasheqf1oi  11112  seq3coll  11169  ccatalpha  11256  reuccatpfxs1lem  11393  reuccatpfxs1  11394  shftlem  11456  shftf  11470  seq3shft  11478  cjval  11485  cjth  11486  remim  11500  uzin2  11627  caubnd2  11757  negfi  11868  xrmaxltsup  11898  clim  11921  clim2  11923  climshftlemg  11942  climcn1  11948  climcn2  11949  iserex  11979  climub  11984  climserle  11985  climcau  11987  serf0  11992  sumfct  12014  sumrbdclem  12018  fsum3cvg  12019  summodclem3  12021  summodclem2a  12022  zsumdc  12025  fsumgcl  12027  fsum3  12028  fsumf1o  12031  isumss  12032  isumss2  12034  fsum3cvg2  12035  fsum3ser  12038  fsumcl2lem  12039  fsumsplitf  12049  sumpr  12054  sumtp  12055  fsumm1  12057  fsum1p  12059  isummulc2  12067  fsum2dlemstep  12075  fisumcom2  12079  fsumshftm  12086  fisum0diag2  12088  fsummulc2  12089  fsumge1  12102  fsum00  12103  fsumabs  12106  telfsumo  12107  telfsumo2  12108  fsumparts  12111  fsumrelem  12112  fsumiun  12118  binomlem  12124  isumshft  12131  isum1p  12133  isumrpcl  12135  cvgratnnlemnexp  12165  cvgratnnlemmn  12166  cvgratnnlemseq  12167  cvgratnnlemabsle  12168  cvgratnnlemfm  12170  cvgratnnlemrate  12171  cvgratnn  12172  cvgratz  12173  mertenslem2  12177  mertensabs  12178  clim2prod  12180  prodfap0  12186  prodfrecap  12187  prodfdivap  12188  prodrbdclem  12212  fproddccvg  12213  prodmodclem3  12216  prodmodclem2a  12217  zproddc  12220  fprodseq  12224  prodfct  12228  fprodf1o  12229  prodssdc  12230  fprodssdc  12231  fprodmul  12232  fprodm1  12239  fprod1p  12240  fprodm1s  12242  fprodp1s  12243  fprodcl2lem  12246  fprodabs  12257  fprod2dlemstep  12263  fprodcnv  12266  fprodcom2fi  12267  fprodrec  12270  fproddivapf  12272  fprodsplitf  12273  fprodsplit1f  12275  fprodle  12281  zeo3  12509  mulsucdiv2z  12526  zob  12532  nn0o1gt2  12546  nno  12547  nn0o  12548  uzwodc  12688  qnumdencl  12839  pcqcl  12959  pcxnn0cl  12963  pcxcl  12964  pcgcd1  12981  dvdsprmpweqle  12990  pcmpt  12996  pcmpt2  12997  pcmptdvds  12998  infpnlem2  13013  1arith  13020  elgz  13024  mul4sq  13047  4sqlem13m  13056  4sqlem17  13060  4sqlem18  13061  4sqlem19  13062  znnen  13099  ennnfonelemj0  13102  ennnfonelemg  13104  ennnfonelemom  13109  ctinfom  13129  ctiunctlemu1st  13135  ctiunctlemu2nd  13136  ctiunctlemudc  13138  ctiunctlemfo  13140  ssnnctlemct  13147  infpn2  13157  isstruct2im  13172  isstruct2r  13173  imasaddfnlemg  13477  ercpbl  13494  xpsfrnel2  13509  mgmsscl  13524  mgm1  13533  sgrppropd  13576  mndpropd  13603  issubm  13635  0subm  13647  insubm  13648  mhmima  13654  mulgsubcl  13803  issubg  13840  subgex  13843  issubg2m  13856  issubg4m  13860  0subg  13866  isnsg  13869  isnsg2  13870  nsgbi  13871  isnsg3  13874  elnmz  13875  nmzbi  13876  nmzsubg  13877  nmznsg  13880  releqgg  13887  eqgex  13888  eqgval  13890  eqgid  13893  ghmrn  13924  ghmnsgima  13935  eqgabl  13997  ablnsg  14001  gsumfzmhm2  14011  isrng  14028  issrg  14059  srgfcl  14067  isring  14094  iscrng  14097  dvdsrd  14189  unitsubm  14214  isrim0  14256  issubrng  14294  subrngringnsg  14300  issubrng2  14305  opprsubrngg  14306  issubrg  14316  subrgsubm  14329  subrgugrp  14335  issubrg2  14336  issubrg3  14342  subrgpropd  14348  aprval  14378  aprsym  14380  islmod  14387  lmodlema  14388  islmodd  14389  lmodprop2d  14444  rmodislmodlem  14446  rmodislmod  14447  lsssetm  14452  islssmd  14455  lssclg  14460  lsslss  14477  lsspropdg  14527  islidlm  14575  rnglidlmcl  14576  isridlrng  14578  rnglidlmmgm  14592  isridl  14600  gsumfzfsumlemm  14683  psrbag  14765  psr1clfi  14789  uniopn  14812  inopn  14814  fiinopn  14815  iscld  14914  iuncld  14926  tgrest  14980  iscn  15008  cnpval  15009  iscnp  15010  tgcn  15019  ssidcn  15021  lmbrf  15026  cnpnei  15030  cnima  15031  cnconst2  15044  cnrest2  15047  cnptopresti  15049  cnptoprest  15050  lmres  15059  lmtopcnp  15061  txbasval  15078  tx1cn  15080  tx2cn  15081  txcnp  15082  txcnmpt  15084  txdis1cn  15089  txlm  15090  cnmpt11  15094  cnmpt12  15098  cnmpt21  15102  cnmpt22  15105  ishmeo  15115  hmeoopn  15122  hmeocld  15123  qtopbasss  15332  fsumcncntop  15378  expcn  15380  expcncf  15420  ivthinclemlopn  15447  ivthinclemlr  15448  ivthinclemuopn  15449  ivthinclemur  15450  ivthinclemdisj  15451  ivthinclemloc  15452  ivthinc  15454  ivthdec  15455  limccl  15470  ellimc3apf  15471  cnmptlimc  15485  limccoap  15489  dvmptfsum  15536  plycolemc  15569  plycj  15572  2irrexpq  15787  2irrexpqap  15789  pellexlem1  15791  fsumdvdsmul  15805  perfect  15815  lgsval  15823  lgsval2lem  15829  lgsdir2lem4  15850  lgsdir2  15852  m1lgs  15904  2lgs  15923  mul2sq  15935  2sqlem6  15939  wlkcprim  16291  isclwwlk  16335  clwwlk1loop  16340  clwwlkccatlem  16341  clwwlkn1  16359  loopclwwlkn1b  16360  clwwlkn1loopb  16361  clwwlkn2  16362  clwwlkext2edg  16363  umgr2cwwk2dif  16365  s2elclwwlknon2  16377  clwwlknonex2lem2  16379  clwwlknonex2  16380  eupth2lem2dc  16400  eulerpathprum  16421  bdinex1g  16617  bj-intexr  16624  bj-prexg  16627  bj-uniex  16633  bj-uniexg  16634  bdunexb  16636  bj-indsuc  16644  exmidsbthrlem  16750  qdencn  16755  repiecef  16760  iswomni0  16784  gfsumval  16809  gfsumcl  16816