Theorem eleq1d 2276

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 2270	. 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 1373   e. wcel 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  eleq12d  2278  eqeltrd  2284  eqneltrd  2303  eqneltrrd  2304  rspcimdv  2885  rspcimedv  2886  reuind  2985  sbcel2g  3122  sbccsb2g  3131  breq1  4062  breq2  4063  inex1g  4196  intexr  4210  pwexg  4240  prexg  4271  opelopabsb  4324  pofun  4377  seex  4400  uniex  4502  uniexg  4504  unexb  4507  abnexg  4511  reusv3  4525  rabxfrd  4534  onun2  4556  onsucelsucexmid  4596  ordsucunielexmid  4597  dcextest  4647  tfisi  4653  peano2  4661  seinxp  4764  opabid2  4827  opeliunxp2  4836  elrn2g  4886  opeldm  4900  opeldmg  4902  elreldm  4923  elrn2  4939  opelresg  4985  elsnres  5015  iss  5024  elimasng  5069  issref  5084  rnxpid  5136  unielrel  5229  dffun5r  5302  funopg  5324  brprcneu  5592  tz6.12f  5628  fvelrnb  5649  ssimaex  5663  dmfco  5670  fvmpt3  5681  mptfvex  5688  fvmptf  5695  respreima  5731  fvelrn  5734  ffnfvf  5762  ffvresb  5766  fmptco  5769  fmptcof  5770  fsn  5775  fressnfv  5794  fnex  5829  funfvima  5839  funfvima3  5841  f1mpt  5863  fliftfuns  5890  isoselem  5912  ovrspc2v  5993  ffnov  6072  fovcld  6073  ovmpos  6092  ov2gf  6093  ovg  6108  funimassov  6119  caovclg  6122  elovmpo  6168  off  6194  caofdig  6215  fnexALT  6219  focdmex  6223  f1stres  6268  f2ndres  6269  xp1st  6274  xp2nd  6275  elxp6  6278  oprssdmm  6280  unielxp  6283  fmpox  6309  mpofvex  6314  opeliunxp2f  6347  dftpos4  6372  smoel  6409  tfrlem3-2d  6421  tfrlem8  6427  tfrlem9  6428  tfrlemibxssdm  6436  tfrlemi1  6441  tfrexlem  6443  tfr1onlemsucfn  6449  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfr1onlemaccex  6457  tfr1onlemres  6458  tfri1dALT  6460  tfrcllemsucfn  6462  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllembfn  6466  tfrcllemaccex  6470  tfrcllemres  6471  tfrcl  6473  rdgtfr  6483  rdgon  6495  frecabex  6507  frecabcl  6508  frecfcllem  6513  frecsuclem  6515  nnacl  6589  nnmcl  6590  nnmordi  6625  nnaordex  6637  nnm00  6639  erexb  6668  qliftfuns  6729  ixpsnval  6811  elixp2  6812  resixp  6843  mptelixpg  6844  elixpsn  6845  fundmen  6922  fopwdom  6958  xpf1o  6966  dif1en  7002  diffitest  7010  diffifi  7017  inffiexmid  7029  unfiexmid  7041  unfidisj  7045  prfidceq  7051  fiintim  7054  xpfi  7055  ssfirab  7059  fnfi  7064  iunfidisj  7074  snexxph  7078  fidcenumlemr  7083  elfi2  7100  ctssdccl  7239  isnumi  7315  cc2lem  7413  cc3  7415  addnidpig  7484  indpi  7490  dfplpq2  7502  addclnq  7523  mulclnq  7524  nnnq0lem1  7594  addclnq0  7599  mulclnq0  7600  nqpnq0nq  7601  distrnq0  7607  prloc  7639  prarloclemlo  7642  prarloclem3  7645  prarloclem5  7648  genpml  7665  genpmu  7666  addnqprl  7677  addnqpru  7678  mulnqprl  7716  mulnqpru  7717  ltexprlemell  7746  ltexprlemelu  7747  ltexprlemdisj  7754  ltexprlemloc  7755  ltexprlemrl  7758  ltexprlemru  7760  ltexpri  7761  recexprlemm  7772  recexprlemdisj  7778  recexprlemloc  7779  recexprlem1ssl  7781  recexprlem1ssu  7782  recexpr  7786  addclsr  7901  mulclsr  7902  suplocsrlemb  7954  suplocsrlempr  7955  suplocsrlem  7956  suplocsr  7957  pitonn  7996  peano2nnnn  8001  axaddrcl  8013  axmulrcl  8015  peano5nnnn  8040  axpre-suploclemres  8049  negreb  8372  negf1o  8489  eqord1  8591  eqord2  8592  cju  9069  peano2nn  9083  nn1m1nn  9089  nnaddcl  9091  nnmulcl  9092  nnsub  9110  nndivtr  9113  un0addcl  9363  un0mulcl  9364  elnnnn0  9373  elz  9409  nnnegz  9410  znegclb  9440  zaddcllempos  9444  zaddcllemneg  9446  zaddcl  9447  nzadd  9460  zmulcl  9461  elz2  9479  zneo  9509  nneoor  9510  zeo  9513  peano5uzti  9516  zindd  9526  uzp1  9717  uzaddcl  9742  supinfneg  9751  infsupneg  9752  supminfex  9753  ublbneg  9769  eqreznegel  9770  negm  9771  qmulz  9779  qnegcl  9792  irradd  9802  irrmul  9803  fzrev2  10242  infssuzex  10413  infssuzcldc  10415  zsupssdc  10418  negqmod0  10513  frec2uzuzd  10584  frecuzrdgrrn  10590  frec2uzrdg  10591  frecuzrdgrcl  10592  frecuzrdgsuc  10596  frecuzrdgrclt  10597  frecuzrdgg  10598  frecuzrdgsuctlem  10605  xnn0nnen  10619  iseqovex  10640  seq3val  10642  seqvalcd  10643  seq3-1  10644  seqf  10646  seq3p1  10647  seqovcd  10649  seqp1cd  10652  seq3clss  10653  monoord  10667  monoord2  10668  ser3mono  10669  seq3split  10670  seqsplitg  10671  seq3caopr3  10673  seq3caopr2  10675  seqcaopr2g  10676  iseqf1olemjpcl  10690  iseqf1olemqpcl  10691  iseqf1olemfvp  10692  seq3f1olemqsumkj  10693  seq3f1olemqsum  10695  seq3f1oleml  10698  seq3f1o  10699  seqf1og  10703  seq3homo  10709  seq3z  10710  seqhomog  10712  seqfeq4g  10713  seq3distr  10714  ser3ge0  10718  expp1  10728  expcllem  10732  expcl2lemap  10733  m1expcl2  10743  facnn  10909  fac0  10910  fac1  10911  faccl  10917  facdiv  10920  facndiv  10921  bccmpl  10936  bcn2  10946  bccl  10949  fihasheqf1oi  10969  seq3coll  11024  reuccatpfxs1lem  11237  reuccatpfxs1  11238  shftlem  11242  shftf  11256  seq3shft  11264  cjval  11271  cjth  11272  remim  11286  uzin2  11413  caubnd2  11543  negfi  11654  xrmaxltsup  11684  clim  11707  clim2  11709  climshftlemg  11728  climcn1  11734  climcn2  11735  iserex  11765  climub  11770  climserle  11771  climcau  11773  serf0  11778  sumfct  11800  sumrbdclem  11803  fsum3cvg  11804  summodclem3  11806  summodclem2a  11807  zsumdc  11810  fsumgcl  11812  fsum3  11813  fsumf1o  11816  isumss  11817  isumss2  11819  fsum3cvg2  11820  fsum3ser  11823  fsumcl2lem  11824  fsumsplitf  11834  sumpr  11839  sumtp  11840  fsumm1  11842  fsum1p  11844  isummulc2  11852  fsum2dlemstep  11860  fisumcom2  11864  fsumshftm  11871  fisum0diag2  11873  fsummulc2  11874  fsumge1  11887  fsum00  11888  fsumabs  11891  telfsumo  11892  telfsumo2  11893  fsumparts  11896  fsumrelem  11897  fsumiun  11903  binomlem  11909  isumshft  11916  isum1p  11918  isumrpcl  11920  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  cvgratnnlemseq  11952  cvgratnnlemabsle  11953  cvgratnnlemfm  11955  cvgratnnlemrate  11956  cvgratnn  11957  cvgratz  11958  mertenslem2  11962  mertensabs  11963  clim2prod  11965  prodfap0  11971  prodfrecap  11972  prodfdivap  11973  prodrbdclem  11997  fproddccvg  11998  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  fprodseq  12009  prodfct  12013  fprodf1o  12014  prodssdc  12015  fprodssdc  12016  fprodmul  12017  fprodm1  12024  fprod1p  12025  fprodm1s  12027  fprodp1s  12028  fprodcl2lem  12031  fprodabs  12042  fprod2dlemstep  12048  fprodcnv  12051  fprodcom2fi  12052  fprodrec  12055  fproddivapf  12057  fprodsplitf  12058  fprodsplit1f  12060  fprodle  12066  zeo3  12294  mulsucdiv2z  12311  zob  12317  nn0o1gt2  12331  nno  12332  nn0o  12333  uzwodc  12473  qnumdencl  12624  pcqcl  12744  pcxnn0cl  12748  pcxcl  12749  pcgcd1  12766  dvdsprmpweqle  12775  pcmpt  12781  pcmpt2  12782  pcmptdvds  12783  infpnlem2  12798  1arith  12805  elgz  12809  mul4sq  12832  4sqlem13m  12841  4sqlem17  12845  4sqlem18  12846  4sqlem19  12847  znnen  12884  ennnfonelemj0  12887  ennnfonelemg  12889  ennnfonelemom  12894  ctinfom  12914  ctiunctlemu1st  12920  ctiunctlemu2nd  12921  ctiunctlemudc  12923  ctiunctlemfo  12925  ssnnctlemct  12932  infpn2  12942  isstruct2im  12957  isstruct2r  12958  imasaddfnlemg  13261  ercpbl  13278  xpsfrnel2  13293  mgmsscl  13308  mgm1  13317  sgrppropd  13360  mndpropd  13387  issubm  13419  0subm  13431  insubm  13432  mhmima  13438  mulgsubcl  13587  issubg  13624  subgex  13627  issubg2m  13640  issubg4m  13644  0subg  13650  isnsg  13653  isnsg2  13654  nsgbi  13655  isnsg3  13658  elnmz  13659  nmzbi  13660  nmzsubg  13661  nmznsg  13664  releqgg  13671  eqgex  13672  eqgval  13674  eqgid  13677  ghmrn  13708  ghmnsgima  13719  eqgabl  13781  ablnsg  13785  gsumfzmhm2  13795  isrng  13811  issrg  13842  srgfcl  13850  isring  13877  iscrng  13880  dvdsrd  13971  unitsubm  13996  isrim0  14038  issubrng  14076  subrngringnsg  14082  issubrng2  14087  opprsubrngg  14088  issubrg  14098  subrgsubm  14111  subrgugrp  14117  issubrg2  14118  issubrg3  14124  subrgpropd  14130  aprval  14159  aprsym  14161  islmod  14168  lmodlema  14169  islmodd  14170  lmodprop2d  14225  rmodislmodlem  14227  rmodislmod  14228  lsssetm  14233  islssmd  14236  lssclg  14241  lsslss  14258  lsspropdg  14308  islidlm  14356  rnglidlmcl  14357  isridlrng  14359  rnglidlmmgm  14373  isridl  14381  gsumfzfsumlemm  14464  psrbag  14546  psr1clfi  14565  uniopn  14588  inopn  14590  fiinopn  14591  iscld  14690  iuncld  14702  tgrest  14756  iscn  14784  cnpval  14785  iscnp  14786  tgcn  14795  ssidcn  14797  lmbrf  14802  cnpnei  14806  cnima  14807  cnconst2  14820  cnrest2  14823  cnptopresti  14825  cnptoprest  14826  lmres  14835  lmtopcnp  14837  txbasval  14854  tx1cn  14856  tx2cn  14857  txcnp  14858  txcnmpt  14860  txdis1cn  14865  txlm  14866  cnmpt11  14870  cnmpt12  14874  cnmpt21  14878  cnmpt22  14881  ishmeo  14891  hmeoopn  14898  hmeocld  14899  qtopbasss  15108  fsumcncntop  15154  expcn  15156  expcncf  15196  ivthinclemlopn  15223  ivthinclemlr  15224  ivthinclemuopn  15225  ivthinclemur  15226  ivthinclemdisj  15227  ivthinclemloc  15228  ivthinc  15230  ivthdec  15231  limccl  15246  ellimc3apf  15247  cnmptlimc  15261  limccoap  15265  dvmptfsum  15312  plycolemc  15345  plycj  15348  2irrexpq  15563  2irrexpqap  15565  fsumdvdsmul  15578  perfect  15588  lgsval  15596  lgsval2lem  15602  lgsdir2lem4  15623  lgsdir2  15625  m1lgs  15677  2lgs  15696  mul2sq  15708  2sqlem6  15712  bdinex1g  16036  bj-intexr  16043  bj-prexg  16046  bj-uniex  16052  bj-uniexg  16053  bdunexb  16055  bj-indsuc  16063  exmidsbthrlem  16163  qdencn  16168  iswomni0  16192