HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Definition df-pw 2392
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 V.
Assertion
Ref Expression
df-pw |- P~A = {x | x (_ A}
Distinct variable group:   x,A
Detailed syntax breakdown of Definition df-pw
StepHypRef Expression
1 cA . . 3 class A
21cpw 2391 . 2 class P~A
3 vx . . . . 5 set x
43cv 952 . . . 4 class x
54, 1wss 2037 . . 3 wff x (_ A
65, 3cab 1456 . 2 class {x | x (_ A}
72, 6wceq 953 1 wff P~A = {x | x (_ A}
Colors of variables: wff set class
This definition is referenced by:  pweq 2393  elpw 2394  pw0 2459  pwpw0 2460  snsspw 2470  pwsn 2491  pwex 2735  iunpw 2904  orduniss2 3080  mapex 4312  mapsspw 4325  ssenen 4484  npex 5063  infmap2lem2 7522  gch-kn 7529  isbasis2g 7554  cncnplem1 7713  opnfss 7798  issubg 8053  avril1 8723  shex 8998
Copyright terms: Public domain