Theorem eleq2d 2148

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 2142	. 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 103   = wceq 1284   e. wcel 1433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077

This theorem is referenced by:  eleq12d  2149  eleqtrd  2157  neleqtrd  2176  neleqtrrd  2177  abeq2d  2191  nfceqdf  2218  drnfc1  2235  drnfc2  2236  sbcbid  2871  cbvcsb  2912  sbcel1g  2925  csbeq2d  2930  csbie2g  2952  cbvralcsf  2964  cbvrexcsf  2965  cbvreucsf  2966  cbvrabcsf  2967  opeq1  3570  opeq2  3571  cbviun  3715  cbviin  3716  iinxsng  3751  iinxprg  3752  iunxsng  3753  cbvdisj  3776  mpteq12f  3858  axpweq  3945  rabxfrd  4219  onsucelsucexmid  4273  ordsucunielexmid  4274  0elsucexmid  4308  0nelelxp  4391  opeliunxp  4413  opeliunxp2  4494  iunxpf  4502  elreimasng  4711  elimasng  4713  xpimasn  4789  ressn  4878  funfni  5019  fnbr  5021  fun11iun  5167  fvelrnb  5242  fvun1  5260  fvco2  5263  elpreima  5307  dff3im  5333  fmptco  5351  funfvima3  5413  eluniimadm  5425  dff13  5428  f1eqcocnv  5451  isoini  5477  riotaeqdv  5489  mpt2eq123dva  5586  cbvmpt2x  5602  ovelrn  5669  elovmpt2  5721  fmpt2x  5846  mpt2xopn0yelv  5877  mpt2xopovel  5879  isprmpt2  5881  rntpos  5895  smoel  5938  smoiso  5940  smoel2  5941  tfrlem9  5958  tfrlemisucaccv  5962  tfrlemiubacc  5967  tfrlemi14d  5970  tfri2d  5973  freceq1  6002  freceq2  6003  frec0g  6006  frecsuclem3  6013  frecsuc  6014  nnsucelsuc  6093  nnmordi  6112  ereldm  6172  iinerm  6201  phplem4  6341  phplem3g  6342  phplem4on  6353  ordiso2  6446  archnqq  6607  ltdfpr  6696  genpelxp  6701  genpelvl  6702  genpelvu  6703  addcanprleml  6804  addcanprlemu  6805  cauappcvgprlem1  6849  eluz1  8623  elixx1  8920  elioo2  8944  elfz1  9034  elfzp1  9089  fzpr  9094  fzsuc2  9096  fzrev3  9104  elfzp12  9116  fzm1  9117  fzoval  9158  elfzo  9159  elfzom1b  9238  fzosplitsni  9244  zmodidfzo  9355  frecuzrdgfn  9414  bcval  9676  bcpasc  9693  shftfn  9712  shftval  9713  sumeq1  10192  divalgmod  10327  ialgfx  10434  eucialgcvga  10440  bj-sels  10705