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

Definition df-pw 3978
Description: Define power class. Definition 5.10 of [TakeutiZaring] p. 17, but we also let it apply to proper classes, i.e. those that are not members of . When applied to a set, this produces its power set. A power set of S is the set of all subsets of S, including the empty set and S itself. For example, if , then ~PA={ ,{3},{5},{7},{3,5}, {3,7},{5,7},{3,5,7}} (ex-pw 24105). We will later introduce the Axiom of Power Sets ax-pow 4587, which can be expressed in class notation per pwexg 4593. Still later we will prove, in hashpw 12356, that the size of the power set of a finite set is 2 raised to the power of the size of the set. (Contributed by NM, 24-Jun-1993.)
Assertion
Ref Expression
df-pw
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-pw
StepHypRef Expression
1 cA . . 3
21cpw 3976 . 2
3 vx . . . . 5
43cv 1369 . . . 4
54, 1wss 3442 . . 3
65, 3cab 2439 . 2
72, 6wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  pweq  3979  elpw  3982  nfpw  3988  pw0  4137  pwpw0  4138  pwsn  4202  pwsnALT  4203  pwex  4592  abssexg  4594  orduniss2  6577  mapex  7354  ssenen  7619  domtriomlem  8748  npex  9292  ustval  20176  avril1  24125  dfon2lem2  28053
  Copyright terms: Public domain W3C validator