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  5622  tz6.12f  5658  fvelrnb  5683  ssimaex  5697  dmfco  5704  fvmpt3  5715  mptfvex  5722  fvmptf  5729  respreima  5765  fvelrn  5768  ffnfvf  5796  ffvresb  5800  fmptco  5803  fmptcof  5804  fsn  5809  fressnfv  5830  fnex  5865  funfvima  5875  funfvima3  5877  f1mpt  5901  fliftfuns  5928  isoselem  5950  ovrspc2v  6033  ffnov  6114  fovcld  6115  ovmpos  6134  ov2gf  6135  ovg  6150  funimassov  6161  caovclg  6164  elovmpo  6210  off  6237  caofdig  6258  fnexALT  6262  focdmex  6266  f1stres  6311  f2ndres  6312  xp1st  6317  xp2nd  6318  elxp6  6321  oprssdmm  6323  unielxp  6326  fmpox  6352  mpofvex  6357  opeliunxp2f  6390  dftpos4  6415  smoel  6452  tfrlem3-2d  6464  tfrlem8  6470  tfrlem9  6471  tfrlemibxssdm  6479  tfrlemi1  6484  tfrexlem  6486  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemaccex  6500  tfr1onlemres  6501  tfri1dALT  6503  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemaccex  6513  tfrcllemres  6514  tfrcl  6516  rdgtfr  6526  rdgon  6538  frecabex  6550  frecabcl  6551  frecfcllem  6556  frecsuclem  6558  nnacl  6634  nnmcl  6635  nnmordi  6670  nnaordex  6682  nnm00  6684  erexb  6713  qliftfuns  6774  ixpsnval  6856  elixp2  6857  resixp  6888  mptelixpg  6889  elixpsn  6890  fundmen  6967  fopwdom  7005  xpf1o  7013  dif1en  7049  diffitest  7057  diffifi  7064  inffiexmid  7079  unfiexmid  7091  unfidisj  7095  prfidceq  7101  fiintim  7104  xpfi  7105  ssfirab  7109  fnfi  7114  iunfidisj  7124  snexxph  7128  fidcenumlemr  7133  elfi2  7150  ctssdccl  7289  isnumi  7365  cc2lem  7463  cc3  7465  addnidpig  7534  indpi  7540  dfplpq2  7552  addclnq  7573  mulclnq  7574  nnnq0lem1  7644  addclnq0  7649  mulclnq0  7650  nqpnq0nq  7651  distrnq0  7657  prloc  7689  prarloclemlo  7692  prarloclem3  7695  prarloclem5  7698  genpml  7715  genpmu  7716  addnqprl  7727  addnqpru  7728  mulnqprl  7766  mulnqpru  7767  ltexprlemell  7796  ltexprlemelu  7797  ltexprlemdisj  7804  ltexprlemloc  7805  ltexprlemrl  7808  ltexprlemru  7810  ltexpri  7811  recexprlemm  7822  recexprlemdisj  7828  recexprlemloc  7829  recexprlem1ssl  7831  recexprlem1ssu  7832  recexpr  7836  addclsr  7951  mulclsr  7952  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  suplocsr  8007  pitonn  8046  peano2nnnn  8051  axaddrcl  8063  axmulrcl  8065  peano5nnnn  8090  axpre-suploclemres  8099  negreb  8422  negf1o  8539  eqord1  8641  eqord2  8642  cju  9119  peano2nn  9133  nn1m1nn  9139  nnaddcl  9141  nnmulcl  9142  nnsub  9160  nndivtr  9163  un0addcl  9413  un0mulcl  9414  elnnnn0  9423  elz  9459  nnnegz  9460  znegclb  9490  zaddcllempos  9494  zaddcllemneg  9496  zaddcl  9497  nzadd  9510  zmulcl  9511  elz2  9529  zneo  9559  nneoor  9560  zeo  9563  peano5uzti  9566  zindd  9576  uzp1  9768  uzaddcl  9793  supinfneg  9802  infsupneg  9803  supminfex  9804  ublbneg  9820  eqreznegel  9821  negm  9822  qmulz  9830  qnegcl  9843  irradd  9853  irrmul  9854  fzrev2  10293  infssuzex  10465  infssuzcldc  10467  zsupssdc  10470  negqmod0  10565  frec2uzuzd  10636  frecuzrdgrrn  10642  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgsuc  10648  frecuzrdgrclt  10649  frecuzrdgg  10650  frecuzrdgsuctlem  10657  xnn0nnen  10671  iseqovex  10692  seq3val  10694  seqvalcd  10695  seq3-1  10696  seqf  10698  seq3p1  10699  seqovcd  10701  seqp1cd  10704  seq3clss  10705  monoord  10719  monoord2  10720  ser3mono  10721  seq3split  10722  seqsplitg  10723  seq3caopr3  10725  seq3caopr2  10727  seqcaopr2g  10728  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsumkj  10745  seq3f1olemqsum  10747  seq3f1oleml  10750  seq3f1o  10751  seqf1og  10755  seq3homo  10761  seq3z  10762  seqhomog  10764  seqfeq4g  10765  seq3distr  10766  ser3ge0  10770  expp1  10780  expcllem  10784  expcl2lemap  10785  m1expcl2  10795  facnn  10961  fac0  10962  fac1  10963  faccl  10969  facdiv  10972  facndiv  10973  bccmpl  10988  bcn2  10998  bccl  11001  fihasheqf1oi  11021  seq3coll  11077  ccatalpha  11161  reuccatpfxs1lem  11294  reuccatpfxs1  11295  shftlem  11343  shftf  11357  seq3shft  11365  cjval  11372  cjth  11373  remim  11387  uzin2  11514  caubnd2  11644  negfi  11755  xrmaxltsup  11785  clim  11808  clim2  11810  climshftlemg  11829  climcn1  11835  climcn2  11836  iserex  11866  climub  11871  climserle  11872  climcau  11874  serf0  11879  sumfct  11901  sumrbdclem  11904  fsum3cvg  11905  summodclem3  11907  summodclem2a  11908  zsumdc  11911  fsumgcl  11913  fsum3  11914  fsumf1o  11917  isumss  11918  isumss2  11920  fsum3cvg2  11921  fsum3ser  11924  fsumcl2lem  11925  fsumsplitf  11935  sumpr  11940  sumtp  11941  fsumm1  11943  fsum1p  11945  isummulc2  11953  fsum2dlemstep  11961  fisumcom2  11965  fsumshftm  11972  fisum0diag2  11974  fsummulc2  11975  fsumge1  11988  fsum00  11989  fsumabs  11992  telfsumo  11993  telfsumo2  11994  fsumparts  11997  fsumrelem  11998  fsumiun  12004  binomlem  12010  isumshft  12017  isum1p  12019  isumrpcl  12021  cvgratnnlemnexp  12051  cvgratnnlemmn  12052  cvgratnnlemseq  12053  cvgratnnlemabsle  12054  cvgratnnlemfm  12056  cvgratnnlemrate  12057  cvgratnn  12058  cvgratz  12059  mertenslem2  12063  mertensabs  12064  clim2prod  12066  prodfap0  12072  prodfrecap  12073  prodfdivap  12074  prodrbdclem  12098  fproddccvg  12099  prodmodclem3  12102  prodmodclem2a  12103  zproddc  12106  fprodseq  12110  prodfct  12114  fprodf1o  12115  prodssdc  12116  fprodssdc  12117  fprodmul  12118  fprodm1  12125  fprod1p  12126  fprodm1s  12128  fprodp1s  12129  fprodcl2lem  12132  fprodabs  12143  fprod2dlemstep  12149  fprodcnv  12152  fprodcom2fi  12153  fprodrec  12156  fproddivapf  12158  fprodsplitf  12159  fprodsplit1f  12161  fprodle  12167  zeo3  12395  mulsucdiv2z  12412  zob  12418  nn0o1gt2  12432  nno  12433  nn0o  12434  uzwodc  12574  qnumdencl  12725  pcqcl  12845  pcxnn0cl  12849  pcxcl  12850  pcgcd1  12867  dvdsprmpweqle  12876  pcmpt  12882  pcmpt2  12883  pcmptdvds  12884  infpnlem2  12899  1arith  12906  elgz  12910  mul4sq  12933  4sqlem13m  12942  4sqlem17  12946  4sqlem18  12947  4sqlem19  12948  znnen  12985  ennnfonelemj0  12988  ennnfonelemg  12990  ennnfonelemom  12995  ctinfom  13015  ctiunctlemu1st  13021  ctiunctlemu2nd  13022  ctiunctlemudc  13024  ctiunctlemfo  13026  ssnnctlemct  13033  infpn2  13043  isstruct2im  13058  isstruct2r  13059  imasaddfnlemg  13363  ercpbl  13380  xpsfrnel2  13395  mgmsscl  13410  mgm1  13419  sgrppropd  13462  mndpropd  13489  issubm  13521  0subm  13533  insubm  13534  mhmima  13540  mulgsubcl  13689  issubg  13726  subgex  13729  issubg2m  13742  issubg4m  13746  0subg  13752  isnsg  13755  isnsg2  13756  nsgbi  13757  isnsg3  13760  elnmz  13761  nmzbi  13762  nmzsubg  13763  nmznsg  13766  releqgg  13773  eqgex  13774  eqgval  13776  eqgid  13779  ghmrn  13810  ghmnsgima  13821  eqgabl  13883  ablnsg  13887  gsumfzmhm2  13897  isrng  13913  issrg  13944  srgfcl  13952  isring  13979  iscrng  13982  dvdsrd  14074  unitsubm  14099  isrim0  14141  issubrng  14179  subrngringnsg  14185  issubrng2  14190  opprsubrngg  14191  issubrg  14201  subrgsubm  14214  subrgugrp  14220  issubrg2  14221  issubrg3  14227  subrgpropd  14233  aprval  14262  aprsym  14264  islmod  14271  lmodlema  14272  islmodd  14273  lmodprop2d  14328  rmodislmodlem  14330  rmodislmod  14331  lsssetm  14336  islssmd  14339  lssclg  14344  lsslss  14361  lsspropdg  14411  islidlm  14459  rnglidlmcl  14460  isridlrng  14462  rnglidlmmgm  14476  isridl  14484  gsumfzfsumlemm  14567  psrbag  14649  psr1clfi  14668  uniopn  14691  inopn  14693  fiinopn  14694  iscld  14793  iuncld  14805  tgrest  14859  iscn  14887  cnpval  14888  iscnp  14889  tgcn  14898  ssidcn  14900  lmbrf  14905  cnpnei  14909  cnima  14910  cnconst2  14923  cnrest2  14926  cnptopresti  14928  cnptoprest  14929  lmres  14938  lmtopcnp  14940  txbasval  14957  tx1cn  14959  tx2cn  14960  txcnp  14961  txcnmpt  14963  txdis1cn  14968  txlm  14969  cnmpt11  14973  cnmpt12  14977  cnmpt21  14981  cnmpt22  14984  ishmeo  14994  hmeoopn  15001  hmeocld  15002  qtopbasss  15211  fsumcncntop  15257  expcn  15259  expcncf  15299  ivthinclemlopn  15326  ivthinclemlr  15327  ivthinclemuopn  15328  ivthinclemur  15329  ivthinclemdisj  15330  ivthinclemloc  15331  ivthinc  15333  ivthdec  15334  limccl  15349  ellimc3apf  15350  cnmptlimc  15364  limccoap  15368  dvmptfsum  15415  plycolemc  15448  plycj  15451  2irrexpq  15666  2irrexpqap  15668  fsumdvdsmul  15681  perfect  15691  lgsval  15699  lgsval2lem  15705  lgsdir2lem4  15726  lgsdir2  15728  m1lgs  15780  2lgs  15799  mul2sq  15811  2sqlem6  15815  wlkcprim  16096  isclwwlk  16137  clwwlk1loop  16142  clwwlkccatlem  16143  clwwlkn1  16160  loopclwwlkn1b  16161  clwwlkn1loopb  16162  clwwlkn2  16163  clwwlkext2edg  16164  umgr2cwwk2dif  16166  bdinex1g  16347  bj-intexr  16354  bj-prexg  16357  bj-uniex  16363  bj-uniexg  16364  bdunexb  16366  bj-indsuc  16374  exmidsbthrlem  16478  qdencn  16483  iswomni0  16507