ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eleq2d Unicode version

Theorem eleq2d 2123
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
StepHypRef Expression
1 eleq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 eleq2 2117 . 2  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
31, 2syl 14 1  |-  ( ph  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102    = wceq 1259    e. wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052
This theorem is referenced by:  eleq12d  2124  eleqtrd  2132  neleqtrd  2151  neleqtrrd  2152  abeq2d  2166  nfceqdf  2193  drnfc1  2210  drnfc2  2211  sbcbid  2842  cbvcsb  2883  sbcel1g  2896  csbeq2d  2901  csbie2g  2923  cbvralcsf  2935  cbvrexcsf  2936  cbvreucsf  2937  cbvrabcsf  2938  opeq1  3576  opeq2  3577  cbviun  3721  cbviin  3722  iinxsng  3757  iinxprg  3758  iunxsng  3759  cbvdisj  3782  mpteq12f  3864  axpweq  3951  rabxfrd  4228  onsucelsucexmid  4282  ordsucunielexmid  4283  0elsucexmid  4316  0nelelxp  4400  opeliunxp  4422  opeliunxp2  4503  iunxpf  4511  elreimasng  4718  elimasng  4720  xpimasn  4796  ressn  4885  funfni  5026  fnbr  5028  fun11iun  5174  fvelrnb  5248  fvun1  5266  fvco2  5269  elpreima  5313  dff3im  5339  fmptco  5357  funfvima3  5419  eluniimadm  5431  dff13  5434  f1eqcocnv  5458  isoini  5484  riotaeqdv  5496  mpt2eq123dva  5593  cbvmpt2x  5609  ovelrn  5676  elovmpt2  5728  fmpt2x  5853  mpt2xopn0yelv  5884  mpt2xopovel  5886  isprmpt2  5888  rntpos  5902  smoel  5945  smoiso  5947  smoel2  5948  tfrlem9  5965  tfrlemisucaccv  5969  tfrlemiubacc  5974  tfrlemi14d  5977  tfri2d  5980  freceq1  6009  freceq2  6010  frec0g  6013  frecsuclem3  6020  frecsuc  6021  nnsucelsuc  6100  nnmordi  6119  ereldm  6179  iinerm  6208  phplem4  6348  phplem3g  6349  phplem4on  6359  ordiso2  6414  archnqq  6572  ltdfpr  6661  genpelxp  6666  genpelvl  6667  genpelvu  6668  addcanprleml  6769  addcanprlemu  6770  cauappcvgprlem1  6814  eluz1  8572  elixx1  8866  elioo2  8890  elfz1  8980  elfzp1  9035  fzpr  9040  fzsuc2  9042  fzrev3  9050  elfzp12  9062  fzm1  9063  fzoval  9106  elfzo  9107  elfzom1b  9186  fzosplitsni  9192  zmodidfzo  9297  frecuzrdgfn  9356  bcval  9610  bcpasc  9627  shftfn  9646  shftval  9647  sumeq1  10097  ialgfx  10246  bj-sels  10393
  Copyright terms: Public domain W3C validator