Theorem eleq2d 2234

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 2228	. 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 1342   e. wcel 2135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-cleq 2157  df-clel 2160

This theorem is referenced by:  eleq12d  2235  eleqtrd  2243  neleqtrd  2262  neleqtrrd  2263  abeq2d  2277  nfceqdf  2305  drnfc1  2323  drnfc2  2324  sbcbid  3003  cbvcsbw  3044  cbvcsb  3045  sbcel1g  3059  csbeq2d  3065  csbie2g  3090  cbvralcsf  3102  cbvrexcsf  3103  cbvreucsf  3104  cbvrabcsf  3105  opeq1  3752  opeq2  3753  cbviun  3897  cbviin  3898  iinxsng  3933  iinxprg  3934  iunxsng  3935  iunxsngf  3937  cbvdisj  3963  disjnim  3967  disjiun  3971  mpteq12f  4056  axpweq  4144  rabxfrd  4441  onsucelsucexmid  4501  ordsucunielexmid  4502  0elsucexmid  4536  0nelelxp  4627  opeliunxp  4653  opeliunxp2  4738  iunxpf  4746  elreimasng  4964  elimasng  4966  xpimasn  5046  ressn  5138  funfni  5282  fnbr  5284  fun11iun  5447  fvelrnb  5528  fvun1  5546  fvco2  5549  elfvmptrab1  5574  elfvmptrab  5575  elpreima  5598  dff3im  5624  resflem  5643  fmptco  5645  funfvima3  5712  foima2  5714  eluniimadm  5727  dff13  5730  f1eqcocnv  5753  isoini  5780  riotaeqdv  5793  mpoeq123dva  5894  cbvmpox  5911  ovelrn  5981  elovmpo  6033  fmpox  6160  disjxp1  6195  opeliunxp2f  6197  mpoxopn0yelv  6198  mpoxopovel  6200  rbropapd  6201  rntpos  6216  smoel  6259  smoiso  6261  smoel2  6262  tfrlem9  6278  tfrlemisucaccv  6284  tfrlemiubacc  6289  tfrlemi14d  6292  tfri2d  6295  tfr1onlemubacc  6305  tfr1onlemres  6308  tfrcllemubacc  6318  tfrcllemres  6321  rdgon  6345  freceq1  6351  freceq2  6352  frec0g  6356  frecabcl  6358  freccllem  6361  frecfcllem  6363  frecsuclem  6365  frecsuc  6366  nnsucelsuc  6450  nnsucuniel  6454  nnmordi  6475  ereldm  6535  iinerm  6564  elmapg  6618  elpmg  6621  elixpsn  6692  ixpsnf1o  6693  phplem4  6812  phplem3g  6813  phplem4on  6824  exmidpw  6865  fiintim  6885  fidcenumlemrks  6909  fidcenumlemrk  6910  elfi  6927  ordiso2  6991  ctssdccl  7067  nnnninfeq  7083  cc2lem  7198  cc2  7199  cc3  7200  archnqq  7349  ltdfpr  7438  genpelxp  7443  genpelvl  7444  genpelvu  7445  addcanprleml  7546  addcanprlemu  7547  cauappcvgprlem1  7591  suplocexprlemell  7645  suplocexprlemmu  7650  suplocexprlemru  7651  suplocexprlemdisj  7652  suplocexprlemloc  7653  suplocexprlemub  7655  suplocexprlemlub  7656  cnm  7764  eluz1  9461  elixx1  9824  elioo2  9848  elfz1  9940  elfzp1  9997  fzpr  10002  fzsuc2  10004  fzrev3  10012  elfzp12  10024  fzm1  10025  fzoval  10073  elfzo  10074  fzodcel  10077  elfzom1b  10154  fzosplitsni  10160  zmodidfzo  10278  frecuzrdgtcl  10337  frecuzrdgfunlem  10344  bcval  10651  bcpasc  10668  shftfn  10752  shftval  10753  seq3shft  10766  iser3shft  11273  sumeq1  11282  summodclem3  11307  summodclem2a  11308  isumss  11318  fsumsplit  11334  sumsplitdc  11359  fsum2dlemstep  11361  fisumcom2  11365  fsumparts  11397  explecnv  11432  fprodsplitdc  11523  fprodsplit  11524  fprod2dlemstep  11549  fprodcom2fi  11553  eftlub  11617  divalgmod  11849  nninfdcex  11871  algfx  11963  eucalgcvga  11969  reumodprminv  12162  nnnn0modprm0  12164  ennnfonelemex  12284  ennnfonelemhom  12285  ennnfonelemf1  12288  ennnfonelemrn  12289  ctinfomlemom  12297  ctinfom  12298  ctiunctlemudc  12307  ctiunctlemf  12308  elrest  12499  istopon  12552  eltg  12593  eltg2  12594  eltop  12610  eltop2  12611  eltop3  12612  iscld  12644  neiss2  12683  isnei  12685  lmfval  12733  cnfval  12735  iscn  12738  iscnp  12740  tgcn  12749  tgcnp  12750  lmbrf  12756  cnptopresti  12779  txbas  12799  eltx  12800  txdis  12818  txdis1cn  12819  hmeofvalg  12844  ishmeo  12845  ispsmet  12864  ismet  12885  isxmet  12886  elblps  12931  elbl  12932  elmopn  12987  neibl  13032  metrest  13047  txmetcnp  13059  txmetcn  13060  metcnpd  13061  elcncf  13101  ellimc3apf  13170  limcmpted  13173  cnlimcim  13181  cnlimc  13182  eldvap  13192  dviaddf  13210  dvimulf  13211  bj-sels  13631  nninfall  13723  nninfsellemeq  13728