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

Theorem eleq1i 2178
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 2175 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 7 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff set class
Syntax hints:  wb 104   = wceq 1312  wcel 1461
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-17 1487  ax-ial 1495  ax-ext 2095
This theorem depends on definitions:  df-bi 116  df-cleq 2106  df-clel 2109
This theorem is referenced by:  eleq12i  2180  eqeltri  2185  intexrabim  4036  abssexg  4064  abnex  4326  snnex  4327  pwexb  4353  sucexb  4371  omex  4465  iprc  4763  dfse2  4868  fressnfv  5559  fnotovb  5766  f1stres  6008  f2ndres  6009  ottposg  6103  dftpos4  6111  frecabex  6246  oacl  6307  diffifi  6738  djuexb  6878  pitonn  7576  axicn  7591  pnfnre  7724  mnfnre  7725  0mnnnnn0  8906  nprmi  11644  txdis1cn  12282  xmeterval  12417  expcncf  12571  bj-sucexg  12799
  Copyright terms: Public domain W3C validator