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

Theorem eleq1i 2103
 Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eleq1i.1
Assertion
Ref Expression
eleq1i

Proof of Theorem eleq1i
StepHypRef Expression
1 eleq1i.1 . 2
2 eleq1 2100 . 2
31, 2ax-mp 7 1
 Colors of variables: wff set class Syntax hints:   wb 98   wceq 1243   wcel 1393 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036 This theorem is referenced by:  eleq12i  2105  eqeltri  2110  intexrabim  3907  abssexg  3934  snnex  4181  pwexb  4206  sucexb  4223  omex  4316  iprc  4600  dfse2  4698  fressnfv  5350  fnotovb  5548  f1stres  5786  f2ndres  5787  ottposg  5870  dftpos4  5878  frecabex  5984  oacl  6040  diffifi  6351  pitonn  6924  axicn  6939  pnfnre  7067  mnfnre  7068  0mnnnnn0  8214  bj-sucexg  10042
 Copyright terms: Public domain W3C validator