Theorem eleq2d 2236

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 2230	. 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 1343   e. wcel 2136

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  eleq12d  2237  eleqtrd  2245  neleqtrd  2264  neleqtrrd  2265  abeq2d  2279  nfceqdf  2307  drnfc1  2325  drnfc2  2326  sbcbid  3008  cbvcsbw  3049  cbvcsb  3050  sbcel1g  3064  csbeq2d  3070  csbie2g  3095  cbvralcsf  3107  cbvrexcsf  3108  cbvreucsf  3109  cbvrabcsf  3110  opeq1  3758  opeq2  3759  cbviun  3903  cbviin  3904  iinxsng  3939  iinxprg  3940  iunxsng  3941  iunxsngf  3943  cbvdisj  3969  disjnim  3973  disjiun  3977  mpteq12f  4062  axpweq  4150  rabxfrd  4447  onsucelsucexmid  4507  ordsucunielexmid  4508  0elsucexmid  4542  0nelelxp  4633  opeliunxp  4659  opeliunxp2  4744  iunxpf  4752  elreimasng  4970  elimasng  4972  xpimasn  5052  ressn  5144  funfni  5288  fnbr  5290  fun11iun  5453  fvelrnb  5534  fvun1  5552  fvco2  5555  elfvmptrab1  5580  elfvmptrab  5581  elpreima  5604  dff3im  5630  resflem  5649  fmptco  5651  funfvima3  5718  foima2  5720  eluniimadm  5733  dff13  5736  f1eqcocnv  5759  isoini  5786  riotaeqdv  5799  mpoeq123dva  5903  cbvmpox  5920  ovelrn  5990  elovmpo  6039  fmpox  6168  disjxp1  6204  opeliunxp2f  6206  mpoxopn0yelv  6207  mpoxopovel  6209  rbropapd  6210  rntpos  6225  smoel  6268  smoiso  6270  smoel2  6271  tfrlem9  6287  tfrlemisucaccv  6293  tfrlemiubacc  6298  tfrlemi14d  6301  tfri2d  6304  tfr1onlemubacc  6314  tfr1onlemres  6317  tfrcllemubacc  6327  tfrcllemres  6330  rdgon  6354  freceq1  6360  freceq2  6361  frec0g  6365  frecabcl  6367  freccllem  6370  frecfcllem  6372  frecsuclem  6374  frecsuc  6375  nnsucelsuc  6459  nnsucuniel  6463  nnmordi  6484  ereldm  6544  iinerm  6573  elmapg  6627  elpmg  6630  elixpsn  6701  ixpsnf1o  6702  phplem4  6821  phplem3g  6822  phplem4on  6833  exmidpw  6874  fiintim  6894  fidcenumlemrks  6918  fidcenumlemrk  6919  elfi  6936  ordiso2  7000  ctssdccl  7076  nnnninfeq  7092  cc2lem  7207  cc2  7208  cc3  7209  archnqq  7358  ltdfpr  7447  genpelxp  7452  genpelvl  7453  genpelvu  7454  addcanprleml  7555  addcanprlemu  7556  cauappcvgprlem1  7600  suplocexprlemell  7654  suplocexprlemmu  7659  suplocexprlemru  7660  suplocexprlemdisj  7661  suplocexprlemloc  7662  suplocexprlemub  7664  suplocexprlemlub  7665  cnm  7773  eluz1  9470  elixx1  9833  elioo2  9857  elfz1  9949  elfzp1  10007  fzpr  10012  fzsuc2  10014  fzrev3  10022  elfzp12  10034  fzm1  10035  fzoval  10083  elfzo  10084  fzodcel  10087  elfzom1b  10164  fzosplitsni  10170  zmodidfzo  10288  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  bcval  10662  bcpasc  10679  shftfn  10766  shftval  10767  seq3shft  10780  iser3shft  11287  sumeq1  11296  summodclem3  11321  summodclem2a  11322  isumss  11332  fsumsplit  11348  sumsplitdc  11373  fsum2dlemstep  11375  fisumcom2  11379  fsumparts  11411  explecnv  11446  fprodsplitdc  11537  fprodsplit  11538  fprod2dlemstep  11563  fprodcom2fi  11567  eftlub  11631  divalgmod  11864  nninfdcex  11886  algfx  11984  eucalgcvga  11990  reumodprminv  12185  nnnn0modprm0  12187  ennnfonelemex  12347  ennnfonelemhom  12348  ennnfonelemf1  12351  ennnfonelemrn  12352  ctinfomlemom  12360  ctinfom  12361  ctiunctlemudc  12370  ctiunctlemf  12371  elrest  12563  grpidvalg  12604  grpidpropdg  12605  grpidd  12614  istopon  12651  eltg  12692  eltg2  12693  eltop  12709  eltop2  12710  eltop3  12711  iscld  12743  neiss2  12782  isnei  12784  lmfval  12832  cnfval  12834  iscn  12837  iscnp  12839  tgcn  12848  tgcnp  12849  lmbrf  12855  cnptopresti  12878  txbas  12898  eltx  12899  txdis  12917  txdis1cn  12918  hmeofvalg  12943  ishmeo  12944  ispsmet  12963  ismet  12984  isxmet  12985  elblps  13030  elbl  13031  elmopn  13086  neibl  13131  metrest  13146  txmetcnp  13158  txmetcn  13159  metcnpd  13160  elcncf  13200  ellimc3apf  13269  limcmpted  13272  cnlimcim  13280  cnlimc  13281  eldvap  13291  dviaddf  13309  dvimulf  13310  bj-sels  13796  nninfall  13889  nninfsellemeq  13894