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

Theorem eleq12d 2276
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 2275 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq1d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2274 . 2  |-  ( ph  ->  ( A  e.  D  <->  B  e.  D ) )
52, 4bitrd 188 1  |-  ( ph  ->  ( A  e.  C  <->  B  e.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105    = wceq 1373    e. wcel 2176
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187
This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201
This theorem is referenced by:  cbvraldva2  2745  cbvrexdva2  2746  cdeqel  2994  ru  2997  sbceqbid  3005  sbcel12g  3108  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  onintexmid  4621  elvvuni  4739  elrnmpt1  4929  canth  5897  smoeq  6376  smores  6378  smores2  6380  iordsmo  6383  nnaordi  6594  nnaordr  6596  fvixp  6790  cbvixp  6802  mptelixpg  6821  opabfi  7035  exmidaclem  7320  cc1  7377  cc2lem  7378  cc3  7380  ltapig  7451  ltmpig  7452  fzsubel  10182  elfzp1b  10219  ennnfonelemg  12774  ennnfonelemp1  12777  ennnfonelemnn0  12793  ctiunctlemu1st  12805  ctiunctlemu2nd  12806  ctiunctlemudc  12808  ctiunctlemfo  12810  prdsbasprj  13114  xpsfrnel  13176  ismgm  13189  mgm1  13202  issgrpd  13244  ismndd  13269  eqgfval  13558  ringcl  13775  unitinvcl  13885  aprval  14044  aprap  14048  islmodd  14055  rspcl  14253  rnglidlmmgm  14258  zndvds  14411  istps  14504  tpspropd  14508  eltpsg  14512  isms  14925  mspropd  14950  cnlimci  15145
  Copyright terms: Public domain W3C validator