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

Theorem eleq12d 2158
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 2157 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq1d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2156 . 2  |-  ( ph  ->  ( A  e.  D  <->  B  e.  D ) )
52, 4bitrd 186 1  |-  ( ph  ->  ( A  e.  C  <->  B  e.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    = wceq 1289    e. wcel 1438
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084
This theorem is referenced by:  cbvraldva2  2594  cbvrexdva2  2595  cdeqel  2836  ru  2839  sbcel12g  2946  cbvralcsf  2990  cbvrexcsf  2991  cbvreucsf  2992  cbvrabcsf  2993  onintexmid  4386  elvvuni  4498  elrnmpt1  4682  smoeq  6047  smores  6049  smores2  6051  iordsmo  6054  nnaordi  6257  nnaordr  6259  ltapig  6887  ltmpig  6888  fzsubel  9463  elfzp1b  9499
  Copyright terms: Public domain W3C validator