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
eleq12i.2
Assertion
Ref Expression
eleq12i

Proof of Theorem eleq12i
StepHypRef Expression
1 eleq12i.2 . . 3
21eleq2i 2360 . 2
3 eleq1i.1 . . 3
43eleq1i 2359 . 2
52, 4bitri 240 1
 Colors of variables: wff set class Syntax hints:   wb 176   wceq 1632   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