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

Theorem eleq2d 2149
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 2143 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1285  wcel 1434
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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078
This theorem is referenced by:  eleq12d  2150  eleqtrd  2158  neleqtrd  2177  neleqtrrd  2178  abeq2d  2192  nfceqdf  2219  drnfc1  2236  drnfc2  2237  sbcbid  2872  cbvcsb  2913  sbcel1g  2926  csbeq2d  2931  csbie2g  2953  cbvralcsf  2965  cbvrexcsf  2966  cbvreucsf  2967  cbvrabcsf  2968  opeq1  3572  opeq2  3573  cbviun  3717  cbviin  3718  iinxsng  3753  iinxprg  3754  iunxsng  3755  cbvdisj  3778  mpteq12f  3860  axpweq  3947  rabxfrd  4221  onsucelsucexmid  4275  ordsucunielexmid  4276  0elsucexmid  4310  0nelelxp  4393  opeliunxp  4415  opeliunxp2  4498  iunxpf  4506  elreimasng  4715  elimasng  4717  xpimasn  4793  ressn  4882  funfni  5024  fnbr  5026  fun11iun  5172  fvelrnb  5247  fvun1  5265  fvco2  5268  elpreima  5312  dff3im  5338  fmptco  5356  funfvima3  5418  eluniimadm  5430  dff13  5433  f1eqcocnv  5456  isoini  5482  riotaeqdv  5494  mpt2eq123dva  5591  cbvmpt2x  5607  ovelrn  5674  elovmpt2  5726  fmpt2x  5851  mpt2xopn0yelv  5882  mpt2xopovel  5884  isprmpt2  5886  rntpos  5900  smoel  5943  smoiso  5945  smoel2  5946  tfrlem9  5962  tfrlemisucaccv  5968  tfrlemiubacc  5973  tfrlemi14d  5976  tfri2d  5979  tfr1onlemubacc  5989  tfr1onlemres  5992  tfrcllemubacc  6002  tfrcllemres  6005  rdgon  6029  freceq1  6035  freceq2  6036  frec0g  6040  frecabcl  6042  freccllem  6045  frecfcllem  6047  frecsuclem  6049  frecsuc  6050  nnsucelsuc  6128  nnsucuniel  6132  nnmordi  6148  ereldm  6208  iinerm  6237  phplem4  6380  phplem3g  6381  phplem4on  6392  ordiso2  6495  archnqq  6658  ltdfpr  6747  genpelxp  6752  genpelvl  6753  genpelvu  6754  addcanprleml  6855  addcanprlemu  6856  cauappcvgprlem1  6900  eluz1  8693  elixx1  8985  elioo2  9009  elfz1  9099  elfzp1  9154  fzpr  9159  fzsuc2  9161  fzrev3  9169  elfzp12  9181  fzm1  9182  fzoval  9224  elfzo  9225  elfzom1b  9304  fzosplitsni  9310  zmodidfzo  9424  frecuzrdgtcl  9483  frecuzrdgfunlem  9490  bcval  9762  bcpasc  9779  shftfn  9839  shftval  9840  sumeq1  10319  divalgmod  10460  ialgfx  10567  eucialgcvga  10573  bj-sels  10848
  Copyright terms: Public domain W3C validator