Theorem eleq2d 2152

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 2146	. 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 1285   e. wcel 1434

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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-clel 2079

This theorem is referenced by:  eleq12d  2153  eleqtrd  2161  neleqtrd  2180  neleqtrrd  2181  abeq2d  2195  nfceqdf  2222  drnfc1  2239  drnfc2  2240  sbcbid  2882  cbvcsb  2923  sbcel1g  2936  csbeq2d  2941  csbie2g  2963  cbvralcsf  2975  cbvrexcsf  2976  cbvreucsf  2977  cbvrabcsf  2978  opeq1  3596  opeq2  3597  cbviun  3741  cbviin  3742  iinxsng  3777  iinxprg  3778  iunxsng  3779  cbvdisj  3802  mpteq12f  3884  axpweq  3971  rabxfrd  4255  onsucelsucexmid  4309  ordsucunielexmid  4310  0elsucexmid  4344  0nelelxp  4429  opeliunxp  4451  opeliunxp2  4534  iunxpf  4542  elreimasng  4753  elimasng  4755  xpimasn  4833  ressn  4925  funfni  5067  fnbr  5069  fun11iun  5222  fvelrnb  5297  fvun1  5315  fvco2  5318  elpreima  5363  dff3im  5389  resflem  5404  fmptco  5406  funfvima3  5468  foima2  5470  eluniimadm  5484  dff13  5487  f1eqcocnv  5510  isoini  5536  riotaeqdv  5548  mpt2eq123dva  5645  cbvmpt2x  5661  ovelrn  5728  elovmpt2  5780  fmpt2x  5905  mpt2xopn0yelv  5936  mpt2xopovel  5938  isprmpt2  5940  rntpos  5954  smoel  5997  smoiso  5999  smoel2  6000  tfrlem9  6016  tfrlemisucaccv  6022  tfrlemiubacc  6027  tfrlemi14d  6030  tfri2d  6033  tfr1onlemubacc  6043  tfr1onlemres  6046  tfrcllemubacc  6056  tfrcllemres  6059  rdgon  6083  freceq1  6089  freceq2  6090  frec0g  6094  frecabcl  6096  freccllem  6099  frecfcllem  6101  frecsuclem  6103  frecsuc  6104  nnsucelsuc  6184  nnsucuniel  6188  nnmordi  6205  ereldm  6265  iinerm  6294  elmapg  6348  elpmg  6351  phplem4  6501  phplem3g  6502  phplem4on  6513  exmidpw  6551  ordiso2  6635  archnqq  6879  ltdfpr  6968  genpelxp  6973  genpelvl  6974  genpelvu  6975  addcanprleml  7076  addcanprlemu  7077  cauappcvgprlem1  7121  eluz1  8918  elixx1  9210  elioo2  9234  elfz1  9324  elfzp1  9379  fzpr  9384  fzsuc2  9386  fzrev3  9394  elfzp12  9406  fzm1  9407  fzoval  9449  elfzo  9450  elfzom1b  9529  fzosplitsni  9535  zmodidfzo  9649  frecuzrdgtcl  9708  frecuzrdgfunlem  9715  bcval  9992  bcpasc  10009  shftfn  10086  shftval  10087  sumeq1  10566  divalgmod  10707  ialgfx  10814  eucialgcvga  10820  bj-sels  11148