Theorem eleq2d 2240

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 2234	. 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 1348   e. wcel 2141

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eleq12d  2241  eleqtrd  2249  neleqtrd  2268  neleqtrrd  2269  abeq2d  2283  nfceqdf  2311  drnfc1  2329  drnfc2  2330  sbcbid  3012  cbvcsbw  3053  cbvcsb  3054  sbcel1g  3068  csbeq2d  3074  csbie2g  3099  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  opeq1  3765  opeq2  3766  cbviun  3910  cbviin  3911  iinxsng  3946  iinxprg  3947  iunxsng  3948  iunxsngf  3950  cbvdisj  3976  disjnim  3980  disjiun  3984  mpteq12f  4069  axpweq  4157  rabxfrd  4454  onsucelsucexmid  4514  ordsucunielexmid  4515  0elsucexmid  4549  0nelelxp  4640  opeliunxp  4666  opeliunxp2  4751  iunxpf  4759  elreimasng  4977  elimasng  4979  xpimasn  5059  ressn  5151  funfni  5298  fnbr  5300  fun11iun  5463  fvelrnb  5544  fvun1  5562  fvco2  5565  elfvmptrab1  5590  elfvmptrab  5591  elpreima  5615  dff3im  5641  resflem  5660  fmptco  5662  funfvima3  5729  foima2  5731  eluniimadm  5744  dff13  5747  f1eqcocnv  5770  isoini  5797  riotaeqdv  5810  mpoeq123dva  5914  cbvmpox  5931  ovelrn  6001  elovmpo  6050  fmpox  6179  disjxp1  6215  opeliunxp2f  6217  mpoxopn0yelv  6218  mpoxopovel  6220  rbropapd  6221  rntpos  6236  smoel  6279  smoiso  6281  smoel2  6282  tfrlem9  6298  tfrlemisucaccv  6304  tfrlemiubacc  6309  tfrlemi14d  6312  tfri2d  6315  tfr1onlemubacc  6325  tfr1onlemres  6328  tfrcllemubacc  6338  tfrcllemres  6341  rdgon  6365  freceq1  6371  freceq2  6372  frec0g  6376  frecabcl  6378  freccllem  6381  frecfcllem  6383  frecsuclem  6385  frecsuc  6386  nnsucelsuc  6470  nnsucuniel  6474  nnmordi  6495  ereldm  6556  iinerm  6585  elmapg  6639  elpmg  6642  elixpsn  6713  ixpsnf1o  6714  phplem4  6833  phplem3g  6834  phplem4on  6845  exmidpw  6886  fiintim  6906  fidcenumlemrks  6930  fidcenumlemrk  6931  elfi  6948  ordiso2  7012  ctssdccl  7088  nnnninfeq  7104  cc2lem  7228  cc2  7229  cc3  7230  archnqq  7379  ltdfpr  7468  genpelxp  7473  genpelvl  7474  genpelvu  7475  addcanprleml  7576  addcanprlemu  7577  cauappcvgprlem1  7621  suplocexprlemell  7675  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemub  7685  suplocexprlemlub  7686  cnm  7794  eluz1  9491  elixx1  9854  elioo2  9878  elfz1  9970  elfzp1  10028  fzpr  10033  fzsuc2  10035  fzrev3  10043  elfzp12  10055  fzm1  10056  fzoval  10104  elfzo  10105  fzodcel  10108  elfzom1b  10185  fzosplitsni  10191  zmodidfzo  10309  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  bcval  10683  bcpasc  10700  shftfn  10788  shftval  10789  seq3shft  10802  iser3shft  11309  sumeq1  11318  summodclem3  11343  summodclem2a  11344  isumss  11354  fsumsplit  11370  sumsplitdc  11395  fsum2dlemstep  11397  fisumcom2  11401  fsumparts  11433  explecnv  11468  fprodsplitdc  11559  fprodsplit  11560  fprod2dlemstep  11585  fprodcom2fi  11589  eftlub  11653  divalgmod  11886  nninfdcex  11908  algfx  12006  eucalgcvga  12012  reumodprminv  12207  nnnn0modprm0  12209  ennnfonelemex  12369  ennnfonelemhom  12370  ennnfonelemf1  12373  ennnfonelemrn  12374  ctinfomlemom  12382  ctinfom  12383  ctiunctlemudc  12392  ctiunctlemf  12393  elrest  12586  grpidvalg  12627  grpidpropdg  12628  grpidd  12637  ismndd  12673  mndpropd  12676  ismhm  12685  issubm  12695  istopon  12805  eltg  12846  eltg2  12847  eltop  12863  eltop2  12864  eltop3  12865  iscld  12897  neiss2  12936  isnei  12938  lmfval  12986  cnfval  12988  iscn  12991  iscnp  12993  tgcn  13002  tgcnp  13003  lmbrf  13009  cnptopresti  13032  txbas  13052  eltx  13053  txdis  13071  txdis1cn  13072  hmeofvalg  13097  ishmeo  13098  ispsmet  13117  ismet  13138  isxmet  13139  elblps  13184  elbl  13185  elmopn  13240  neibl  13285  metrest  13300  txmetcnp  13312  txmetcn  13313  metcnpd  13314  elcncf  13354  ellimc3apf  13423  limcmpted  13426  cnlimcim  13434  cnlimc  13435  eldvap  13445  dviaddf  13463  dvimulf  13464  bj-sels  13949  nninfall  14042  nninfsellemeq  14047