Theorem eleq1d 2246

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 2240	. 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 1353   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eleq12d  2248  eqeltrd  2254  eqneltrd  2273  eqneltrrd  2274  rspcimdv  2844  rspcimedv  2845  reuind  2944  sbcel2g  3080  sbccsb2g  3089  breq1  4008  breq2  4009  inex1g  4141  intexr  4152  pwexg  4182  prexg  4213  opelopabsb  4262  pofun  4314  seex  4337  uniex  4439  uniexg  4441  unexb  4444  abnexg  4448  reusv3  4462  rabxfrd  4471  onun2  4491  onsucelsucexmid  4531  ordsucunielexmid  4532  dcextest  4582  tfisi  4588  peano2  4596  seinxp  4699  opabid2  4760  opeliunxp2  4769  elrn2g  4819  opeldm  4832  opeldmg  4834  elreldm  4855  elrn2  4871  opelresg  4916  elsnres  4946  iss  4955  elimasng  4998  issref  5013  rnxpid  5065  unielrel  5158  dffun5r  5230  funopg  5252  brprcneu  5510  tz6.12f  5546  fvelrnb  5565  ssimaex  5579  dmfco  5586  fvmpt3  5597  mptfvex  5603  fvmptf  5610  respreima  5646  fvelrn  5649  ffnfvf  5677  ffvresb  5681  fmptco  5684  fmptcof  5685  fsn  5690  fressnfv  5705  fnex  5740  funfvima  5750  funfvima3  5752  f1mpt  5774  fliftfuns  5801  isoselem  5823  ovrspc2v  5903  ffnov  5981  fovcl  5982  ovmpos  6000  ov2gf  6001  ovg  6015  funimassov  6026  caovclg  6029  elovmpo  6074  off  6097  fnexALT  6114  focdmex  6118  f1stres  6162  f2ndres  6163  xp1st  6168  xp2nd  6169  elxp6  6172  oprssdmm  6174  unielxp  6177  fmpox  6203  mpofvex  6206  opeliunxp2f  6241  dftpos4  6266  smoel  6303  tfrlem3-2d  6315  tfrlem8  6321  tfrlem9  6322  tfrlemibxssdm  6330  tfrlemi1  6335  tfrexlem  6337  tfr1onlemsucfn  6343  tfr1onlemsucaccv  6344  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfr1onlemaccex  6351  tfr1onlemres  6352  tfri1dALT  6354  tfrcllemsucfn  6356  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllembfn  6360  tfrcllemaccex  6364  tfrcllemres  6365  tfrcl  6367  rdgtfr  6377  rdgon  6389  frecabex  6401  frecabcl  6402  frecfcllem  6407  frecsuclem  6409  nnacl  6483  nnmcl  6484  nnmordi  6519  nnaordex  6531  nnm00  6533  erexb  6562  qliftfuns  6621  ixpsnval  6703  elixp2  6704  resixp  6735  mptelixpg  6736  elixpsn  6737  fundmen  6808  fopwdom  6838  xpf1o  6846  dif1en  6881  diffitest  6889  diffifi  6896  inffiexmid  6908  unfiexmid  6919  unfidisj  6923  fiintim  6930  xpfi  6931  ssfirab  6935  fnfi  6938  iunfidisj  6947  snexxph  6951  fidcenumlemr  6956  elfi2  6973  ctssdccl  7112  isnumi  7183  cc2lem  7267  cc3  7269  addnidpig  7337  indpi  7343  dfplpq2  7355  addclnq  7376  mulclnq  7377  nnnq0lem1  7447  addclnq0  7452  mulclnq0  7453  nqpnq0nq  7454  distrnq0  7460  prloc  7492  prarloclemlo  7495  prarloclem3  7498  prarloclem5  7501  genpml  7518  genpmu  7519  addnqprl  7530  addnqpru  7531  mulnqprl  7569  mulnqpru  7570  ltexprlemell  7599  ltexprlemelu  7600  ltexprlemdisj  7607  ltexprlemloc  7608  ltexprlemrl  7611  ltexprlemru  7613  ltexpri  7614  recexprlemm  7625  recexprlemdisj  7631  recexprlemloc  7632  recexprlem1ssl  7634  recexprlem1ssu  7635  recexpr  7639  addclsr  7754  mulclsr  7755  suplocsrlemb  7807  suplocsrlempr  7808  suplocsrlem  7809  suplocsr  7810  pitonn  7849  peano2nnnn  7854  axaddrcl  7866  axmulrcl  7868  peano5nnnn  7893  axpre-suploclemres  7902  negreb  8224  negf1o  8341  eqord1  8442  eqord2  8443  cju  8920  peano2nn  8933  nn1m1nn  8939  nnaddcl  8941  nnmulcl  8942  nnsub  8960  nndivtr  8963  un0addcl  9211  un0mulcl  9212  elnnnn0  9221  elz  9257  nnnegz  9258  znegclb  9288  zaddcllempos  9292  zaddcllemneg  9294  zaddcl  9295  nzadd  9307  zmulcl  9308  elz2  9326  zneo  9356  nneoor  9357  zeo  9360  peano5uzti  9363  zindd  9373  uzp1  9563  uzaddcl  9588  supinfneg  9597  infsupneg  9598  supminfex  9599  ublbneg  9615  eqreznegel  9616  negm  9617  qmulz  9625  qnegcl  9638  irradd  9648  irrmul  9649  fzrev2  10087  negqmod0  10333  frec2uzuzd  10404  frecuzrdgrrn  10410  frec2uzrdg  10411  frecuzrdgrcl  10412  frecuzrdgsuc  10416  frecuzrdgrclt  10417  frecuzrdgg  10418  frecuzrdgsuctlem  10425  iseqovex  10458  seq3val  10460  seqvalcd  10461  seq3-1  10462  seqf  10463  seq3p1  10464  seqovcd  10465  seqp1cd  10468  seq3clss  10469  monoord  10478  monoord2  10479  ser3mono  10480  seq3split  10481  seq3caopr3  10483  seq3caopr2  10484  iseqf1olemjpcl  10497  iseqf1olemqpcl  10498  iseqf1olemfvp  10499  seq3f1olemqsumkj  10500  seq3f1olemqsum  10502  seq3f1oleml  10505  seq3f1o  10506  seq3homo  10512  seq3z  10513  seq3distr  10515  ser3ge0  10519  expp1  10529  expcllem  10533  expcl2lemap  10534  m1expcl2  10544  facnn  10709  fac0  10710  fac1  10711  faccl  10717  facdiv  10720  facndiv  10721  bccmpl  10736  bcn2  10746  bccl  10749  fihasheqf1oi  10769  seq3coll  10824  shftlem  10827  shftf  10841  seq3shft  10849  cjval  10856  cjth  10857  remim  10871  uzin2  10998  caubnd2  11128  negfi  11238  xrmaxltsup  11268  clim  11291  clim2  11293  climshftlemg  11312  climcn1  11318  climcn2  11319  iserex  11349  climub  11354  climserle  11355  climcau  11357  serf0  11362  sumfct  11384  sumrbdclem  11387  fsum3cvg  11388  summodclem3  11390  summodclem2a  11391  zsumdc  11394  fsumgcl  11396  fsum3  11397  fsumf1o  11400  isumss  11401  isumss2  11403  fsum3cvg2  11404  fsum3ser  11407  fsumcl2lem  11408  fsumsplitf  11418  sumpr  11423  sumtp  11424  fsumm1  11426  fsum1p  11428  isummulc2  11436  fsum2dlemstep  11444  fisumcom2  11448  fsumshftm  11455  fisum0diag2  11457  fsummulc2  11458  fsumge1  11471  fsum00  11472  fsumabs  11475  telfsumo  11476  telfsumo2  11477  fsumparts  11480  fsumrelem  11481  fsumiun  11487  binomlem  11493  isumshft  11500  isum1p  11502  isumrpcl  11504  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  cvgratnnlemseq  11536  cvgratnnlemabsle  11537  cvgratnnlemfm  11539  cvgratnnlemrate  11540  cvgratnn  11541  cvgratz  11542  mertenslem2  11546  mertensabs  11547  clim2prod  11549  prodfap0  11555  prodfrecap  11556  prodfdivap  11557  prodrbdclem  11581  fproddccvg  11582  prodmodclem3  11585  prodmodclem2a  11586  zproddc  11589  fprodseq  11593  prodfct  11597  fprodf1o  11598  prodssdc  11599  fprodssdc  11600  fprodmul  11601  fprodm1  11608  fprod1p  11609  fprodm1s  11611  fprodp1s  11612  fprodcl2lem  11615  fprodabs  11626  fprod2dlemstep  11632  fprodcnv  11635  fprodcom2fi  11636  fprodrec  11639  fproddivapf  11641  fprodsplitf  11642  fprodsplit1f  11644  fprodle  11650  zeo3  11875  mulsucdiv2z  11892  zob  11898  nn0o1gt2  11912  nno  11913  nn0o  11914  infssuzex  11952  infssuzcldc  11954  zsupssdc  11957  uzwodc  12040  qnumdencl  12189  pcqcl  12308  pcxnn0cl  12312  pcxcl  12313  pcgcd1  12329  dvdsprmpweqle  12338  pcmpt  12343  pcmpt2  12344  pcmptdvds  12345  infpnlem2  12360  1arith  12367  elgz  12371  mul4sq  12394  znnen  12401  ennnfonelemj0  12404  ennnfonelemg  12406  ennnfonelemom  12411  ctinfom  12431  ctiunctlemu1st  12437  ctiunctlemu2nd  12438  ctiunctlemudc  12440  ctiunctlemfo  12442  ssnnctlemct  12449  infpn2  12459  isstruct2im  12474  isstruct2r  12475  imasaddfnlemg  12740  ercpbl  12755  xpsfrnel2  12770  mgmsscl  12785  mgm1  12794  mndpropd  12846  issubm  12868  0subm  12876  insubm  12877  mhmima  12880  mulgsubcl  13002  issubg  13038  subgex  13041  issubg2m  13054  issubg4m  13058  0subg  13064  isnsg  13067  isnsg2  13068  nsgbi  13069  isnsg3  13072  elnmz  13073  nmzbi  13074  nmzsubg  13075  nmznsg  13078  releqgg  13085  eqgval  13087  eqgid  13090  issrg  13153  srgfcl  13161  isring  13188  iscrng  13191  dvdsrd  13268  unitsubm  13293  issubrg  13347  subrgsubm  13360  subrgugrp  13366  issubrg2  13367  issubrg3  13373  subrgpropd  13374  aprval  13377  aprsym  13379  islmod  13386  lmodlema  13387  islmodd  13388  lmodprop2d  13443  rmodislmodlem  13445  rmodislmod  13446  lsssetm  13449  islssmd  13451  lssclg  13456  lsslss  13473  uniopn  13540  inopn  13542  fiinopn  13543  iscld  13642  iuncld  13654  tgrest  13708  iscn  13736  cnpval  13737  iscnp  13738  tgcn  13747  ssidcn  13749  lmbrf  13754  cnpnei  13758  cnima  13759  cnconst2  13772  cnrest2  13775  cnptopresti  13777  cnptoprest  13778  lmres  13787  lmtopcnp  13789  txbasval  13806  tx1cn  13808  tx2cn  13809  txcnp  13810  txcnmpt  13812  txdis1cn  13817  txlm  13818  cnmpt11  13822  cnmpt12  13826  cnmpt21  13830  cnmpt22  13833  ishmeo  13843  hmeoopn  13850  hmeocld  13851  qtopbasss  14060  fsumcncntop  14095  expcncf  14131  ivthinclemlopn  14153  ivthinclemlr  14154  ivthinclemuopn  14155  ivthinclemur  14156  ivthinclemdisj  14157  ivthinclemloc  14158  ivthinc  14160  ivthdec  14161  limccl  14167  ellimc3apf  14168  cnmptlimc  14182  limccoap  14186  2irrexpq  14433  2irrexpqap  14435  lgsval  14444  lgsval2lem  14450  lgsdir2lem4  14471  lgsdir2  14473  m1lgs  14491  mul2sq  14502  2sqlem6  14506  bdinex1g  14692  bj-intexr  14699  bj-prexg  14702  bj-uniex  14708  bj-uniexg  14709  bdunexb  14711  bj-indsuc  14719  exmidsbthrlem  14809  qdencn  14814  iswomni0  14838