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

Theorem eleq2d 2187
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 2181 . 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 104    = wceq 1316    e. wcel 1465
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113
This theorem is referenced by:  eleq12d  2188  eleqtrd  2196  neleqtrd  2215  neleqtrrd  2216  abeq2d  2230  nfceqdf  2257  drnfc1  2275  drnfc2  2276  sbcbid  2938  cbvcsb  2979  sbcel1g  2992  csbeq2d  2997  csbie2g  3020  cbvralcsf  3032  cbvrexcsf  3033  cbvreucsf  3034  cbvrabcsf  3035  opeq1  3675  opeq2  3676  cbviun  3820  cbviin  3821  iinxsng  3856  iinxprg  3857  iunxsng  3858  iunxsngf  3860  cbvdisj  3886  disjnim  3890  disjiun  3894  mpteq12f  3978  axpweq  4065  rabxfrd  4360  onsucelsucexmid  4415  ordsucunielexmid  4416  0elsucexmid  4450  0nelelxp  4538  opeliunxp  4564  opeliunxp2  4649  iunxpf  4657  elreimasng  4875  elimasng  4877  xpimasn  4957  ressn  5049  funfni  5193  fnbr  5195  fun11iun  5356  fvelrnb  5437  fvun1  5455  fvco2  5458  elfvmptrab1  5483  elfvmptrab  5484  elpreima  5507  dff3im  5533  resflem  5552  fmptco  5554  funfvima3  5619  foima2  5621  eluniimadm  5634  dff13  5637  f1eqcocnv  5660  isoini  5687  riotaeqdv  5699  mpoeq123dva  5800  cbvmpox  5817  ovelrn  5887  elovmpo  5939  fmpox  6066  disjxp1  6101  opeliunxp2f  6103  mpoxopn0yelv  6104  mpoxopovel  6106  rbropapd  6107  rntpos  6122  smoel  6165  smoiso  6167  smoel2  6168  tfrlem9  6184  tfrlemisucaccv  6190  tfrlemiubacc  6195  tfrlemi14d  6198  tfri2d  6201  tfr1onlemubacc  6211  tfr1onlemres  6214  tfrcllemubacc  6224  tfrcllemres  6227  rdgon  6251  freceq1  6257  freceq2  6258  frec0g  6262  frecabcl  6264  freccllem  6267  frecfcllem  6269  frecsuclem  6271  frecsuc  6272  nnsucelsuc  6355  nnsucuniel  6359  nnmordi  6380  ereldm  6440  iinerm  6469  elmapg  6523  elpmg  6526  elixpsn  6597  ixpsnf1o  6598  phplem4  6717  phplem3g  6718  phplem4on  6729  exmidpw  6770  fiintim  6785  fidcenumlemrks  6809  fidcenumlemrk  6810  elfi  6827  ordiso2  6888  ctssdccl  6964  archnqq  7193  ltdfpr  7282  genpelxp  7287  genpelvl  7288  genpelvu  7289  addcanprleml  7390  addcanprlemu  7391  cauappcvgprlem1  7435  suplocexprlemell  7489  suplocexprlemmu  7494  suplocexprlemru  7495  suplocexprlemdisj  7496  suplocexprlemloc  7497  suplocexprlemub  7499  suplocexprlemlub  7500  cnm  7608  eluz1  9286  elixx1  9635  elioo2  9659  elfz1  9750  elfzp1  9807  fzpr  9812  fzsuc2  9814  fzrev3  9822  elfzp12  9834  fzm1  9835  fzoval  9880  elfzo  9881  fzodcel  9884  elfzom1b  9961  fzosplitsni  9967  zmodidfzo  10081  frecuzrdgtcl  10140  frecuzrdgfunlem  10147  bcval  10450  bcpasc  10467  shftfn  10551  shftval  10552  seq3shft  10565  iser3shft  11070  sumeq1  11079  summodclem3  11104  summodclem2a  11105  isumss  11115  fsumsplit  11131  sumsplitdc  11156  fsum2dlemstep  11158  fisumcom2  11162  fsumparts  11194  explecnv  11229  eftlub  11310  divalgmod  11536  algfx  11645  eucalgcvga  11651  ennnfonelemex  11838  ennnfonelemhom  11839  ennnfonelemf1  11842  ennnfonelemrn  11843  ctinfomlemom  11851  ctinfom  11852  ctiunctlemudc  11861  ctiunctlemf  11862  elrest  12038  istopon  12091  eltg  12132  eltg2  12133  eltop  12149  eltop2  12150  eltop3  12151  iscld  12183  neiss2  12222  isnei  12224  lmfval  12272  cnfval  12274  iscn  12277  iscnp  12279  tgcn  12288  tgcnp  12289  lmbrf  12295  cnptopresti  12318  txbas  12338  eltx  12339  txdis  12357  txdis1cn  12358  hmeofvalg  12383  ishmeo  12384  ispsmet  12403  ismet  12424  isxmet  12425  elblps  12470  elbl  12471  elmopn  12526  neibl  12571  metrest  12586  txmetcnp  12598  txmetcn  12599  metcnpd  12600  elcncf  12640  ellimc3apf  12709  limcmpted  12712  cnlimcim  12720  cnlimc  12721  eldvap  12731  dviaddf  12749  dvimulf  12750  bj-sels  13008  nninfalllemn  13098  nninfall  13100  nninfsellemeq  13106
  Copyright terms: Public domain W3C validator