Theorem eleq2d 2157

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 2151	. 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 1289   e. wcel 1438

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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084

This theorem is referenced by:  eleq12d  2158  eleqtrd  2166  neleqtrd  2185  neleqtrrd  2186  abeq2d  2200  nfceqdf  2227  drnfc1  2245  drnfc2  2246  sbcbid  2894  cbvcsb  2935  sbcel1g  2948  csbeq2d  2953  csbie2g  2976  cbvralcsf  2988  cbvrexcsf  2989  cbvreucsf  2990  cbvrabcsf  2991  opeq1  3617  opeq2  3618  cbviun  3762  cbviin  3763  iinxsng  3798  iinxprg  3799  iunxsng  3800  iunxsngf  3802  cbvdisj  3824  disjnim  3828  disjiun  3832  mpteq12f  3910  axpweq  3998  rabxfrd  4282  onsucelsucexmid  4336  ordsucunielexmid  4337  0elsucexmid  4371  0nelelxp  4456  opeliunxp  4481  opeliunxp2  4564  iunxpf  4572  elreimasng  4785  elimasng  4787  xpimasn  4866  ressn  4958  funfni  5100  fnbr  5102  fun11iun  5258  fvelrnb  5336  fvun1  5354  fvco2  5357  elpreima  5402  dff3im  5428  resflem  5446  fmptco  5448  funfvima3  5510  foima2  5512  eluniimadm  5526  dff13  5529  f1eqcocnv  5552  isoini  5579  riotaeqdv  5591  mpt2eq123dva  5692  cbvmpt2x  5708  ovelrn  5775  elovmpt2  5827  fmpt2x  5952  disjxp1  5983  opeliunxp2f  5985  mpt2xopn0yelv  5986  mpt2xopovel  5988  isprmpt2  5990  rntpos  6004  smoel  6047  smoiso  6049  smoel2  6050  tfrlem9  6066  tfrlemisucaccv  6072  tfrlemiubacc  6077  tfrlemi14d  6080  tfri2d  6083  tfr1onlemubacc  6093  tfr1onlemres  6096  tfrcllemubacc  6106  tfrcllemres  6109  rdgon  6133  freceq1  6139  freceq2  6140  frec0g  6144  frecabcl  6146  freccllem  6149  frecfcllem  6151  frecsuclem  6153  frecsuc  6154  nnsucelsuc  6234  nnsucuniel  6238  nnmordi  6255  ereldm  6315  iinerm  6344  elmapg  6398  elpmg  6401  phplem4  6551  phplem3g  6552  phplem4on  6563  exmidpw  6604  fidcenumlemrks  6641  fidcenumlemrk  6642  ordiso2  6707  archnqq  6955  ltdfpr  7044  genpelxp  7049  genpelvl  7050  genpelvu  7051  addcanprleml  7152  addcanprlemu  7153  cauappcvgprlem1  7197  eluz1  8992  elixx1  9284  elioo2  9308  elfz1  9398  elfzp1  9453  fzpr  9458  fzsuc2  9460  fzrev3  9468  elfzp12  9480  fzm1  9481  fzoval  9524  elfzo  9525  fzodcel  9528  elfzom1b  9605  fzosplitsni  9611  zmodidfzo  9725  frecuzrdgtcl  9784  frecuzrdgfunlem  9791  bcval  10121  bcpasc  10138  shftfn  10222  shftval  10223  seq3shft  10236  iser3shft  10698  sumeq1  10707  isummolem3  10732  isummolem2a  10733  isumss  10745  fsumsplit  10762  sumsplitdc  10787  fsum2dlemstep  10789  fisumcom2  10793  fsumparts  10825  explecnv  10858  divalgmod  11007  ialgfx  11114  eucialgcvga  11120  bj-sels  11449  nninfalllemn  11542  nninfall  11544  nninfsellemeq  11550