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

Theorem eleq1i 2183
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 2180 . 2  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
31, 2ax-mp 5 1  |-  ( A  e.  C  <->  B  e.  C )
Colors of variables: wff set class
Syntax hints:    <-> wb 104    = wceq 1316    e. wcel 1465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113
This theorem is referenced by:  eleq12i  2185  eqeltri  2190  intexrabim  4048  abssexg  4076  abnex  4338  snnex  4339  pwexb  4365  sucexb  4383  omex  4477  iprc  4777  dfse2  4882  fressnfv  5575  fnotovb  5782  f1stres  6025  f2ndres  6026  ottposg  6120  dftpos4  6128  frecabex  6263  oacl  6324  diffifi  6756  djuexb  6897  pitonn  7624  axicn  7639  pnfnre  7775  mnfnre  7776  0mnnnnn0  8977  nprmi  11732  txdis1cn  12374  xmeterval  12531  expcncf  12688  bj-sucexg  13047
  Copyright terms: Public domain W3C validator