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

Theorem eleq12i 2361
Description: Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
Hypotheses
Ref Expression
eleq1i.1  |-  A  =  B
eleq12i.2  |-  C  =  D
Assertion
Ref Expression
eleq12i  |-  ( A  e.  C  <->  B  e.  D )

Proof of Theorem eleq12i
StepHypRef Expression
1 eleq12i.2 . . 3  |-  C  =  D
21eleq2i 2360 . 2  |-  ( A  e.  C  <->  A  e.  D )
3 eleq1i.1 . . 3  |-  A  =  B
43eleq1i 2359 . 2  |-  ( A  e.  D  <->  B  e.  D )
52, 4bitri 240 1  |-  ( A  e.  C  <->  B  e.  D )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1632    e. wcel 1696
This theorem is referenced by:  3eltr3g  2378  3eltr4g  2379  sbcel12g  3109  rankelun  7560  rankelpr  7561  rankelop  7562  isf34lem7  8021  0r  8718  1sr  8719  m1r  8720  cxpcn3  20104  bposlem4  20542  xrge0mulc1cn  23338  brsigarn  23530  geme2  25378  phckle  26130  psckle  26131  fnckle  26148  mapfzcons  26896  bnj98  29215
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