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  4235  pwexg  4265  prexg  4296  opelopabsb  4349  pofun  4404  seex  4427  uniex  4529  uniexg  4531  unexb  4534  abnexg  4538  reusv3  4552  rabxfrd  4561  onun2  4583  onsucelsucexmid  4623  ordsucunielexmid  4624  dcextest  4674  tfisi  4680  peano2  4688  seinxp  4792  opabid2  4856  opeliunxp2  4865  elrn2g  4915  opeldm  4929  opeldmg  4931  elreldm  4953  elrn2  4969  opelresg  5015  elsnres  5045  iss  5054  elimasng  5099  issref  5114  rnxpid  5166  unielrel  5259  dffun5r  5333  funopg  5355  brprcneu  5625  tz6.12f  5661  fvelrnb  5686  ssimaex  5700  dmfco  5707  fvmpt3  5718  mptfvex  5725  fvmptf  5732  respreima  5768  fvelrn  5771  ffnfvf  5799  ffvresb  5803  fmptco  5806  fmptcof  5807  fsn  5812  fressnfv  5833  fnex  5868  funfvima  5878  funfvima3  5880  f1mpt  5904  fliftfuns  5931  isoselem  5953  ovrspc2v  6036  ffnov  6117  fovcld  6118  ovmpos  6137  ov2gf  6138  ovg  6153  funimassov  6164  caovclg  6167  elovmpo  6213  off  6240  caofdig  6261  fnexALT  6265  focdmex  6269  f1stres  6314  f2ndres  6315  xp1st  6320  xp2nd  6321  elxp6  6324  oprssdmm  6326  unielxp  6329  fmpox  6357  mpofvex  6362  opeliunxp2f  6395  dftpos4  6420  smoel  6457  tfrlem3-2d  6469  tfrlem8  6475  tfrlem9  6476  tfrlemibxssdm  6484  tfrlemi1  6489  tfrexlem  6491  tfr1onlemsucfn  6497  tfr1onlemsucaccv  6498  tfr1onlembxssdm  6500  tfr1onlembfn  6501  tfr1onlemaccex  6505  tfr1onlemres  6506  tfri1dALT  6508  tfrcllemsucfn  6510  tfrcllemsucaccv  6511  tfrcllembxssdm  6513  tfrcllembfn  6514  tfrcllemaccex  6518  tfrcllemres  6519  tfrcl  6521  rdgtfr  6531  rdgon  6543  frecabex  6555  frecabcl  6556  frecfcllem  6561  frecsuclem  6563  nnacl  6639  nnmcl  6640  nnmordi  6675  nnaordex  6687  nnm00  6689  erexb  6718  qliftfuns  6779  ixpsnval  6861  elixp2  6862  resixp  6893  mptelixpg  6894  elixpsn  6895  fundmen  6972  fopwdom  7010  xpf1o  7018  dif1en  7054  diffitest  7062  diffifi  7069  inffiexmid  7084  unfiexmid  7096  unfidisj  7100  prfidceq  7106  fiintim  7109  xpfi  7110  ssfirab  7114  fnfi  7119  iunfidisj  7129  snexxph  7133  fidcenumlemr  7138  elfi2  7155  ctssdccl  7294  isnumi  7370  cc2lem  7468  cc3  7470  addnidpig  7539  indpi  7545  dfplpq2  7557  addclnq  7578  mulclnq  7579  nnnq0lem1  7649  addclnq0  7654  mulclnq0  7655  nqpnq0nq  7656  distrnq0  7662  prloc  7694  prarloclemlo  7697  prarloclem3  7700  prarloclem5  7703  genpml  7720  genpmu  7721  addnqprl  7732  addnqpru  7733  mulnqprl  7771  mulnqpru  7772  ltexprlemell  7801  ltexprlemelu  7802  ltexprlemdisj  7809  ltexprlemloc  7810  ltexprlemrl  7813  ltexprlemru  7815  ltexpri  7816  recexprlemm  7827  recexprlemdisj  7833  recexprlemloc  7834  recexprlem1ssl  7836  recexprlem1ssu  7837  recexpr  7841  addclsr  7956  mulclsr  7957  suplocsrlemb  8009  suplocsrlempr  8010  suplocsrlem  8011  suplocsr  8012  pitonn  8051  peano2nnnn  8056  axaddrcl  8068  axmulrcl  8070  peano5nnnn  8095  axpre-suploclemres  8104  negreb  8427  negf1o  8544  eqord1  8646  eqord2  8647  cju  9124  peano2nn  9138  nn1m1nn  9144  nnaddcl  9146  nnmulcl  9147  nnsub  9165  nndivtr  9168  un0addcl  9418  un0mulcl  9419  elnnnn0  9428  elz  9464  nnnegz  9465  znegclb  9495  zaddcllempos  9499  zaddcllemneg  9501  zaddcl  9502  nzadd  9515  zmulcl  9516  elz2  9534  zneo  9564  nneoor  9565  zeo  9568  peano5uzti  9571  zindd  9581  uzp1  9773  uzaddcl  9798  supinfneg  9807  infsupneg  9808  supminfex  9809  ublbneg  9825  eqreznegel  9826  negm  9827  qmulz  9835  qnegcl  9848  irradd  9858  irrmul  9859  fzrev2  10298  infssuzex  10470  infssuzcldc  10472  zsupssdc  10475  negqmod0  10570  frec2uzuzd  10641  frecuzrdgrrn  10647  frec2uzrdg  10648  frecuzrdgrcl  10649  frecuzrdgsuc  10653  frecuzrdgrclt  10654  frecuzrdgg  10655  frecuzrdgsuctlem  10662  xnn0nnen  10676  iseqovex  10697  seq3val  10699  seqvalcd  10700  seq3-1  10701  seqf  10703  seq3p1  10704  seqovcd  10706  seqp1cd  10709  seq3clss  10710  monoord  10724  monoord2  10725  ser3mono  10726  seq3split  10727  seqsplitg  10728  seq3caopr3  10730  seq3caopr2  10732  seqcaopr2g  10733  iseqf1olemjpcl  10747  iseqf1olemqpcl  10748  iseqf1olemfvp  10749  seq3f1olemqsumkj  10750  seq3f1olemqsum  10752  seq3f1oleml  10755  seq3f1o  10756  seqf1og  10760  seq3homo  10766  seq3z  10767  seqhomog  10769  seqfeq4g  10770  seq3distr  10771  ser3ge0  10775  expp1  10785  expcllem  10789  expcl2lemap  10790  m1expcl2  10800  facnn  10966  fac0  10967  fac1  10968  faccl  10974  facdiv  10977  facndiv  10978  bccmpl  10993  bcn2  11003  bccl  11006  fihasheqf1oi  11026  seq3coll  11082  ccatalpha  11166  reuccatpfxs1lem  11299  reuccatpfxs1  11300  shftlem  11348  shftf  11362  seq3shft  11370  cjval  11377  cjth  11378  remim  11392  uzin2  11519  caubnd2  11649  negfi  11760  xrmaxltsup  11790  clim  11813  clim2  11815  climshftlemg  11834  climcn1  11840  climcn2  11841  iserex  11871  climub  11876  climserle  11877  climcau  11879  serf0  11884  sumfct  11906  sumrbdclem  11909  fsum3cvg  11910  summodclem3  11912  summodclem2a  11913  zsumdc  11916  fsumgcl  11918  fsum3  11919  fsumf1o  11922  isumss  11923  isumss2  11925  fsum3cvg2  11926  fsum3ser  11929  fsumcl2lem  11930  fsumsplitf  11940  sumpr  11945  sumtp  11946  fsumm1  11948  fsum1p  11950  isummulc2  11958  fsum2dlemstep  11966  fisumcom2  11970  fsumshftm  11977  fisum0diag2  11979  fsummulc2  11980  fsumge1  11993  fsum00  11994  fsumabs  11997  telfsumo  11998  telfsumo2  11999  fsumparts  12002  fsumrelem  12003  fsumiun  12009  binomlem  12015  isumshft  12022  isum1p  12024  isumrpcl  12026  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  cvgratnnlemseq  12058  cvgratnnlemabsle  12059  cvgratnnlemfm  12061  cvgratnnlemrate  12062  cvgratnn  12063  cvgratz  12064  mertenslem2  12068  mertensabs  12069  clim2prod  12071  prodfap0  12077  prodfrecap  12078  prodfdivap  12079  prodrbdclem  12103  fproddccvg  12104  prodmodclem3  12107  prodmodclem2a  12108  zproddc  12111  fprodseq  12115  prodfct  12119  fprodf1o  12120  prodssdc  12121  fprodssdc  12122  fprodmul  12123  fprodm1  12130  fprod1p  12131  fprodm1s  12133  fprodp1s  12134  fprodcl2lem  12137  fprodabs  12148  fprod2dlemstep  12154  fprodcnv  12157  fprodcom2fi  12158  fprodrec  12161  fproddivapf  12163  fprodsplitf  12164  fprodsplit1f  12166  fprodle  12172  zeo3  12400  mulsucdiv2z  12417  zob  12423  nn0o1gt2  12437  nno  12438  nn0o  12439  uzwodc  12579  qnumdencl  12730  pcqcl  12850  pcxnn0cl  12854  pcxcl  12855  pcgcd1  12872  dvdsprmpweqle  12881  pcmpt  12887  pcmpt2  12888  pcmptdvds  12889  infpnlem2  12904  1arith  12911  elgz  12915  mul4sq  12938  4sqlem13m  12947  4sqlem17  12951  4sqlem18  12952  4sqlem19  12953  znnen  12990  ennnfonelemj0  12993  ennnfonelemg  12995  ennnfonelemom  13000  ctinfom  13020  ctiunctlemu1st  13026  ctiunctlemu2nd  13027  ctiunctlemudc  13029  ctiunctlemfo  13031  ssnnctlemct  13038  infpn2  13048  isstruct2im  13063  isstruct2r  13064  imasaddfnlemg  13368  ercpbl  13385  xpsfrnel2  13400  mgmsscl  13415  mgm1  13424  sgrppropd  13467  mndpropd  13494  issubm  13526  0subm  13538  insubm  13539  mhmima  13545  mulgsubcl  13694  issubg  13731  subgex  13734  issubg2m  13747  issubg4m  13751  0subg  13757  isnsg  13760  isnsg2  13761  nsgbi  13762  isnsg3  13765  elnmz  13766  nmzbi  13767  nmzsubg  13768  nmznsg  13771  releqgg  13778  eqgex  13779  eqgval  13781  eqgid  13784  ghmrn  13815  ghmnsgima  13826  eqgabl  13888  ablnsg  13892  gsumfzmhm2  13902  isrng  13918  issrg  13949  srgfcl  13957  isring  13984  iscrng  13987  dvdsrd  14079  unitsubm  14104  isrim0  14146  issubrng  14184  subrngringnsg  14190  issubrng2  14195  opprsubrngg  14196  issubrg  14206  subrgsubm  14219  subrgugrp  14225  issubrg2  14226  issubrg3  14232  subrgpropd  14238  aprval  14267  aprsym  14269  islmod  14276  lmodlema  14277  islmodd  14278  lmodprop2d  14333  rmodislmodlem  14335  rmodislmod  14336  lsssetm  14341  islssmd  14344  lssclg  14349  lsslss  14366  lsspropdg  14416  islidlm  14464  rnglidlmcl  14465  isridlrng  14467  rnglidlmmgm  14481  isridl  14489  gsumfzfsumlemm  14572  psrbag  14654  psr1clfi  14673  uniopn  14696  inopn  14698  fiinopn  14699  iscld  14798  iuncld  14810  tgrest  14864  iscn  14892  cnpval  14893  iscnp  14894  tgcn  14903  ssidcn  14905  lmbrf  14910  cnpnei  14914  cnima  14915  cnconst2  14928  cnrest2  14931  cnptopresti  14933  cnptoprest  14934  lmres  14943  lmtopcnp  14945  txbasval  14962  tx1cn  14964  tx2cn  14965  txcnp  14966  txcnmpt  14968  txdis1cn  14973  txlm  14974  cnmpt11  14978  cnmpt12  14982  cnmpt21  14986  cnmpt22  14989  ishmeo  14999  hmeoopn  15006  hmeocld  15007  qtopbasss  15216  fsumcncntop  15262  expcn  15264  expcncf  15304  ivthinclemlopn  15331  ivthinclemlr  15332  ivthinclemuopn  15333  ivthinclemur  15334  ivthinclemdisj  15335  ivthinclemloc  15336  ivthinc  15338  ivthdec  15339  limccl  15354  ellimc3apf  15355  cnmptlimc  15369  limccoap  15373  dvmptfsum  15420  plycolemc  15453  plycj  15456  2irrexpq  15671  2irrexpqap  15673  fsumdvdsmul  15686  perfect  15696  lgsval  15704  lgsval2lem  15710  lgsdir2lem4  15731  lgsdir2  15733  m1lgs  15785  2lgs  15804  mul2sq  15816  2sqlem6  15820  wlkcprim  16122  isclwwlk  16163  clwwlk1loop  16168  clwwlkccatlem  16169  clwwlkn1  16186  loopclwwlkn1b  16187  clwwlkn1loopb  16188  clwwlkn2  16189  clwwlkext2edg  16190  umgr2cwwk2dif  16192  bdinex1g  16373  bj-intexr  16380  bj-prexg  16383  bj-uniex  16389  bj-uniexg  16390  bdunexb  16392  bj-indsuc  16400  exmidsbthrlem  16504  qdencn  16509  iswomni0  16533