Theorem eleq2d 2107

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)

Hypothesis

Ref	Expression
eleq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
eleq2d	|- ( ph -> ( C e. A <-> C e. B ) )

Proof of Theorem eleq2d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 |- ( ph -> A = B )
2		eleq2 2101	. 2 |- ( A = B -> ( C e. A <-> C e. B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C e. A <-> C e. B ) )

Syntax hints:   -> wi 4   <-> wb 98   = wceq 1243   e. wcel 1393

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036

This theorem is referenced by:  eleq12d  2108  eleqtrd  2116  neleqtrd  2135  neleqtrrd  2136  abeq2d  2150  nfceqdf  2177  drnfc1  2194  drnfc2  2195  sbcbid  2816  cbvcsb  2856  sbcel1g  2869  csbeq2d  2874  csbie2g  2896  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  opeq1  3549  opeq2  3550  cbviun  3694  cbviin  3695  iinxsng  3730  iinxprg  3731  iunxsng  3732  cbvdisj  3755  mpteq12f  3837  axpweq  3924  rabxfrd  4201  onsucelsucexmid  4255  ordsucunielexmid  4256  0elsucexmid  4289  0nelelxp  4373  opeliunxp  4395  opeliunxp2  4476  iunxpf  4484  elreimasng  4691  elimasng  4693  xpimasn  4769  ressn  4858  funfni  4999  fnbr  5001  fun11iun  5147  fvelrnb  5221  fvun1  5239  fvco2  5242  elpreima  5286  dff3im  5312  fmptco  5330  funfvima3  5392  eluniimadm  5404  dff13  5407  f1eqcocnv  5431  isoini  5457  riotaeqdv  5469  mpt2eq123dva  5566  cbvmpt2x  5582  ovelrn  5649  elovmpt2  5701  fmpt2x  5826  mpt2xopn0yelv  5854  mpt2xopovel  5856  isprmpt2  5858  rntpos  5872  smoel  5915  smoiso  5917  smoel2  5918  tfrlem9  5935  tfrlemisucaccv  5939  tfrlemiubacc  5944  tfrlemi14d  5947  tfri2d  5950  freceq1  5979  freceq2  5980  frec0g  5983  frecsuclem3  5990  frecsuc  5991  nnsucelsuc  6070  nnmordi  6089  ereldm  6149  iinerm  6178  phplem4  6318  phplem3g  6319  phplem4on  6329  ordiso2  6357  archnqq  6515  ltdfpr  6604  genpelxp  6609  genpelvl  6610  genpelvu  6611  addcanprleml  6712  addcanprlemu  6713  cauappcvgprlem1  6757  eluz1  8477  elixx1  8766  elioo2  8790  elfz1  8879  elfzp1  8934  fzpr  8939  fzsuc2  8941  fzrev3  8949  elfzp12  8961  fzm1  8962  fzoval  9005  elfzo  9006  elfzom1b  9085  fzosplitsni  9091  frecuzrdgfn  9198  shftfn  9425  shftval  9426  sumeq1  9874  ialgfx  9891  bj-sels  10034