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

Theorem eleq1i 2150
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 2147 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 7 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff set class
Syntax hints:  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:  eleq12i  2152  eqeltri  2157  intexrabim  3964  abssexg  3991  snnex  4245  pwexb  4270  sucexb  4287  omex  4381  iprc  4669  dfse2  4772  fressnfv  5447  fnotovb  5649  f1stres  5887  f2ndres  5888  ottposg  5974  dftpos4  5982  frecabex  6117  oacl  6175  diffifi  6562  pitonn  7329  axicn  7344  pnfnre  7473  mnfnre  7474  0mnnnnn0  8638  nprmi  10981  bj-sucexg  11251
  Copyright terms: Public domain W3C validator