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

Theorem eleq2d 2154
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)
Hypothesis
Ref Expression
eleq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
eleq2d (𝜑 → (𝐶𝐴𝐶𝐵))

Proof of Theorem eleq2d
StepHypRef Expression
1 eleq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 eleq2 2148 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1287  wcel 1436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081
This theorem is referenced by:  eleq12d  2155  eleqtrd  2163  neleqtrd  2182  neleqtrrd  2183  abeq2d  2197  nfceqdf  2224  drnfc1  2241  drnfc2  2242  sbcbid  2885  cbvcsb  2926  sbcel1g  2939  csbeq2d  2944  csbie2g  2967  cbvralcsf  2979  cbvrexcsf  2980  cbvreucsf  2981  cbvrabcsf  2982  opeq1  3605  opeq2  3606  cbviun  3750  cbviin  3751  iinxsng  3786  iinxprg  3787  iunxsng  3788  cbvdisj  3811  mpteq12f  3893  axpweq  3981  rabxfrd  4265  onsucelsucexmid  4319  ordsucunielexmid  4320  0elsucexmid  4354  0nelelxp  4439  opeliunxp  4461  opeliunxp2  4544  iunxpf  4552  elreimasng  4765  elimasng  4767  xpimasn  4845  ressn  4937  funfni  5079  fnbr  5081  fun11iun  5237  fvelrnb  5315  fvun1  5333  fvco2  5336  elpreima  5381  dff3im  5407  resflem  5425  fmptco  5427  funfvima3  5489  foima2  5491  eluniimadm  5505  dff13  5508  f1eqcocnv  5531  isoini  5558  riotaeqdv  5570  mpt2eq123dva  5667  cbvmpt2x  5683  ovelrn  5750  elovmpt2  5802  fmpt2x  5927  mpt2xopn0yelv  5958  mpt2xopovel  5960  isprmpt2  5962  rntpos  5976  smoel  6019  smoiso  6021  smoel2  6022  tfrlem9  6038  tfrlemisucaccv  6044  tfrlemiubacc  6049  tfrlemi14d  6052  tfri2d  6055  tfr1onlemubacc  6065  tfr1onlemres  6068  tfrcllemubacc  6078  tfrcllemres  6081  rdgon  6105  freceq1  6111  freceq2  6112  frec0g  6116  frecabcl  6118  freccllem  6121  frecfcllem  6123  frecsuclem  6125  frecsuc  6126  nnsucelsuc  6206  nnsucuniel  6210  nnmordi  6227  ereldm  6287  iinerm  6316  elmapg  6370  elpmg  6373  phplem4  6523  phplem3g  6524  phplem4on  6535  exmidpw  6576  ordiso2  6672  archnqq  6920  ltdfpr  7009  genpelxp  7014  genpelvl  7015  genpelvu  7016  addcanprleml  7117  addcanprlemu  7118  cauappcvgprlem1  7162  eluz1  8955  elixx1  9247  elioo2  9271  elfz1  9361  elfzp1  9416  fzpr  9421  fzsuc2  9423  fzrev3  9431  elfzp12  9443  fzm1  9444  fzoval  9487  elfzo  9488  fzodcel  9491  elfzom1b  9568  fzosplitsni  9574  zmodidfzo  9688  frecuzrdgtcl  9747  frecuzrdgfunlem  9754  bcval  10053  bcpasc  10070  shftfn  10154  shftval  10155  sumeq1  10634  isummolem3  10659  isummolem2a  10660  isumss  10669  divalgmod  10802  ialgfx  10909  eucialgcvga  10915  bj-sels  11243  nninfalllemn  11336  nninfall  11338  nninfsellemeq  11344
  Copyright terms: Public domain W3C validator