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

Theorem eleq12 2480
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 2476 . 2  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
2 eleq2 2477 . 2  |-  ( C  =  D  ->  ( B  e.  C  <->  B  e.  D ) )
31, 2sylan9bb 700 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  e.  C  <->  B  e.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186    /\ wa 369    = wceq 1407    e. wcel 1844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-ex 1636  df-cleq 2396  df-clel 2399
This theorem is referenced by:  trel  4498  pwnss  4561  epelg  4737  preleq  8069  oemapval  8136  cantnf  8146  cantnfOLD  8168  wemapwe  8173  wemapweOLD  8174  nnsdomel  8405  cldval  19818  isufil  20698  issiga  28572  wepwsolem  35362  aomclem8  35382
  Copyright terms: Public domain W3C validator