MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleq12 Unicode version

Theorem eleq12 2358
Description: Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
Assertion
Ref Expression
eleq12  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  e.  C  <->  B  e.  D ) )

Proof of Theorem eleq12
StepHypRef Expression
1 eleq1 2356 . 2  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
2 eleq2 2357 . 2  |-  ( C  =  D  ->  ( B  e.  C  <->  B  e.  D ) )
31, 2sylan9bb 680 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  e.  C  <->  B  e.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696
This theorem is referenced by:  trel  4136  pwnss  4192  epelg  4322  preleq  7334  oemapval  7401  cantnf  7411  wemapwe  7416  nnsdomel  7639  cldval  16776  isufil  17614  issiga  23487  wepwsolem  27241  aomclem8  27262
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator