ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  abid2 Unicode version

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

Proof of Theorem abid2
StepHypRef Expression
1 biid 169 . . 3  |-  ( x  e.  A  <->  x  e.  A )
21abbi2i 2194 . 2  |-  A  =  { x  |  x  e.  A }
32eqcomi 2086 1  |-  { x  |  x  e.  A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1285    e. wcel 1434   {cab 2068
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078
This theorem is referenced by:  csbid  2916  abss  3064  ssab  3065  abssi  3070  notab  3241  inrab2  3244  dfrab2  3246  dfrab3  3247  notrab  3248  eusn  3474  dfopg  3576  iunid  3741  csbexga  3914  imai  4711  dffv4g  5206  frec0g  6046  euen1b  6350
  Copyright terms: Public domain W3C validator