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

Definition df-pw 4014
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 25150). We will later introduce the Axiom of Power Sets ax-pow 4630, which can be expressed in class notation per pwexg 4636. Still later we will prove, in hashpw 12494, 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 4012 . 2
3 vx . . . . 5
43cv 1394 . . . 4
54, 1wss 3475 . . 3
65, 3cab 2442 . 2
72, 6wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  pweq  4015  elpw  4018  nfpw  4024  pw0  4177  pwpw0  4178  pwsn  4243  pwsnALT  4244  pwex  4635  abssexg  4637  orduniss2  6668  mapex  7445  ssenen  7711  domtriomlem  8843  npex  9385  ustval  20705  avril1  25171  dfon2lem2  29216
  Copyright terms: Public domain W3C validator