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

Theorem eleq12d 2248
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 2247 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq1d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2246 . 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 1353    e. wcel 2148
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173
This theorem is referenced by:  cbvraldva2  2710  cbvrexdva2  2711  cdeqel  2958  ru  2961  sbceqbid  2969  sbcel12g  3072  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  onintexmid  4572  elvvuni  4690  elrnmpt1  4878  canth  5828  smoeq  6290  smores  6292  smores2  6294  iordsmo  6297  nnaordi  6508  nnaordr  6510  fvixp  6702  cbvixp  6714  mptelixpg  6733  exmidaclem  7206  cc1  7263  cc2lem  7264  cc3  7266  ltapig  7336  ltmpig  7337  fzsubel  10057  elfzp1b  10094  ennnfonelemg  12398  ennnfonelemp1  12401  ennnfonelemnn0  12417  ctiunctlemu1st  12429  ctiunctlemu2nd  12430  ctiunctlemudc  12432  ctiunctlemfo  12434  ismgm  12730  mgm1  12743  ismndd  12792  eqgfval  13034  ringcl  13149  unitinvcl  13245  aprval  13293  aprap  13297  istps  13423  tpspropd  13427  eltpsg  13431  isms  13846  mspropd  13871  cnlimci  14035
  Copyright terms: Public domain W3C validator