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

Theorem abid2 2400
 Description: A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.)
Assertion
Ref Expression
abid2
Distinct variable group:   ,

Proof of Theorem abid2
StepHypRef Expression
1 biid 227 . . 3
21abbi2i 2394 . 2
32eqcomi 2287 1
 Colors of variables: wff set class Syntax hints:   wceq 1623   wcel 1684  cab 2269 This theorem is referenced by:  csbid  3088  csbexg  3091  abss  3242  ssab  3243  abssi  3248  notab  3438  inrab2  3441  dfrab2  3443  dfrab3  3444  notrab  3445  eusn  3703  uniintsn  3899  iunid  3957  orduniss2  4624  imai  5027  dffv4  5522  riotav  6309  cbvriota  6315  riotaund  6341  dfixp  6819  euen1b  6932  modom2  7064  infmap2  7844  ballotlem2  23047  dffv5  24463  mapex2  25140  prismorcsetlemb  25913  aomclem4  27154  rngunsnply  27378  compneOLD  27643  pmapglb  29959  polval2N  30095 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-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279
 Copyright terms: Public domain W3C validator