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

Theorem eleq12 2450
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 2448 . 2  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
2 eleq2 2449 . 2  |-  ( C  =  D  ->  ( B  e.  C  <->  B  e.  D ) )
31, 2sylan9bb 681 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  e.  C  <->  B  e.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717
This theorem is referenced by:  trel  4251  pwnss  4307  epelg  4437  preleq  7506  oemapval  7573  cantnf  7583  wemapwe  7588  nnsdomel  7811  cldval  17011  isufil  17857  issiga  24291  wepwsolem  26808  aomclem8  26829
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2381  df-clel 2384
  Copyright terms: Public domain W3C validator