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

Theorem abid2 2233
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 170 . . 3 (𝑥𝐴𝑥𝐴)
21abbi2i 2227 . 2 𝐴 = {𝑥𝑥𝐴}
32eqcomi 2117 1 {𝑥𝑥𝐴} = 𝐴
Colors of variables: wff set class
Syntax hints:   = wceq 1312  wcel 1461  {cab 2099
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095
This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109
This theorem is referenced by:  csbid  2976  abss  3130  ssab  3131  abssi  3136  notab  3310  inrab2  3313  dfrab2  3315  dfrab3  3316  notrab  3317  eusn  3561  dfopg  3667  iunid  3832  csbexga  4014  imai  4851  dffv4g  5370  frec0g  6245  dfixp  6545  euen1b  6648  acfun  7007
  Copyright terms: Public domain W3C validator