New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > df-pw1fn | GIF version |
Description: Define the function that takes a singleton to the unit power class of its member. This function is defined in such a way as to ensure stratification. (Contributed by SF, 9-Feb-2015.) |
Ref | Expression |
---|---|
df-pw1fn | ⊢ Pw1Fn = (x ∈ 1c ↦ ℘1∪x) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cpw1fn 5765 | . 2 class Pw1Fn | |
2 | vx | . . 3 setvar x | |
3 | c1c 4134 | . . 3 class 1c | |
4 | 2 | cv 1641 | . . . . 5 class x |
5 | 4 | cuni 3891 | . . . 4 class ∪x |
6 | 5 | cpw1 4135 | . . 3 class ℘1∪x |
7 | 2, 3, 6 | cmpt 5651 | . 2 class (x ∈ 1c ↦ ℘1∪x) |
8 | 1, 7 | wceq 1642 | 1 wff Pw1Fn = (x ∈ 1c ↦ ℘1∪x) |
Colors of variables: wff setvar class |
This definition is referenced by: pw1fnval 5851 pw1fnex 5852 fnpw1fn 5853 pw1fnf1o 5855 |
Copyright terms: Public domain | W3C validator |