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

Theorem abid2 2236
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 170 . . 3  |-  ( x  e.  A  <->  x  e.  A )
21abbi2i 2230 . 2  |-  A  =  { x  |  x  e.  A }
32eqcomi 2119 1  |-  { x  |  x  e.  A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1314    e. wcel 1463   {cab 2101
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111
This theorem is referenced by:  csbid  2980  abss  3134  ssab  3135  abssi  3140  notab  3314  inrab2  3317  dfrab2  3319  dfrab3  3320  notrab  3321  eusn  3565  dfopg  3671  iunid  3836  csbexga  4024  imai  4863  dffv4g  5384  frec0g  6260  dfixp  6560  euen1b  6663  acfun  7027  ccfunen  7043
  Copyright terms: Public domain W3C validator