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

Theorem eleq12d 2208
 Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
Hypotheses
Ref Expression
eleq1d.1
eleq12d.2
Assertion
Ref Expression
eleq12d

Proof of Theorem eleq12d
StepHypRef Expression
1 eleq12d.2 . . 3
21eleq2d 2207 . 2
3 eleq1d.1 . . 3
43eleq1d 2206 . 2
52, 4bitrd 187 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 104   wceq 1331   wcel 1480 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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119 This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133 This theorem is referenced by:  cbvraldva2  2656  cbvrexdva2  2657  cdeqel  2900  ru  2903  sbcel12g  3012  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  onintexmid  4482  elvvuni  4598  elrnmpt1  4785  smoeq  6180  smores  6182  smores2  6184  iordsmo  6187  nnaordi  6397  nnaordr  6399  fvixp  6590  cbvixp  6602  mptelixpg  6621  exmidaclem  7057  ltapig  7139  ltmpig  7140  fzsubel  9833  elfzp1b  9870  ennnfonelemg  11905  ennnfonelemp1  11908  ennnfonelemnn0  11924  ctiunctlemu1st  11936  ctiunctlemu2nd  11937  ctiunctlemudc  11939  ctiunctlemfo  11941  istps  12188  tpspropd  12192  eltpsg  12196  isms  12611  mspropd  12636  cnlimci  12800
 Copyright terms: Public domain W3C validator