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

Definition df-pw 3895
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 22758). We will later introduce the Axiom of Power Sets ax-pow 4493, which can be expressed in class notation per pwexg 4499. Still later we will prove, in hashpw 12045, 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, 5-Aug-1993.)
Assertion
Ref Expression
df-pw
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-pw
StepHypRef Expression
1 cA . . 3
21cpw 3893 . 2
3 vx . . . . 5
43cv 1669 . . . 4
54, 1wss 3365 . . 3
65, 3cab 2475 . 2
72, 6wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  pweq  3896  elpw  3899  nfpw  3905  pw0  4045  pwpw0  4046  pwsn  4111  pwsnALT  4112  pwex  4498  abssexg  4500  orduniss2  6454  mapex  7186  ssenen  7446  domtriomlem  8493  npex  9034  ustval  19247  avril1  22778  dfon2lem2  26750
  Copyright terms: Public domain W3C validator