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

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

Proof of Theorem eleq1i
StepHypRef Expression
1 eleq1i.1 . 2 A = B
2 eleq1 2082 . 2 (A = B → (A 𝐶B 𝐶))
31, 2ax-mp 7 1 (A 𝐶B 𝐶)
Colors of variables: wff set class
Syntax hints:  wb 98   = wceq 1228   wcel 1374
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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015  df-clel 2018
This theorem is referenced by:  eleq12i  2087  eqeltri  2092  intexrabim  3881  abssexg  3908  snnex  4131  pwexb  4156  sucexb  4173  omex  4243  iprc  4527  dfse2  4625  fressnfv  5275  fnotovb  5471  f1stres  5709  f2ndres  5710  ottposg  5792  dftpos4  5800  frecabex  5899  frec0g  5902  oacl  5955  axicn  6559  pnfnre  6668  mnfnre  6669  bj-sucexg  7145
  Copyright terms: Public domain W3C validator