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

Theorem abid2 2597
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 236 . . 3
21abbi2i 2590 . 2
32eqcomi 2470 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  e.wcel 1818  {cab 2442
This theorem is referenced by:  csbid  3442  abss  3568  ssab  3569  abssi  3574  notab  3767  inrab2  3770  dfrab3  3772  notrab  3774  eusn  4106  uniintsn  4324  iunid  4385  csbexg  4584  csbexgOLD  4586  imai  5354  dffv4  5868  orduniss2  6668  dfixp  7491  euen1b  7606  modom2  7741  infmap2  8619  cshwsexa  12792  ustfn  20704  ustn0  20723  fpwrelmap  27556  eulerpartlemgvv  28315  ballotlem2  28427  dffv5  29574  ptrest  30048  cnambfre  30063  aomclem4  31003  rngunsnply  31122  iocinico  31179  riotaclbgBAD  34685  pmapglb  35494  polval2N  35630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452
  Copyright terms: Public domain W3C validator