Theorem eleq1d 2298

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 2292	. 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 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

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

This theorem is referenced by:  eleq12d  2300  eqeltrd  2306  eqneltrd  2325  eqneltrrd  2326  rspcimdv  2908  rspcimedv  2909  reuind  3008  sbcel2g  3145  sbccsb2g  3154  breq1  4086  breq2  4087  inex1g  4220  intexr  4234  pwexg  4264  prexg  4295  opelopabsb  4348  pofun  4403  seex  4426  uniex  4528  uniexg  4530  unexb  4533  abnexg  4537  reusv3  4551  rabxfrd  4560  onun2  4582  onsucelsucexmid  4622  ordsucunielexmid  4623  dcextest  4673  tfisi  4679  peano2  4687  seinxp  4790  opabid2  4853  opeliunxp2  4862  elrn2g  4912  opeldm  4926  opeldmg  4928  elreldm  4950  elrn2  4966  opelresg  5012  elsnres  5042  iss  5051  elimasng  5096  issref  5111  rnxpid  5163  unielrel  5256  dffun5r  5330  funopg  5352  brprcneu  5620  tz6.12f  5656  fvelrnb  5681  ssimaex  5695  dmfco  5702  fvmpt3  5713  mptfvex  5720  fvmptf  5727  respreima  5763  fvelrn  5766  ffnfvf  5794  ffvresb  5798  fmptco  5801  fmptcof  5802  fsn  5807  fressnfv  5826  fnex  5861  funfvima  5871  funfvima3  5873  f1mpt  5895  fliftfuns  5922  isoselem  5944  ovrspc2v  6027  ffnov  6108  fovcld  6109  ovmpos  6128  ov2gf  6129  ovg  6144  funimassov  6155  caovclg  6158  elovmpo  6204  off  6231  caofdig  6252  fnexALT  6256  focdmex  6260  f1stres  6305  f2ndres  6306  xp1st  6311  xp2nd  6312  elxp6  6315  oprssdmm  6317  unielxp  6320  fmpox  6346  mpofvex  6351  opeliunxp2f  6384  dftpos4  6409  smoel  6446  tfrlem3-2d  6458  tfrlem8  6464  tfrlem9  6465  tfrlemibxssdm  6473  tfrlemi1  6478  tfrexlem  6480  tfr1onlemsucfn  6486  tfr1onlemsucaccv  6487  tfr1onlembxssdm  6489  tfr1onlembfn  6490  tfr1onlemaccex  6494  tfr1onlemres  6495  tfri1dALT  6497  tfrcllemsucfn  6499  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllembfn  6503  tfrcllemaccex  6507  tfrcllemres  6508  tfrcl  6510  rdgtfr  6520  rdgon  6532  frecabex  6544  frecabcl  6545  frecfcllem  6550  frecsuclem  6552  nnacl  6626  nnmcl  6627  nnmordi  6662  nnaordex  6674  nnm00  6676  erexb  6705  qliftfuns  6766  ixpsnval  6848  elixp2  6849  resixp  6880  mptelixpg  6881  elixpsn  6882  fundmen  6959  fopwdom  6997  xpf1o  7005  dif1en  7041  diffitest  7049  diffifi  7056  inffiexmid  7068  unfiexmid  7080  unfidisj  7084  prfidceq  7090  fiintim  7093  xpfi  7094  ssfirab  7098  fnfi  7103  iunfidisj  7113  snexxph  7117  fidcenumlemr  7122  elfi2  7139  ctssdccl  7278  isnumi  7354  cc2lem  7452  cc3  7454  addnidpig  7523  indpi  7529  dfplpq2  7541  addclnq  7562  mulclnq  7563  nnnq0lem1  7633  addclnq0  7638  mulclnq0  7639  nqpnq0nq  7640  distrnq0  7646  prloc  7678  prarloclemlo  7681  prarloclem3  7684  prarloclem5  7687  genpml  7704  genpmu  7705  addnqprl  7716  addnqpru  7717  mulnqprl  7755  mulnqpru  7756  ltexprlemell  7785  ltexprlemelu  7786  ltexprlemdisj  7793  ltexprlemloc  7794  ltexprlemrl  7797  ltexprlemru  7799  ltexpri  7800  recexprlemm  7811  recexprlemdisj  7817  recexprlemloc  7818  recexprlem1ssl  7820  recexprlem1ssu  7821  recexpr  7825  addclsr  7940  mulclsr  7941  suplocsrlemb  7993  suplocsrlempr  7994  suplocsrlem  7995  suplocsr  7996  pitonn  8035  peano2nnnn  8040  axaddrcl  8052  axmulrcl  8054  peano5nnnn  8079  axpre-suploclemres  8088  negreb  8411  negf1o  8528  eqord1  8630  eqord2  8631  cju  9108  peano2nn  9122  nn1m1nn  9128  nnaddcl  9130  nnmulcl  9131  nnsub  9149  nndivtr  9152  un0addcl  9402  un0mulcl  9403  elnnnn0  9412  elz  9448  nnnegz  9449  znegclb  9479  zaddcllempos  9483  zaddcllemneg  9485  zaddcl  9486  nzadd  9499  zmulcl  9500  elz2  9518  zneo  9548  nneoor  9549  zeo  9552  peano5uzti  9555  zindd  9565  uzp1  9756  uzaddcl  9781  supinfneg  9790  infsupneg  9791  supminfex  9792  ublbneg  9808  eqreznegel  9809  negm  9810  qmulz  9818  qnegcl  9831  irradd  9841  irrmul  9842  fzrev2  10281  infssuzex  10453  infssuzcldc  10455  zsupssdc  10458  negqmod0  10553  frec2uzuzd  10624  frecuzrdgrrn  10630  frec2uzrdg  10631  frecuzrdgrcl  10632  frecuzrdgsuc  10636  frecuzrdgrclt  10637  frecuzrdgg  10638  frecuzrdgsuctlem  10645  xnn0nnen  10659  iseqovex  10680  seq3val  10682  seqvalcd  10683  seq3-1  10684  seqf  10686  seq3p1  10687  seqovcd  10689  seqp1cd  10692  seq3clss  10693  monoord  10707  monoord2  10708  ser3mono  10709  seq3split  10710  seqsplitg  10711  seq3caopr3  10713  seq3caopr2  10715  seqcaopr2g  10716  iseqf1olemjpcl  10730  iseqf1olemqpcl  10731  iseqf1olemfvp  10732  seq3f1olemqsumkj  10733  seq3f1olemqsum  10735  seq3f1oleml  10738  seq3f1o  10739  seqf1og  10743  seq3homo  10749  seq3z  10750  seqhomog  10752  seqfeq4g  10753  seq3distr  10754  ser3ge0  10758  expp1  10768  expcllem  10772  expcl2lemap  10773  m1expcl2  10783  facnn  10949  fac0  10950  fac1  10951  faccl  10957  facdiv  10960  facndiv  10961  bccmpl  10976  bcn2  10986  bccl  10989  fihasheqf1oi  11009  seq3coll  11064  reuccatpfxs1lem  11278  reuccatpfxs1  11279  shftlem  11327  shftf  11341  seq3shft  11349  cjval  11356  cjth  11357  remim  11371  uzin2  11498  caubnd2  11628  negfi  11739  xrmaxltsup  11769  clim  11792  clim2  11794  climshftlemg  11813  climcn1  11819  climcn2  11820  iserex  11850  climub  11855  climserle  11856  climcau  11858  serf0  11863  sumfct  11885  sumrbdclem  11888  fsum3cvg  11889  summodclem3  11891  summodclem2a  11892  zsumdc  11895  fsumgcl  11897  fsum3  11898  fsumf1o  11901  isumss  11902  isumss2  11904  fsum3cvg2  11905  fsum3ser  11908  fsumcl2lem  11909  fsumsplitf  11919  sumpr  11924  sumtp  11925  fsumm1  11927  fsum1p  11929  isummulc2  11937  fsum2dlemstep  11945  fisumcom2  11949  fsumshftm  11956  fisum0diag2  11958  fsummulc2  11959  fsumge1  11972  fsum00  11973  fsumabs  11976  telfsumo  11977  telfsumo2  11978  fsumparts  11981  fsumrelem  11982  fsumiun  11988  binomlem  11994  isumshft  12001  isum1p  12003  isumrpcl  12005  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  cvgratnnlemseq  12037  cvgratnnlemabsle  12038  cvgratnnlemfm  12040  cvgratnnlemrate  12041  cvgratnn  12042  cvgratz  12043  mertenslem2  12047  mertensabs  12048  clim2prod  12050  prodfap0  12056  prodfrecap  12057  prodfdivap  12058  prodrbdclem  12082  fproddccvg  12083  prodmodclem3  12086  prodmodclem2a  12087  zproddc  12090  fprodseq  12094  prodfct  12098  fprodf1o  12099  prodssdc  12100  fprodssdc  12101  fprodmul  12102  fprodm1  12109  fprod1p  12110  fprodm1s  12112  fprodp1s  12113  fprodcl2lem  12116  fprodabs  12127  fprod2dlemstep  12133  fprodcnv  12136  fprodcom2fi  12137  fprodrec  12140  fproddivapf  12142  fprodsplitf  12143  fprodsplit1f  12145  fprodle  12151  zeo3  12379  mulsucdiv2z  12396  zob  12402  nn0o1gt2  12416  nno  12417  nn0o  12418  uzwodc  12558  qnumdencl  12709  pcqcl  12829  pcxnn0cl  12833  pcxcl  12834  pcgcd1  12851  dvdsprmpweqle  12860  pcmpt  12866  pcmpt2  12867  pcmptdvds  12868  infpnlem2  12883  1arith  12890  elgz  12894  mul4sq  12917  4sqlem13m  12926  4sqlem17  12930  4sqlem18  12931  4sqlem19  12932  znnen  12969  ennnfonelemj0  12972  ennnfonelemg  12974  ennnfonelemom  12979  ctinfom  12999  ctiunctlemu1st  13005  ctiunctlemu2nd  13006  ctiunctlemudc  13008  ctiunctlemfo  13010  ssnnctlemct  13017  infpn2  13027  isstruct2im  13042  isstruct2r  13043  imasaddfnlemg  13347  ercpbl  13364  xpsfrnel2  13379  mgmsscl  13394  mgm1  13403  sgrppropd  13446  mndpropd  13473  issubm  13505  0subm  13517  insubm  13518  mhmima  13524  mulgsubcl  13673  issubg  13710  subgex  13713  issubg2m  13726  issubg4m  13730  0subg  13736  isnsg  13739  isnsg2  13740  nsgbi  13741  isnsg3  13744  elnmz  13745  nmzbi  13746  nmzsubg  13747  nmznsg  13750  releqgg  13757  eqgex  13758  eqgval  13760  eqgid  13763  ghmrn  13794  ghmnsgima  13805  eqgabl  13867  ablnsg  13871  gsumfzmhm2  13881  isrng  13897  issrg  13928  srgfcl  13936  isring  13963  iscrng  13966  dvdsrd  14058  unitsubm  14083  isrim0  14125  issubrng  14163  subrngringnsg  14169  issubrng2  14174  opprsubrngg  14175  issubrg  14185  subrgsubm  14198  subrgugrp  14204  issubrg2  14205  issubrg3  14211  subrgpropd  14217  aprval  14246  aprsym  14248  islmod  14255  lmodlema  14256  islmodd  14257  lmodprop2d  14312  rmodislmodlem  14314  rmodislmod  14315  lsssetm  14320  islssmd  14323  lssclg  14328  lsslss  14345  lsspropdg  14395  islidlm  14443  rnglidlmcl  14444  isridlrng  14446  rnglidlmmgm  14460  isridl  14468  gsumfzfsumlemm  14551  psrbag  14633  psr1clfi  14652  uniopn  14675  inopn  14677  fiinopn  14678  iscld  14777  iuncld  14789  tgrest  14843  iscn  14871  cnpval  14872  iscnp  14873  tgcn  14882  ssidcn  14884  lmbrf  14889  cnpnei  14893  cnima  14894  cnconst2  14907  cnrest2  14910  cnptopresti  14912  cnptoprest  14913  lmres  14922  lmtopcnp  14924  txbasval  14941  tx1cn  14943  tx2cn  14944  txcnp  14945  txcnmpt  14947  txdis1cn  14952  txlm  14953  cnmpt11  14957  cnmpt12  14961  cnmpt21  14965  cnmpt22  14968  ishmeo  14978  hmeoopn  14985  hmeocld  14986  qtopbasss  15195  fsumcncntop  15241  expcn  15243  expcncf  15283  ivthinclemlopn  15310  ivthinclemlr  15311  ivthinclemuopn  15312  ivthinclemur  15313  ivthinclemdisj  15314  ivthinclemloc  15315  ivthinc  15317  ivthdec  15318  limccl  15333  ellimc3apf  15334  cnmptlimc  15348  limccoap  15352  dvmptfsum  15399  plycolemc  15432  plycj  15435  2irrexpq  15650  2irrexpqap  15652  fsumdvdsmul  15665  perfect  15675  lgsval  15683  lgsval2lem  15689  lgsdir2lem4  15710  lgsdir2  15712  m1lgs  15764  2lgs  15783  mul2sq  15795  2sqlem6  15799  wlkcprim  16061  bdinex1g  16264  bj-intexr  16271  bj-prexg  16274  bj-uniex  16280  bj-uniexg  16281  bdunexb  16283  bj-indsuc  16291  exmidsbthrlem  16390  qdencn  16395  iswomni0  16419