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

Theorem eleq1i 2180
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  e.  C  <->  B  e.  C )

Proof of Theorem eleq1i
StepHypRef Expression
1 eleq1i.1 . 2  |-  A  =  B
2 eleq1 2177 . 2  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
31, 2ax-mp 7 1  |-  ( A  e.  C  <->  B  e.  C )
Colors of variables: wff set class
Syntax hints:    <-> wb 104    = wceq 1314    e. wcel 1463
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111
This theorem is referenced by:  eleq12i  2182  eqeltri  2187  intexrabim  4038  abssexg  4066  abnex  4328  snnex  4329  pwexb  4355  sucexb  4373  omex  4467  iprc  4765  dfse2  4870  fressnfv  5561  fnotovb  5768  f1stres  6011  f2ndres  6012  ottposg  6106  dftpos4  6114  frecabex  6249  oacl  6310  diffifi  6741  djuexb  6881  pitonn  7583  axicn  7598  pnfnre  7731  mnfnre  7732  0mnnnnn0  8913  nprmi  11651  txdis1cn  12289  xmeterval  12424  expcncf  12578  bj-sucexg  12812
  Copyright terms: Public domain W3C validator