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

Definition df-phi 4565
Description: Define the phi operator. This operation increments all the naturals in A and leaves all its other members the same. (Contributed by SF, 3-Feb-2015.)
Assertion
Ref Expression
df-phi Phi A = {y x A y = if(x Nn , (x +c 1c), x)}
Distinct variable group:   x,y,A

Detailed syntax breakdown of Definition df-phi
StepHypRef Expression
1 cA . . 3 class A
21cphi 4562 . 2 class Phi A
3 vy . . . . . 6 setvar y
43cv 1641 . . . . 5 class y
5 vx . . . . . . . 8 setvar x
65cv 1641 . . . . . . 7 class x
7 cnnc 4373 . . . . . . 7 class Nn
86, 7wcel 1710 . . . . . 6 wff x Nn
9 c1c 4134 . . . . . . 7 class 1c
106, 9cplc 4375 . . . . . 6 class (x +c 1c)
118, 10, 6cif 3662 . . . . 5 class if(x Nn , (x +c 1c), x)
124, 11wceq 1642 . . . 4 wff y = if(x Nn , (x +c 1c), x)
1312, 5, 1wrex 2615 . . 3 wff x A y = if(x Nn , (x +c 1c), x)
1413, 3cab 2339 . 2 class {y x A y = if(x Nn , (x +c 1c), x)}
152, 14wceq 1642 1 wff Phi A = {y x A y = if(x Nn , (x +c 1c), x)}
Colors of variables: wff setvar class
This definition is referenced by:  dfphi2  4569  phi11lem1  4595  0cnelphi  4597  phiun  4614  phidisjnn  4615  phialllem1  4616
  Copyright terms: Public domain W3C validator