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

Theorem eleq12d 2124
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
Hypotheses
Ref Expression
eleq1d.1  |-  ( ph  ->  A  =  B )
eleq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
eleq12d  |-  ( ph  ->  ( A  e.  C  <->  B  e.  D ) )

Proof of Theorem eleq12d
StepHypRef Expression
1 eleq12d.2 . . 3  |-  ( ph  ->  C  =  D )
21eleq2d 2123 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq1d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2122 . 2  |-  ( ph  ->  ( A  e.  D  <->  B  e.  D ) )
52, 4bitrd 181 1  |-  ( ph  ->  ( A  e.  C  <->  B  e.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102    = wceq 1259    e. 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:  cbvraldva2  2554  cbvrexdva2  2555  cdeqel  2783  ru  2786  sbcel12g  2893  cbvralcsf  2936  cbvrexcsf  2937  cbvreucsf  2938  cbvrabcsf  2939  onintexmid  4325  elvvuni  4432  elrnmpt1  4613  smoeq  5936  smores  5938  smores2  5940  iordsmo  5943  nnaordi  6112  nnaordr  6114  ltapig  6494  ltmpig  6495  fzsubel  9025  elfzp1b  9061
  Copyright terms: Public domain W3C validator