Definition df-phi 4566

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 | E.x e. A y = if(x e. Nn , (x +o 1c), x)}

Distinct variable group:   x,y,A

Detailed syntax breakdown of Definition df-phi

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cphi 4563	. 2 class Phi A
3		vy	. . . . . 6 setvar y
4	3	cv 1641	. . . . 5 class y
5		vx	. . . . . . . 8 setvar x
6	5	cv 1641	. . . . . . 7 class x
7		cnnc 4374	. . . . . . 7 class Nn
8	6, 7	wcel 1710	. . . . . 6 wff x e. Nn
9		c1c 4135	. . . . . . 7 class 1c
10	6, 9	cplc 4376	. . . . . 6 class (x +o 1c)
11	8, 10, 6	cif 3663	. . . . 5 class if(x e. Nn , (x +o 1c), x)
12	4, 11	wceq 1642	. . . 4 wff y = if(x e. Nn , (x +o 1c), x)
13	12, 5, 1	wrex 2616	. . 3 wff E.x e. A y = if(x e. Nn , (x +o 1c), x)
14	13, 3	cab 2339	. 2 class {y | E.x e. A y = if(x e. Nn , (x +o 1c), x)}
15	2, 14	wceq 1642	1 wff Phi A = {y | E.x e. A y = if(x e. Nn , (x +o 1c), x)}

This definition is referenced by:  dfphi2  4570  phi11lem1  4596  0cnelphi  4598  phiun  4615  phidisjnn  4616  phialllem1  4617