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

Theorem eleq12i 2348
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 2347 . 2  |-  ( A  e.  C  <->  A  e.  D )
3 eleq1i.1 . . 3  |-  A  =  B
43eleq1i 2346 . 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 1623    e. wcel 1684
This theorem is referenced by:  3eltr3g  2365  3eltr4g  2366  sbcel12g  3096  rankelun  7544  rankelpr  7545  rankelop  7546  isf34lem7  8005  0r  8702  1sr  8703  m1r  8704  cxpcn3  20088  bposlem4  20526  xrge0mulc1cn  23323  brsigarn  23515  geme2  25275  phckle  26027  psckle  26028  fnckle  26045  mapfzcons  26793  bnj98  28899
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator