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  3763  opeq2  3764  cbviun  3908  cbviin  3909  iinxsng  3944  iinxprg  3945  iunxsng  3946  iunxsngf  3948  cbvdisj  3974  disjnim  3978  disjiun  3982  mpteq12f  4067  axpweq  4155  rabxfrd  4452  onsucelsucexmid  4512  ordsucunielexmid  4513  0elsucexmid  4547  0nelelxp  4638  opeliunxp  4664  opeliunxp2  4749  iunxpf  4757  elreimasng  4975  elimasng  4977  xpimasn  5057  ressn  5149  funfni  5296  fnbr  5298  fun11iun  5461  fvelrnb  5542  fvun1  5560  fvco2  5563  elfvmptrab1  5588  elfvmptrab  5589  elpreima  5612  dff3im  5638  resflem  5657  fmptco  5659  funfvima3  5726  foima2  5728  eluniimadm  5741  dff13  5744  f1eqcocnv  5767  isoini  5794  riotaeqdv  5807  mpoeq123dva  5911  cbvmpox  5928  ovelrn  5998  elovmpo  6047  fmpox  6176  disjxp1  6212  opeliunxp2f  6214  mpoxopn0yelv  6215  mpoxopovel  6217  rbropapd  6218  rntpos  6233  smoel  6276  smoiso  6278  smoel2  6279  tfrlem9  6295  tfrlemisucaccv  6301  tfrlemiubacc  6306  tfrlemi14d  6309  tfri2d  6312  tfr1onlemubacc  6322  tfr1onlemres  6325  tfrcllemubacc  6335  tfrcllemres  6338  rdgon  6362  freceq1  6368  freceq2  6369  frec0g  6373  frecabcl  6375  freccllem  6378  frecfcllem  6380  frecsuclem  6382  frecsuc  6383  nnsucelsuc  6467  nnsucuniel  6471  nnmordi  6492  ereldm  6552  iinerm  6581  elmapg  6635  elpmg  6638  elixpsn  6709  ixpsnf1o  6710  phplem4  6829  phplem3g  6830  phplem4on  6841  exmidpw  6882  fiintim  6902  fidcenumlemrks  6926  fidcenumlemrk  6927  elfi  6944  ordiso2  7008  ctssdccl  7084  nnnninfeq  7100  cc2lem  7215  cc2  7216  cc3  7217  archnqq  7366  ltdfpr  7455  genpelxp  7460  genpelvl  7461  genpelvu  7462  addcanprleml  7563  addcanprlemu  7564  cauappcvgprlem1  7608  suplocexprlemell  7662  suplocexprlemmu  7667  suplocexprlemru  7668  suplocexprlemdisj  7669  suplocexprlemloc  7670  suplocexprlemub  7672  suplocexprlemlub  7673  cnm  7781  eluz1  9478  elixx1  9841  elioo2  9865  elfz1  9957  elfzp1  10015  fzpr  10020  fzsuc2  10022  fzrev3  10030  elfzp12  10042  fzm1  10043  fzoval  10091  elfzo  10092  fzodcel  10095  elfzom1b  10172  fzosplitsni  10178  zmodidfzo  10296  frecuzrdgtcl  10355  frecuzrdgfunlem  10362  bcval  10670  bcpasc  10687  shftfn  10775  shftval  10776  seq3shft  10789  iser3shft  11296  sumeq1  11305  summodclem3  11330  summodclem2a  11331  isumss  11341  fsumsplit  11357  sumsplitdc  11382  fsum2dlemstep  11384  fisumcom2  11388  fsumparts  11420  explecnv  11455  fprodsplitdc  11546  fprodsplit  11547  fprod2dlemstep  11572  fprodcom2fi  11576  eftlub  11640  divalgmod  11873  nninfdcex  11895  algfx  11993  eucalgcvga  11999  reumodprminv  12194  nnnn0modprm0  12196  ennnfonelemex  12356  ennnfonelemhom  12357  ennnfonelemf1  12360  ennnfonelemrn  12361  ctinfomlemom  12369  ctinfom  12370  ctiunctlemudc  12379  ctiunctlemf  12380  elrest  12573  grpidvalg  12614  grpidpropdg  12615  grpidd  12624  ismndd  12660  mndpropd  12663  ismhm  12672  issubm  12682  istopon  12764  eltg  12805  eltg2  12806  eltop  12822  eltop2  12823  eltop3  12824  iscld  12856  neiss2  12895  isnei  12897  lmfval  12945  cnfval  12947  iscn  12950  iscnp  12952  tgcn  12961  tgcnp  12962  lmbrf  12968  cnptopresti  12991  txbas  13011  eltx  13012  txdis  13030  txdis1cn  13031  hmeofvalg  13056  ishmeo  13057  ispsmet  13076  ismet  13097  isxmet  13098  elblps  13143  elbl  13144  elmopn  13199  neibl  13244  metrest  13259  txmetcnp  13271  txmetcn  13272  metcnpd  13273  elcncf  13313  ellimc3apf  13382  limcmpted  13385  cnlimcim  13393  cnlimc  13394  eldvap  13404  dviaddf  13422  dvimulf  13423  bj-sels  13909  nninfall  14002  nninfsellemeq  14007