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

Theorem eleq1i 2206
 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 2203 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶𝐵𝐶)
 Colors of variables: wff set class Syntax hints:   ↔ wb 104   = wceq 1332   ∈ 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:  eleq12i  2208  eqeltri  2213  intexrabim  4082  abssexg  4110  abnex  4372  snnex  4373  pwexb  4399  sucexb  4417  omex  4511  iprc  4811  dfse2  4916  fressnfv  5611  fnotovb  5818  f1stres  6061  f2ndres  6062  ottposg  6156  dftpos4  6164  frecabex  6299  oacl  6360  diffifi  6792  djuexb  6933  pitonn  7676  axicn  7691  pnfnre  7827  mnfnre  7828  0mnnnnn0  9029  nprmi  11832  txdis1cn  12477  xmeterval  12634  expcncf  12791  bj-sucexg  13274
 Copyright terms: Public domain W3C validator