Theorem eleq1d 2274

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 2268	. 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 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eleq12d  2276  eqeltrd  2282  eqneltrd  2301  eqneltrrd  2302  rspcimdv  2878  rspcimedv  2879  reuind  2978  sbcel2g  3114  sbccsb2g  3123  breq1  4047  breq2  4048  inex1g  4180  intexr  4194  pwexg  4224  prexg  4255  opelopabsb  4306  pofun  4359  seex  4382  uniex  4484  uniexg  4486  unexb  4489  abnexg  4493  reusv3  4507  rabxfrd  4516  onun2  4538  onsucelsucexmid  4578  ordsucunielexmid  4579  dcextest  4629  tfisi  4635  peano2  4643  seinxp  4746  opabid2  4809  opeliunxp2  4818  elrn2g  4868  opeldm  4881  opeldmg  4883  elreldm  4904  elrn2  4920  opelresg  4966  elsnres  4996  iss  5005  elimasng  5050  issref  5065  rnxpid  5117  unielrel  5210  dffun5r  5283  funopg  5305  brprcneu  5569  tz6.12f  5605  fvelrnb  5626  ssimaex  5640  dmfco  5647  fvmpt3  5658  mptfvex  5665  fvmptf  5672  respreima  5708  fvelrn  5711  ffnfvf  5739  ffvresb  5743  fmptco  5746  fmptcof  5747  fsn  5752  fressnfv  5771  fnex  5806  funfvima  5816  funfvima3  5818  f1mpt  5840  fliftfuns  5867  isoselem  5889  ovrspc2v  5970  ffnov  6049  fovcld  6050  ovmpos  6069  ov2gf  6070  ovg  6085  funimassov  6096  caovclg  6099  elovmpo  6145  off  6171  caofdig  6192  fnexALT  6196  focdmex  6200  f1stres  6245  f2ndres  6246  xp1st  6251  xp2nd  6252  elxp6  6255  oprssdmm  6257  unielxp  6260  fmpox  6286  mpofvex  6291  opeliunxp2f  6324  dftpos4  6349  smoel  6386  tfrlem3-2d  6398  tfrlem8  6404  tfrlem9  6405  tfrlemibxssdm  6413  tfrlemi1  6418  tfrexlem  6420  tfr1onlemsucfn  6426  tfr1onlemsucaccv  6427  tfr1onlembxssdm  6429  tfr1onlembfn  6430  tfr1onlemaccex  6434  tfr1onlemres  6435  tfri1dALT  6437  tfrcllemsucfn  6439  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllembfn  6443  tfrcllemaccex  6447  tfrcllemres  6448  tfrcl  6450  rdgtfr  6460  rdgon  6472  frecabex  6484  frecabcl  6485  frecfcllem  6490  frecsuclem  6492  nnacl  6566  nnmcl  6567  nnmordi  6602  nnaordex  6614  nnm00  6616  erexb  6645  qliftfuns  6706  ixpsnval  6788  elixp2  6789  resixp  6820  mptelixpg  6821  elixpsn  6822  fundmen  6898  fopwdom  6933  xpf1o  6941  dif1en  6976  diffitest  6984  diffifi  6991  inffiexmid  7003  unfiexmid  7015  unfidisj  7019  prfidceq  7025  fiintim  7028  xpfi  7029  ssfirab  7033  fnfi  7038  iunfidisj  7048  snexxph  7052  fidcenumlemr  7057  elfi2  7074  ctssdccl  7213  isnumi  7289  cc2lem  7378  cc3  7380  addnidpig  7449  indpi  7455  dfplpq2  7467  addclnq  7488  mulclnq  7489  nnnq0lem1  7559  addclnq0  7564  mulclnq0  7565  nqpnq0nq  7566  distrnq0  7572  prloc  7604  prarloclemlo  7607  prarloclem3  7610  prarloclem5  7613  genpml  7630  genpmu  7631  addnqprl  7642  addnqpru  7643  mulnqprl  7681  mulnqpru  7682  ltexprlemell  7711  ltexprlemelu  7712  ltexprlemdisj  7719  ltexprlemloc  7720  ltexprlemrl  7723  ltexprlemru  7725  ltexpri  7726  recexprlemm  7737  recexprlemdisj  7743  recexprlemloc  7744  recexprlem1ssl  7746  recexprlem1ssu  7747  recexpr  7751  addclsr  7866  mulclsr  7867  suplocsrlemb  7919  suplocsrlempr  7920  suplocsrlem  7921  suplocsr  7922  pitonn  7961  peano2nnnn  7966  axaddrcl  7978  axmulrcl  7980  peano5nnnn  8005  axpre-suploclemres  8014  negreb  8337  negf1o  8454  eqord1  8556  eqord2  8557  cju  9034  peano2nn  9048  nn1m1nn  9054  nnaddcl  9056  nnmulcl  9057  nnsub  9075  nndivtr  9078  un0addcl  9328  un0mulcl  9329  elnnnn0  9338  elz  9374  nnnegz  9375  znegclb  9405  zaddcllempos  9409  zaddcllemneg  9411  zaddcl  9412  nzadd  9425  zmulcl  9426  elz2  9444  zneo  9474  nneoor  9475  zeo  9478  peano5uzti  9481  zindd  9491  uzp1  9682  uzaddcl  9707  supinfneg  9716  infsupneg  9717  supminfex  9718  ublbneg  9734  eqreznegel  9735  negm  9736  qmulz  9744  qnegcl  9757  irradd  9767  irrmul  9768  fzrev2  10207  infssuzex  10376  infssuzcldc  10378  zsupssdc  10381  negqmod0  10476  frec2uzuzd  10547  frecuzrdgrrn  10553  frec2uzrdg  10554  frecuzrdgrcl  10555  frecuzrdgsuc  10559  frecuzrdgrclt  10560  frecuzrdgg  10561  frecuzrdgsuctlem  10568  xnn0nnen  10582  iseqovex  10603  seq3val  10605  seqvalcd  10606  seq3-1  10607  seqf  10609  seq3p1  10610  seqovcd  10612  seqp1cd  10615  seq3clss  10616  monoord  10630  monoord2  10631  ser3mono  10632  seq3split  10633  seqsplitg  10634  seq3caopr3  10636  seq3caopr2  10638  seqcaopr2g  10639  iseqf1olemjpcl  10653  iseqf1olemqpcl  10654  iseqf1olemfvp  10655  seq3f1olemqsumkj  10656  seq3f1olemqsum  10658  seq3f1oleml  10661  seq3f1o  10662  seqf1og  10666  seq3homo  10672  seq3z  10673  seqhomog  10675  seqfeq4g  10676  seq3distr  10677  ser3ge0  10681  expp1  10691  expcllem  10695  expcl2lemap  10696  m1expcl2  10706  facnn  10872  fac0  10873  fac1  10874  faccl  10880  facdiv  10883  facndiv  10884  bccmpl  10899  bcn2  10909  bccl  10912  fihasheqf1oi  10932  seq3coll  10987  shftlem  11127  shftf  11141  seq3shft  11149  cjval  11156  cjth  11157  remim  11171  uzin2  11298  caubnd2  11428  negfi  11539  xrmaxltsup  11569  clim  11592  clim2  11594  climshftlemg  11613  climcn1  11619  climcn2  11620  iserex  11650  climub  11655  climserle  11656  climcau  11658  serf0  11663  sumfct  11685  sumrbdclem  11688  fsum3cvg  11689  summodclem3  11691  summodclem2a  11692  zsumdc  11695  fsumgcl  11697  fsum3  11698  fsumf1o  11701  isumss  11702  isumss2  11704  fsum3cvg2  11705  fsum3ser  11708  fsumcl2lem  11709  fsumsplitf  11719  sumpr  11724  sumtp  11725  fsumm1  11727  fsum1p  11729  isummulc2  11737  fsum2dlemstep  11745  fisumcom2  11749  fsumshftm  11756  fisum0diag2  11758  fsummulc2  11759  fsumge1  11772  fsum00  11773  fsumabs  11776  telfsumo  11777  telfsumo2  11778  fsumparts  11781  fsumrelem  11782  fsumiun  11788  binomlem  11794  isumshft  11801  isum1p  11803  isumrpcl  11805  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  cvgratnnlemseq  11837  cvgratnnlemabsle  11838  cvgratnnlemfm  11840  cvgratnnlemrate  11841  cvgratnn  11842  cvgratz  11843  mertenslem2  11847  mertensabs  11848  clim2prod  11850  prodfap0  11856  prodfrecap  11857  prodfdivap  11858  prodrbdclem  11882  fproddccvg  11883  prodmodclem3  11886  prodmodclem2a  11887  zproddc  11890  fprodseq  11894  prodfct  11898  fprodf1o  11899  prodssdc  11900  fprodssdc  11901  fprodmul  11902  fprodm1  11909  fprod1p  11910  fprodm1s  11912  fprodp1s  11913  fprodcl2lem  11916  fprodabs  11927  fprod2dlemstep  11933  fprodcnv  11936  fprodcom2fi  11937  fprodrec  11940  fproddivapf  11942  fprodsplitf  11943  fprodsplit1f  11945  fprodle  11951  zeo3  12179  mulsucdiv2z  12196  zob  12202  nn0o1gt2  12216  nno  12217  nn0o  12218  uzwodc  12358  qnumdencl  12509  pcqcl  12629  pcxnn0cl  12633  pcxcl  12634  pcgcd1  12651  dvdsprmpweqle  12660  pcmpt  12666  pcmpt2  12667  pcmptdvds  12668  infpnlem2  12683  1arith  12690  elgz  12694  mul4sq  12717  4sqlem13m  12726  4sqlem17  12730  4sqlem18  12731  4sqlem19  12732  znnen  12769  ennnfonelemj0  12772  ennnfonelemg  12774  ennnfonelemom  12779  ctinfom  12799  ctiunctlemu1st  12805  ctiunctlemu2nd  12806  ctiunctlemudc  12808  ctiunctlemfo  12810  ssnnctlemct  12817  infpn2  12827  isstruct2im  12842  isstruct2r  12843  imasaddfnlemg  13146  ercpbl  13163  xpsfrnel2  13178  mgmsscl  13193  mgm1  13202  sgrppropd  13245  mndpropd  13272  issubm  13304  0subm  13316  insubm  13317  mhmima  13323  mulgsubcl  13472  issubg  13509  subgex  13512  issubg2m  13525  issubg4m  13529  0subg  13535  isnsg  13538  isnsg2  13539  nsgbi  13540  isnsg3  13543  elnmz  13544  nmzbi  13545  nmzsubg  13546  nmznsg  13549  releqgg  13556  eqgex  13557  eqgval  13559  eqgid  13562  ghmrn  13593  ghmnsgima  13604  eqgabl  13666  ablnsg  13670  gsumfzmhm2  13680  isrng  13696  issrg  13727  srgfcl  13735  isring  13762  iscrng  13765  dvdsrd  13856  unitsubm  13881  isrim0  13923  issubrng  13961  subrngringnsg  13967  issubrng2  13972  opprsubrngg  13973  issubrg  13983  subrgsubm  13996  subrgugrp  14002  issubrg2  14003  issubrg3  14009  subrgpropd  14015  aprval  14044  aprsym  14046  islmod  14053  lmodlema  14054  islmodd  14055  lmodprop2d  14110  rmodislmodlem  14112  rmodislmod  14113  lsssetm  14118  islssmd  14121  lssclg  14126  lsslss  14143  lsspropdg  14193  islidlm  14241  rnglidlmcl  14242  isridlrng  14244  rnglidlmmgm  14258  isridl  14266  gsumfzfsumlemm  14349  psrbag  14431  psr1clfi  14450  uniopn  14473  inopn  14475  fiinopn  14476  iscld  14575  iuncld  14587  tgrest  14641  iscn  14669  cnpval  14670  iscnp  14671  tgcn  14680  ssidcn  14682  lmbrf  14687  cnpnei  14691  cnima  14692  cnconst2  14705  cnrest2  14708  cnptopresti  14710  cnptoprest  14711  lmres  14720  lmtopcnp  14722  txbasval  14739  tx1cn  14741  tx2cn  14742  txcnp  14743  txcnmpt  14745  txdis1cn  14750  txlm  14751  cnmpt11  14755  cnmpt12  14759  cnmpt21  14763  cnmpt22  14766  ishmeo  14776  hmeoopn  14783  hmeocld  14784  qtopbasss  14993  fsumcncntop  15039  expcn  15041  expcncf  15081  ivthinclemlopn  15108  ivthinclemlr  15109  ivthinclemuopn  15110  ivthinclemur  15111  ivthinclemdisj  15112  ivthinclemloc  15113  ivthinc  15115  ivthdec  15116  limccl  15131  ellimc3apf  15132  cnmptlimc  15146  limccoap  15150  dvmptfsum  15197  plycolemc  15230  plycj  15233  2irrexpq  15448  2irrexpqap  15450  fsumdvdsmul  15463  perfect  15473  lgsval  15481  lgsval2lem  15487  lgsdir2lem4  15508  lgsdir2  15510  m1lgs  15562  2lgs  15581  mul2sq  15593  2sqlem6  15597  bdinex1g  15837  bj-intexr  15844  bj-prexg  15847  bj-uniex  15853  bj-uniexg  15854  bdunexb  15856  bj-indsuc  15864  exmidsbthrlem  15961  qdencn  15966  iswomni0  15990