NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-pw1fn GIF version

Definition df-pw1fn 5766
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 1x)

Detailed syntax breakdown of Definition df-pw1fn
StepHypRef Expression
1 cpw1fn 5765 . 2 class Pw1Fn
2 vx . . 3 setvar x
3 c1c 4134 . . 3 class 1c
42cv 1641 . . . . 5 class x
54cuni 3891 . . . 4 class x
65cpw1 4135 . . 3 class 1x
72, 3, 6cmpt 5651 . 2 class (x 1c 1x)
81, 7wceq 1642 1 wff Pw1Fn = (x 1c 1x)
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