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

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

Detailed syntax breakdown of Definition df-phi
StepHypRef Expression
1 cA . . 3
21cphi 4562 . 2 Phi
3 vy . . . . . 6
43cv 1641 . . . . 5
5 vx . . . . . . . 8
65cv 1641 . . . . . . 7
7 cnnc 4373 . . . . . . 7 Nn
86, 7wcel 1710 . . . . . 6 Nn
9 c1c 4134 . . . . . . 7 1c
106, 9cplc 4375 . . . . . 6 1c
118, 10, 6cif 3662 . . . . 5 Nn 1c
124, 11wceq 1642 . . . 4 Nn 1c
1312, 5, 1wrex 2615 . . 3 Nn 1c
1413, 3cab 2339 . 2 Nn 1c
152, 14wceq 1642 1 Phi Nn 1c
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