Theorem eleq1d 2301

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 2295	. 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 2203

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 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  eleq12d  2303  eqeltrd  2309  eqneltrd  2328  eqneltrrd  2329  rspcimdv  2922  rspcimedv  2923  reuind  3022  sbcel2g  3159  sbccsb2g  3168  breq1  4112  breq2  4113  inex1g  4246  intexr  4262  pwexg  4293  prexg  4325  opelopabsb  4378  pofun  4433  seex  4456  uniex  4558  uniexg  4560  unexb  4563  abnexg  4567  reusv3  4581  rabxfrd  4590  onun2  4612  onsucelsucexmid  4652  ordsucunielexmid  4653  dcextest  4703  tfisi  4709  peano2  4717  seinxp  4821  opabid2  4886  opeliunxp2  4895  elrn2g  4945  opeldm  4959  opeldmg  4961  elreldm  4983  elrn2  4999  opelresg  5045  elsnres  5075  iss  5084  xpexcnvm  5117  elimasng  5130  issref  5145  rnxpid  5197  unielrel  5290  dffun5r  5364  funopg  5386  brprcneu  5663  tz6.12f  5699  fvelrnb  5724  ssimaex  5738  dmfco  5745  fvmpt3  5756  mptfvex  5763  fvmptf  5770  respreima  5805  fvelrn  5808  ffnfvf  5836  ffvresb  5840  fmptco  5843  fmptcof  5844  fsn  5849  fsn2g  5852  fressnfv  5871  fnex  5906  funfvima  5918  funfvima3  5920  f1mpt  5944  fliftfuns  5971  isoselem  5993  ovrspc2v  6076  ffnov  6157  fovcld  6158  ovmpos  6177  ov2gf  6178  ovg  6193  funimassov  6204  caovclg  6207  elovmpo  6253  off  6279  caofdig  6300  fnexALT  6304  focdmex  6308  f1stres  6353  f2ndres  6354  xp1st  6359  xp2nd  6360  elxp6  6363  oprssdmm  6365  unielxp  6368  fmpox  6396  mpofvex  6401  elmpom  6434  suppofss1dcl  6464  suppofss2dcl  6465  opeliunxp2f  6469  dftpos4  6494  smoel  6531  tfrlem3-2d  6543  tfrlem8  6549  tfrlem9  6550  tfrlemibxssdm  6558  tfrlemi1  6563  tfrexlem  6565  tfr1onlemsucfn  6571  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfr1onlemaccex  6579  tfr1onlemres  6580  tfri1dALT  6582  tfrcllemsucfn  6584  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllembfn  6588  tfrcllemaccex  6592  tfrcllemres  6593  tfrcl  6595  rdgtfr  6605  rdgon  6617  frecabex  6629  frecabcl  6630  frecfcllem  6635  frecsuclem  6637  nnacl  6713  nnmcl  6714  nnmordi  6749  nnaordex  6761  nnm00  6763  erexb  6792  qliftfuns  6853  ixpsnval  6936  elixp2  6937  resixp  6968  mptelixpg  6969  elixpsn  6970  fundmen  7047  fopwdom  7089  xpf1o  7097  dif1en  7136  diffitest  7144  diffifi  7151  inffiexmid  7166  unfiexmid  7178  unfidisj  7182  prfidceq  7188  fiintim  7191  xpfi  7192  ssfirab  7197  fnfi  7203  iunfidisj  7213  mapfi  7214  snexxph  7220  fidcenumlemr  7225  isfsupp  7242  ffsuppbi  7253  elfi2  7259  ctssdccl  7402  isnumi  7478  cc2lem  7580  cc3  7582  addnidpig  7651  indpi  7657  dfplpq2  7669  addclnq  7690  mulclnq  7691  nnnq0lem1  7761  addclnq0  7766  mulclnq0  7767  nqpnq0nq  7768  distrnq0  7774  prloc  7806  prarloclemlo  7809  prarloclem3  7812  prarloclem5  7815  genpml  7832  genpmu  7833  addnqprl  7844  addnqpru  7845  mulnqprl  7883  mulnqpru  7884  ltexprlemell  7913  ltexprlemelu  7914  ltexprlemdisj  7921  ltexprlemloc  7922  ltexprlemrl  7925  ltexprlemru  7927  ltexpri  7928  recexprlemm  7939  recexprlemdisj  7945  recexprlemloc  7946  recexprlem1ssl  7948  recexprlem1ssu  7949  recexpr  7953  addclsr  8068  mulclsr  8069  suplocsrlemb  8121  suplocsrlempr  8122  suplocsrlem  8123  suplocsr  8124  pitonn  8163  peano2nnnn  8168  axaddrcl  8180  axmulrcl  8182  peano5nnnn  8207  axpre-suploclemres  8216  negreb  8538  negf1o  8655  eqord1  8757  eqord2  8758  cju  9235  peano2nn  9249  nn1m1nn  9255  nnaddcl  9257  nnmulcl  9258  nnsub  9276  nndivtr  9279  un0addcl  9529  un0mulcl  9530  elnnnn0  9539  fcdmnn0fsuppg  9551  elz  9579  nnnegz  9580  znegclb  9610  zaddcllempos  9614  zaddcllemneg  9616  zaddcl  9617  nzadd  9630  zmulcl  9631  elz2  9649  zneo  9679  nneoor  9680  zeo  9683  peano5uzti  9686  zindd  9696  uzp1  9888  uzaddcl  9918  supinfneg  9927  infsupneg  9928  supminfex  9929  ublbneg  9945  eqreznegel  9946  negm  9947  qmulz  9955  qnegcl  9968  irradd  9978  irrmul  9979  fzrev2  10419  infssuzex  10593  infssuzcldc  10595  zsupssdc  10598  negqmod0  10693  frec2uzuzd  10764  frecuzrdgrrn  10770  frec2uzrdg  10771  frecuzrdgrcl  10772  frecuzrdgsuc  10776  frecuzrdgrclt  10777  frecuzrdgg  10778  frecuzrdgsuctlem  10785  xnn0nnen  10799  iseqovex  10820  seq3val  10822  seqvalcd  10823  seq3-1  10824  seqf  10826  seq3p1  10827  seqovcd  10829  seqp1cd  10832  seq3clss  10833  monoord  10847  monoord2  10848  ser3mono  10849  seq3split  10850  seqsplitg  10851  seq3caopr3  10853  seq3caopr2  10855  seqcaopr2g  10856  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  iseqf1olemfvp  10872  seq3f1olemqsumkj  10873  seq3f1olemqsum  10875  seq3f1oleml  10878  seq3f1o  10879  seqf1og  10883  seq3homo  10889  seq3z  10890  seqhomog  10892  seqfeq4g  10893  seq3distr  10894  ser3ge0  10898  expp1  10908  expcllem  10912  expcl2lemap  10913  m1expcl2  10923  facnn  11089  fac0  11090  fac1  11091  faccl  11097  facdiv  11100  facndiv  11101  bccmpl  11116  bcn2  11126  bccl  11129  fihasheqf1oi  11150  seq3coll  11214  ccatalpha  11301  reuccatpfxs1lem  11438  reuccatpfxs1  11439  shftlem  11501  shftf  11515  seq3shft  11523  cjval  11530  cjth  11531  remim  11545  uzin2  11672  caubnd2  11802  negfi  11913  xrmaxltsup  11943  clim  11966  clim2  11968  climshftlemg  11987  climcn1  11993  climcn2  11994  iserex  12024  climub  12029  climserle  12030  climcau  12032  serf0  12037  sumfct  12059  sumrbdclem  12063  fsum3cvg  12064  summodclem3  12066  summodclem2a  12067  zsumdc  12070  fsumgcl  12072  fsum3  12073  fsumf1o  12076  isumss  12077  isumss2  12079  fsum3cvg2  12080  fsum3ser  12083  fsumcl2lem  12084  fsumsplitf  12094  sumpr  12099  sumtp  12100  fsumm1  12102  fsum1p  12104  isummulc2  12112  fsum2dlemstep  12120  fisumcom2  12124  fsumshftm  12131  fisum0diag2  12133  fsummulc2  12134  fsumge1  12147  fsum00  12148  fsumabs  12151  telfsumo  12152  telfsumo2  12153  fsumparts  12156  fsumrelem  12157  fsumiun  12163  binomlem  12169  isumshft  12176  isum1p  12178  isumrpcl  12180  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  cvgratnnlemseq  12212  cvgratnnlemabsle  12213  cvgratnnlemfm  12215  cvgratnnlemrate  12216  cvgratnn  12217  cvgratz  12218  mertenslem2  12222  mertensabs  12223  clim2prod  12225  prodfap0  12231  prodfrecap  12232  prodfdivap  12233  prodrbdclem  12257  fproddccvg  12258  prodmodclem3  12261  prodmodclem2a  12262  zproddc  12265  fprodseq  12269  prodfct  12273  fprodf1o  12274  prodssdc  12275  fprodssdc  12276  fprodmul  12277  fprodm1  12284  fprod1p  12285  fprodm1s  12287  fprodp1s  12288  fprodcl2lem  12291  fprodabs  12302  fprod2dlemstep  12308  fprodcnv  12311  fprodcom2fi  12312  fprodrec  12315  fproddivapf  12317  fprodsplitf  12318  fprodsplit1f  12320  fprodle  12326  zeo3  12554  mulsucdiv2z  12571  zob  12577  nn0o1gt2  12591  nno  12592  nn0o  12593  uzwodc  12733  qnumdencl  12884  pcqcl  13004  pcxnn0cl  13008  pcxcl  13009  pcgcd1  13026  dvdsprmpweqle  13035  pcmpt  13041  pcmpt2  13042  pcmptdvds  13043  infpnlem2  13058  1arith  13065  elgz  13069  mul4sq  13092  4sqlem13m  13101  4sqlem17  13105  4sqlem18  13106  4sqlem19  13107  znnen  13149  ennnfonelemj0  13152  ennnfonelemg  13154  ennnfonelemom  13159  ctinfom  13179  ctiunctlemu1st  13185  ctiunctlemu2nd  13186  ctiunctlemudc  13188  ctiunctlemfo  13190  ssnnctlemct  13197  infpn2  13207  isstruct2im  13222  isstruct2r  13223  imasaddfnlemg  13527  ercpbl  13544  xpsfrnel2  13559  mgmsscl  13574  mgm1  13583  sgrppropd  13626  mndpropd  13653  issubm  13685  0subm  13697  insubm  13698  mhmima  13704  mulgsubcl  13853  issubg  13890  subgex  13893  issubg2m  13906  issubg4m  13910  0subg  13916  isnsg  13919  isnsg2  13920  nsgbi  13921  isnsg3  13924  elnmz  13925  nmzbi  13926  nmzsubg  13927  nmznsg  13930  releqgg  13937  eqgex  13938  eqgval  13940  eqgid  13943  ghmrn  13974  ghmnsgima  13985  eqgabl  14047  ablnsg  14051  gsumfzmhm2  14061  isrng  14078  issrg  14109  srgfcl  14117  isring  14144  iscrng  14147  dvdsrd  14239  unitsubm  14264  isrim0  14306  issubrng  14344  subrngringnsg  14350  issubrng2  14355  opprsubrngg  14356  issubrg  14366  subrgsubm  14379  subrgugrp  14385  issubrg2  14386  issubrg3  14392  subrgpropd  14398  aprval  14428  aprsym  14430  islmod  14439  lmodlema  14440  islmodd  14441  lmodprop2d  14496  rmodislmodlem  14498  rmodislmod  14499  lsssetm  14504  islssmd  14507  lssclg  14512  lsslss  14529  lsspropdg  14579  islidlm  14627  rnglidlmcl  14628  isridlrng  14630  rnglidlmmgm  14644  isridl  14652  gsumfzfsumlemm  14735  psrbag  14817  psr1clfi  14843  uniopn  14866  inopn  14868  fiinopn  14869  iscld  14968  iuncld  14980  tgrest  15034  iscn  15062  cnpval  15063  iscnp  15064  tgcn  15073  ssidcn  15075  lmbrf  15080  cnpnei  15084  cnima  15085  cnconst2  15098  cnrest2  15101  cnptopresti  15103  cnptoprest  15104  lmres  15113  lmtopcnp  15115  txbasval  15132  tx1cn  15134  tx2cn  15135  txcnp  15136  txcnmpt  15138  txdis1cn  15143  txlm  15144  cnmpt11  15148  cnmpt12  15152  cnmpt21  15156  cnmpt22  15159  ishmeo  15169  hmeoopn  15176  hmeocld  15177  qtopbasss  15386  fsumcncntop  15432  expcn  15434  expcncf  15474  ivthinclemlopn  15501  ivthinclemlr  15502  ivthinclemuopn  15503  ivthinclemur  15504  ivthinclemdisj  15505  ivthinclemloc  15506  ivthinc  15508  ivthdec  15509  limccl  15524  ellimc3apf  15525  cnmptlimc  15539  limccoap  15543  dvmptfsum  15590  plycolemc  15623  plycj  15626  2irrexpq  15841  2irrexpqap  15843  pellexlem1  15845  fsumdvdsmul  15859  perfect  15869  lgsval  15877  lgsval2lem  15883  lgsdir2lem4  15904  lgsdir2  15906  m1lgs  15958  2lgs  15977  mul2sq  15989  2sqlem6  15993  wlkcprim  16345  isclwwlk  16389  clwwlk1loop  16394  clwwlkccatlem  16395  clwwlkn1  16413  loopclwwlkn1b  16414  clwwlkn1loopb  16415  clwwlkn2  16416  clwwlkext2edg  16417  umgr2cwwk2dif  16419  s2elclwwlknon2  16431  clwwlknonex2lem2  16433  clwwlknonex2  16434  eupth2lem2dc  16454  eulerpathprum  16475  bdinex1g  16671  bj-intexr  16678  bj-prexg  16681  bj-uniex  16687  bj-uniexg  16688  bdunexb  16690  bj-indsuc  16698  exmidsbthrlem  16802  qdencn  16807  repiecef  16812  iswomni0  16836  gfsumval  16862  gfsumcl  16870