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

Theorem eleq12 2543
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 2539 . 2  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
2 eleq2 2540 . 2  |-  ( C  =  D  ->  ( B  e.  C  <->  B  e.  D ) )
31, 2sylan9bb 699 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  e.  C  <->  B  e.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379    e. wcel 1767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462
This theorem is referenced by:  trel  4547  pwnss  4612  epelg  4792  preleq  8030  oemapval  8098  cantnf  8108  cantnfOLD  8130  wemapwe  8135  wemapweOLD  8136  nnsdomel  8367  cldval  19290  isufil  20139  issiga  27751  wepwsolem  30591  aomclem8  30611
  Copyright terms: Public domain W3C validator