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

Theorem eleq1i 2119
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 2116 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 7 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff set class
Syntax hints:  wb 102   = wceq 1259  wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052
This theorem is referenced by:  eleq12i  2121  eqeltri  2126  intexrabim  3934  abssexg  3961  snnex  4208  pwexb  4233  sucexb  4250  omex  4343  iprc  4627  dfse2  4725  fressnfv  5377  fnotovb  5575  f1stres  5813  f2ndres  5814  ottposg  5900  dftpos4  5908  frecabex  6014  oacl  6070  diffifi  6381  pitonn  6981  axicn  6996  pnfnre  7125  mnfnre  7126  0mnnnnn0  8270  bj-sucexg  10401
  Copyright terms: Public domain W3C validator