Theorem eleq1d 2265

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 2259	. 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 1364   e. wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eleq12d  2267  eqeltrd  2273  eqneltrd  2292  eqneltrrd  2293  rspcimdv  2869  rspcimedv  2870  reuind  2969  sbcel2g  3105  sbccsb2g  3114  breq1  4037  breq2  4038  inex1g  4170  intexr  4184  pwexg  4214  prexg  4245  opelopabsb  4295  pofun  4348  seex  4371  uniex  4473  uniexg  4475  unexb  4478  abnexg  4482  reusv3  4496  rabxfrd  4505  onun2  4527  onsucelsucexmid  4567  ordsucunielexmid  4568  dcextest  4618  tfisi  4624  peano2  4632  seinxp  4735  opabid2  4798  opeliunxp2  4807  elrn2g  4857  opeldm  4870  opeldmg  4872  elreldm  4893  elrn2  4909  opelresg  4954  elsnres  4984  iss  4993  elimasng  5038  issref  5053  rnxpid  5105  unielrel  5198  dffun5r  5271  funopg  5293  brprcneu  5554  tz6.12f  5590  fvelrnb  5611  ssimaex  5625  dmfco  5632  fvmpt3  5643  mptfvex  5650  fvmptf  5657  respreima  5693  fvelrn  5696  ffnfvf  5724  ffvresb  5728  fmptco  5731  fmptcof  5732  fsn  5737  fressnfv  5752  fnex  5787  funfvima  5797  funfvima3  5799  f1mpt  5821  fliftfuns  5848  isoselem  5870  ovrspc2v  5951  ffnov  6030  fovcld  6031  ovmpos  6050  ov2gf  6051  ovg  6066  funimassov  6077  caovclg  6080  elovmpo  6126  off  6152  caofdig  6173  fnexALT  6177  focdmex  6181  f1stres  6226  f2ndres  6227  xp1st  6232  xp2nd  6233  elxp6  6236  oprssdmm  6238  unielxp  6241  fmpox  6267  mpofvex  6272  opeliunxp2f  6305  dftpos4  6330  smoel  6367  tfrlem3-2d  6379  tfrlem8  6385  tfrlem9  6386  tfrlemibxssdm  6394  tfrlemi1  6399  tfrexlem  6401  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemaccex  6415  tfr1onlemres  6416  tfri1dALT  6418  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemaccex  6428  tfrcllemres  6429  tfrcl  6431  rdgtfr  6441  rdgon  6453  frecabex  6465  frecabcl  6466  frecfcllem  6471  frecsuclem  6473  nnacl  6547  nnmcl  6548  nnmordi  6583  nnaordex  6595  nnm00  6597  erexb  6626  qliftfuns  6687  ixpsnval  6769  elixp2  6770  resixp  6801  mptelixpg  6802  elixpsn  6803  fundmen  6874  fopwdom  6906  xpf1o  6914  dif1en  6949  diffitest  6957  diffifi  6964  inffiexmid  6976  unfiexmid  6988  unfidisj  6992  prfidceq  6998  fiintim  7001  xpfi  7002  ssfirab  7006  fnfi  7011  iunfidisj  7021  snexxph  7025  fidcenumlemr  7030  elfi2  7047  ctssdccl  7186  isnumi  7260  cc2lem  7349  cc3  7351  addnidpig  7420  indpi  7426  dfplpq2  7438  addclnq  7459  mulclnq  7460  nnnq0lem1  7530  addclnq0  7535  mulclnq0  7536  nqpnq0nq  7537  distrnq0  7543  prloc  7575  prarloclemlo  7578  prarloclem3  7581  prarloclem5  7584  genpml  7601  genpmu  7602  addnqprl  7613  addnqpru  7614  mulnqprl  7652  mulnqpru  7653  ltexprlemell  7682  ltexprlemelu  7683  ltexprlemdisj  7690  ltexprlemloc  7691  ltexprlemrl  7694  ltexprlemru  7696  ltexpri  7697  recexprlemm  7708  recexprlemdisj  7714  recexprlemloc  7715  recexprlem1ssl  7717  recexprlem1ssu  7718  recexpr  7722  addclsr  7837  mulclsr  7838  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  suplocsr  7893  pitonn  7932  peano2nnnn  7937  axaddrcl  7949  axmulrcl  7951  peano5nnnn  7976  axpre-suploclemres  7985  negreb  8308  negf1o  8425  eqord1  8527  eqord2  8528  cju  9005  peano2nn  9019  nn1m1nn  9025  nnaddcl  9027  nnmulcl  9028  nnsub  9046  nndivtr  9049  un0addcl  9299  un0mulcl  9300  elnnnn0  9309  elz  9345  nnnegz  9346  znegclb  9376  zaddcllempos  9380  zaddcllemneg  9382  zaddcl  9383  nzadd  9395  zmulcl  9396  elz2  9414  zneo  9444  nneoor  9445  zeo  9448  peano5uzti  9451  zindd  9461  uzp1  9652  uzaddcl  9677  supinfneg  9686  infsupneg  9687  supminfex  9688  ublbneg  9704  eqreznegel  9705  negm  9706  qmulz  9714  qnegcl  9727  irradd  9737  irrmul  9738  fzrev2  10177  infssuzex  10340  infssuzcldc  10342  zsupssdc  10345  negqmod0  10440  frec2uzuzd  10511  frecuzrdgrrn  10517  frec2uzrdg  10518  frecuzrdgrcl  10519  frecuzrdgsuc  10523  frecuzrdgrclt  10524  frecuzrdgg  10525  frecuzrdgsuctlem  10532  xnn0nnen  10546  iseqovex  10567  seq3val  10569  seqvalcd  10570  seq3-1  10571  seqf  10573  seq3p1  10574  seqovcd  10576  seqp1cd  10579  seq3clss  10580  monoord  10594  monoord2  10595  ser3mono  10596  seq3split  10597  seqsplitg  10598  seq3caopr3  10600  seq3caopr2  10602  seqcaopr2g  10603  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  iseqf1olemfvp  10619  seq3f1olemqsumkj  10620  seq3f1olemqsum  10622  seq3f1oleml  10625  seq3f1o  10626  seqf1og  10630  seq3homo  10636  seq3z  10637  seqhomog  10639  seqfeq4g  10640  seq3distr  10641  ser3ge0  10645  expp1  10655  expcllem  10659  expcl2lemap  10660  m1expcl2  10670  facnn  10836  fac0  10837  fac1  10838  faccl  10844  facdiv  10847  facndiv  10848  bccmpl  10863  bcn2  10873  bccl  10876  fihasheqf1oi  10896  seq3coll  10951  shftlem  10998  shftf  11012  seq3shft  11020  cjval  11027  cjth  11028  remim  11042  uzin2  11169  caubnd2  11299  negfi  11410  xrmaxltsup  11440  clim  11463  clim2  11465  climshftlemg  11484  climcn1  11490  climcn2  11491  iserex  11521  climub  11526  climserle  11527  climcau  11529  serf0  11534  sumfct  11556  sumrbdclem  11559  fsum3cvg  11560  summodclem3  11562  summodclem2a  11563  zsumdc  11566  fsumgcl  11568  fsum3  11569  fsumf1o  11572  isumss  11573  isumss2  11575  fsum3cvg2  11576  fsum3ser  11579  fsumcl2lem  11580  fsumsplitf  11590  sumpr  11595  sumtp  11596  fsumm1  11598  fsum1p  11600  isummulc2  11608  fsum2dlemstep  11616  fisumcom2  11620  fsumshftm  11627  fisum0diag2  11629  fsummulc2  11630  fsumge1  11643  fsum00  11644  fsumabs  11647  telfsumo  11648  telfsumo2  11649  fsumparts  11652  fsumrelem  11653  fsumiun  11659  binomlem  11665  isumshft  11672  isum1p  11674  isumrpcl  11676  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  cvgratnnlemseq  11708  cvgratnnlemabsle  11709  cvgratnnlemfm  11711  cvgratnnlemrate  11712  cvgratnn  11713  cvgratz  11714  mertenslem2  11718  mertensabs  11719  clim2prod  11721  prodfap0  11727  prodfrecap  11728  prodfdivap  11729  prodrbdclem  11753  fproddccvg  11754  prodmodclem3  11757  prodmodclem2a  11758  zproddc  11761  fprodseq  11765  prodfct  11769  fprodf1o  11770  prodssdc  11771  fprodssdc  11772  fprodmul  11773  fprodm1  11780  fprod1p  11781  fprodm1s  11783  fprodp1s  11784  fprodcl2lem  11787  fprodabs  11798  fprod2dlemstep  11804  fprodcnv  11807  fprodcom2fi  11808  fprodrec  11811  fproddivapf  11813  fprodsplitf  11814  fprodsplit1f  11816  fprodle  11822  zeo3  12050  mulsucdiv2z  12067  zob  12073  nn0o1gt2  12087  nno  12088  nn0o  12089  uzwodc  12229  qnumdencl  12380  pcqcl  12500  pcxnn0cl  12504  pcxcl  12505  pcgcd1  12522  dvdsprmpweqle  12531  pcmpt  12537  pcmpt2  12538  pcmptdvds  12539  infpnlem2  12554  1arith  12561  elgz  12565  mul4sq  12588  4sqlem13m  12597  4sqlem17  12601  4sqlem18  12602  4sqlem19  12603  znnen  12640  ennnfonelemj0  12643  ennnfonelemg  12645  ennnfonelemom  12650  ctinfom  12670  ctiunctlemu1st  12676  ctiunctlemu2nd  12677  ctiunctlemudc  12679  ctiunctlemfo  12681  ssnnctlemct  12688  infpn2  12698  isstruct2im  12713  isstruct2r  12714  imasaddfnlemg  13016  ercpbl  13033  xpsfrnel2  13048  mgmsscl  13063  mgm1  13072  sgrppropd  13115  mndpropd  13142  issubm  13174  0subm  13186  insubm  13187  mhmima  13193  mulgsubcl  13342  issubg  13379  subgex  13382  issubg2m  13395  issubg4m  13399  0subg  13405  isnsg  13408  isnsg2  13409  nsgbi  13410  isnsg3  13413  elnmz  13414  nmzbi  13415  nmzsubg  13416  nmznsg  13419  releqgg  13426  eqgex  13427  eqgval  13429  eqgid  13432  ghmrn  13463  ghmnsgima  13474  eqgabl  13536  ablnsg  13540  gsumfzmhm2  13550  isrng  13566  issrg  13597  srgfcl  13605  isring  13632  iscrng  13635  dvdsrd  13726  unitsubm  13751  isrim0  13793  issubrng  13831  subrngringnsg  13837  issubrng2  13842  opprsubrngg  13843  issubrg  13853  subrgsubm  13866  subrgugrp  13872  issubrg2  13873  issubrg3  13879  subrgpropd  13885  aprval  13914  aprsym  13916  islmod  13923  lmodlema  13924  islmodd  13925  lmodprop2d  13980  rmodislmodlem  13982  rmodislmod  13983  lsssetm  13988  islssmd  13991  lssclg  13996  lsslss  14013  lsspropdg  14063  islidlm  14111  rnglidlmcl  14112  isridlrng  14114  rnglidlmmgm  14128  isridl  14136  gsumfzfsumlemm  14219  psrbag  14299  psr1clfi  14316  uniopn  14321  inopn  14323  fiinopn  14324  iscld  14423  iuncld  14435  tgrest  14489  iscn  14517  cnpval  14518  iscnp  14519  tgcn  14528  ssidcn  14530  lmbrf  14535  cnpnei  14539  cnima  14540  cnconst2  14553  cnrest2  14556  cnptopresti  14558  cnptoprest  14559  lmres  14568  lmtopcnp  14570  txbasval  14587  tx1cn  14589  tx2cn  14590  txcnp  14591  txcnmpt  14593  txdis1cn  14598  txlm  14599  cnmpt11  14603  cnmpt12  14607  cnmpt21  14611  cnmpt22  14614  ishmeo  14624  hmeoopn  14631  hmeocld  14632  qtopbasss  14841  fsumcncntop  14887  expcn  14889  expcncf  14929  ivthinclemlopn  14956  ivthinclemlr  14957  ivthinclemuopn  14958  ivthinclemur  14959  ivthinclemdisj  14960  ivthinclemloc  14961  ivthinc  14963  ivthdec  14964  limccl  14979  ellimc3apf  14980  cnmptlimc  14994  limccoap  14998  dvmptfsum  15045  plycolemc  15078  plycj  15081  2irrexpq  15296  2irrexpqap  15298  fsumdvdsmul  15311  perfect  15321  lgsval  15329  lgsval2lem  15335  lgsdir2lem4  15356  lgsdir2  15358  m1lgs  15410  2lgs  15429  mul2sq  15441  2sqlem6  15445  bdinex1g  15631  bj-intexr  15638  bj-prexg  15641  bj-uniex  15647  bj-uniexg  15648  bdunexb  15650  bj-indsuc  15658  exmidsbthrlem  15753  qdencn  15758  iswomni0  15782