Theorem eleq2d 2184

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 2178	. 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 104   = wceq 1314   e. wcel 1463

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111

This theorem is referenced by:  eleq12d  2185  eleqtrd  2193  neleqtrd  2212  neleqtrrd  2213  abeq2d  2227  nfceqdf  2254  drnfc1  2272  drnfc2  2273  sbcbid  2934  cbvcsb  2975  sbcel1g  2988  csbeq2d  2993  csbie2g  3016  cbvralcsf  3028  cbvrexcsf  3029  cbvreucsf  3030  cbvrabcsf  3031  opeq1  3671  opeq2  3672  cbviun  3816  cbviin  3817  iinxsng  3852  iinxprg  3853  iunxsng  3854  iunxsngf  3856  cbvdisj  3882  disjnim  3886  disjiun  3890  mpteq12f  3968  axpweq  4055  rabxfrd  4350  onsucelsucexmid  4405  ordsucunielexmid  4406  0elsucexmid  4440  0nelelxp  4528  opeliunxp  4554  opeliunxp2  4639  iunxpf  4647  elreimasng  4863  elimasng  4865  xpimasn  4945  ressn  5037  funfni  5181  fnbr  5183  fun11iun  5344  fvelrnb  5423  fvun1  5441  fvco2  5444  elfvmptrab1  5469  elfvmptrab  5470  elpreima  5493  dff3im  5519  resflem  5538  fmptco  5540  funfvima3  5605  foima2  5607  eluniimadm  5620  dff13  5623  f1eqcocnv  5646  isoini  5673  riotaeqdv  5685  mpoeq123dva  5786  cbvmpox  5803  ovelrn  5873  elovmpo  5925  fmpox  6052  disjxp1  6087  opeliunxp2f  6089  mpoxopn0yelv  6090  mpoxopovel  6092  rbropapd  6093  rntpos  6108  smoel  6151  smoiso  6153  smoel2  6154  tfrlem9  6170  tfrlemisucaccv  6176  tfrlemiubacc  6181  tfrlemi14d  6184  tfri2d  6187  tfr1onlemubacc  6197  tfr1onlemres  6200  tfrcllemubacc  6210  tfrcllemres  6213  rdgon  6237  freceq1  6243  freceq2  6244  frec0g  6248  frecabcl  6250  freccllem  6253  frecfcllem  6255  frecsuclem  6257  frecsuc  6258  nnsucelsuc  6341  nnsucuniel  6345  nnmordi  6366  ereldm  6426  iinerm  6455  elmapg  6509  elpmg  6512  elixpsn  6583  ixpsnf1o  6584  phplem4  6702  phplem3g  6703  phplem4on  6714  exmidpw  6755  fiintim  6770  fidcenumlemrks  6793  fidcenumlemrk  6794  elfi  6811  ordiso2  6872  ctssdccl  6948  archnqq  7173  ltdfpr  7262  genpelxp  7267  genpelvl  7268  genpelvu  7269  addcanprleml  7370  addcanprlemu  7371  cauappcvgprlem1  7415  cnm  7567  eluz1  9232  elixx1  9573  elioo2  9597  elfz1  9688  elfzp1  9745  fzpr  9750  fzsuc2  9752  fzrev3  9760  elfzp12  9772  fzm1  9773  fzoval  9818  elfzo  9819  fzodcel  9822  elfzom1b  9899  fzosplitsni  9905  zmodidfzo  10019  frecuzrdgtcl  10078  frecuzrdgfunlem  10085  bcval  10388  bcpasc  10405  shftfn  10489  shftval  10490  seq3shft  10503  iser3shft  11007  sumeq1  11016  summodclem3  11041  summodclem2a  11042  isumss  11052  fsumsplit  11068  sumsplitdc  11093  fsum2dlemstep  11095  fisumcom2  11099  fsumparts  11131  explecnv  11166  eftlub  11247  divalgmod  11472  algfx  11579  eucalgcvga  11585  ennnfonelemex  11772  ennnfonelemhom  11773  ennnfonelemf1  11776  ennnfonelemrn  11777  ctinfomlemom  11785  ctinfom  11786  ctiunctlemudc  11793  ctiunctlemf  11794  elrest  11970  istopon  12023  eltg  12064  eltg2  12065  eltop  12081  eltop2  12082  eltop3  12083  iscld  12115  neiss2  12154  isnei  12156  lmfval  12204  cnfval  12206  iscn  12208  iscnp  12210  tgcn  12219  tgcnp  12220  lmbrf  12226  cnptopresti  12249  txbas  12269  eltx  12270  txdis  12288  txdis1cn  12289  ispsmet  12312  ismet  12333  isxmet  12334  elblps  12379  elbl  12380  elmopn  12435  neibl  12480  metrest  12495  txmetcnp  12507  txmetcn  12508  metcnpd  12509  elcncf  12546  ellimc3apf  12585  limcmpted  12588  cnlimcim  12596  cnlimc  12597  eldvap  12606  dviaddf  12624  dvimulf  12625  bj-sels  12804  nninfalllemn  12894  nninfall  12896  nninfsellemeq  12902