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

Theorem eleq2d 2210
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 2204 . 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 1332    e. wcel 1481
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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136
This theorem is referenced by:  eleq12d  2211  eleqtrd  2219  neleqtrd  2238  neleqtrrd  2239  abeq2d  2253  nfceqdf  2281  drnfc1  2299  drnfc2  2300  sbcbid  2969  cbvcsbw  3010  cbvcsb  3011  sbcel1g  3025  csbeq2d  3031  csbie2g  3054  cbvralcsf  3066  cbvrexcsf  3067  cbvreucsf  3068  cbvrabcsf  3069  opeq1  3712  opeq2  3713  cbviun  3857  cbviin  3858  iinxsng  3893  iinxprg  3894  iunxsng  3895  iunxsngf  3897  cbvdisj  3923  disjnim  3927  disjiun  3931  mpteq12f  4015  axpweq  4102  rabxfrd  4397  onsucelsucexmid  4452  ordsucunielexmid  4453  0elsucexmid  4487  0nelelxp  4575  opeliunxp  4601  opeliunxp2  4686  iunxpf  4694  elreimasng  4912  elimasng  4914  xpimasn  4994  ressn  5086  funfni  5230  fnbr  5232  fun11iun  5395  fvelrnb  5476  fvun1  5494  fvco2  5497  elfvmptrab1  5522  elfvmptrab  5523  elpreima  5546  dff3im  5572  resflem  5591  fmptco  5593  funfvima3  5658  foima2  5660  eluniimadm  5673  dff13  5676  f1eqcocnv  5699  isoini  5726  riotaeqdv  5738  mpoeq123dva  5839  cbvmpox  5856  ovelrn  5926  elovmpo  5978  fmpox  6105  disjxp1  6140  opeliunxp2f  6142  mpoxopn0yelv  6143  mpoxopovel  6145  rbropapd  6146  rntpos  6161  smoel  6204  smoiso  6206  smoel2  6207  tfrlem9  6223  tfrlemisucaccv  6229  tfrlemiubacc  6234  tfrlemi14d  6237  tfri2d  6240  tfr1onlemubacc  6250  tfr1onlemres  6253  tfrcllemubacc  6263  tfrcllemres  6266  rdgon  6290  freceq1  6296  freceq2  6297  frec0g  6301  frecabcl  6303  freccllem  6306  frecfcllem  6308  frecsuclem  6310  frecsuc  6311  nnsucelsuc  6394  nnsucuniel  6398  nnmordi  6419  ereldm  6479  iinerm  6508  elmapg  6562  elpmg  6565  elixpsn  6636  ixpsnf1o  6637  phplem4  6756  phplem3g  6757  phplem4on  6768  exmidpw  6809  fiintim  6824  fidcenumlemrks  6848  fidcenumlemrk  6849  elfi  6866  ordiso2  6927  ctssdccl  7003  cc2lem  7097  cc2  7098  cc3  7099  archnqq  7248  ltdfpr  7337  genpelxp  7342  genpelvl  7343  genpelvu  7344  addcanprleml  7445  addcanprlemu  7446  cauappcvgprlem1  7490  suplocexprlemell  7544  suplocexprlemmu  7549  suplocexprlemru  7550  suplocexprlemdisj  7551  suplocexprlemloc  7552  suplocexprlemub  7554  suplocexprlemlub  7555  cnm  7663  eluz1  9353  elixx1  9709  elioo2  9733  elfz1  9825  elfzp1  9882  fzpr  9887  fzsuc2  9889  fzrev3  9897  elfzp12  9909  fzm1  9910  fzoval  9955  elfzo  9956  fzodcel  9959  elfzom1b  10036  fzosplitsni  10042  zmodidfzo  10156  frecuzrdgtcl  10215  frecuzrdgfunlem  10222  bcval  10526  bcpasc  10543  shftfn  10627  shftval  10628  seq3shft  10641  iser3shft  11146  sumeq1  11155  summodclem3  11180  summodclem2a  11181  isumss  11191  fsumsplit  11207  sumsplitdc  11232  fsum2dlemstep  11234  fisumcom2  11238  fsumparts  11270  explecnv  11305  eftlub  11431  divalgmod  11658  algfx  11767  eucalgcvga  11773  ennnfonelemex  11961  ennnfonelemhom  11962  ennnfonelemf1  11965  ennnfonelemrn  11966  ctinfomlemom  11974  ctinfom  11975  ctiunctlemudc  11984  ctiunctlemf  11985  elrest  12164  istopon  12217  eltg  12258  eltg2  12259  eltop  12275  eltop2  12276  eltop3  12277  iscld  12309  neiss2  12348  isnei  12350  lmfval  12398  cnfval  12400  iscn  12403  iscnp  12405  tgcn  12414  tgcnp  12415  lmbrf  12421  cnptopresti  12444  txbas  12464  eltx  12465  txdis  12483  txdis1cn  12484  hmeofvalg  12509  ishmeo  12510  ispsmet  12529  ismet  12550  isxmet  12551  elblps  12596  elbl  12597  elmopn  12652  neibl  12697  metrest  12712  txmetcnp  12724  txmetcn  12725  metcnpd  12726  elcncf  12766  ellimc3apf  12835  limcmpted  12838  cnlimcim  12846  cnlimc  12847  eldvap  12857  dviaddf  12875  dvimulf  12876  bj-sels  13281  nninfalllemn  13375  nninfall  13377  nninfsellemeq  13383
  Copyright terms: Public domain W3C validator