Definition df-pw1fn 5767

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.)

Assertion

Ref	Expression
df-pw1fn	⊢ Pw1Fn = (x ∈ 1c ↦ ℘1∪x)

Detailed syntax breakdown of Definition df-pw1fn

Step	Hyp	Ref	Expression
1		cpw1fn 5766	. 2 class Pw1Fn
2		vx	. . 3 setvar x
3		c1c 4135	. . 3 class 1c
4	2	cv 1641	. . . . 5 class x
5	4	cuni 3892	. . . 4 class ∪x
6	5	cpw1 4136	. . 3 class ℘1∪x
7	2, 3, 6	cmpt 5652	. 2 class (x ∈ 1c ↦ ℘1∪x)
8	1, 7	wceq 1642	1 wff Pw1Fn = (x ∈ 1c ↦ ℘1∪x)

This definition is referenced by:  pw1fnval  5852  pw1fnex  5853  fnpw1fn  5854  pw1fnf1o  5856