Definition df-ncfin 4443

Description: Define the finite cardinal function. Definition from [Rosser] p. 527. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-ncfin	|- Ncfin A = (iotax(x e. Nn /\ A e. x))

Distinct variable group:   x,A

Detailed syntax breakdown of Definition df-ncfin

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cncfin 4435	. 2 class Ncfin A
3		vx	. . . . . 6 setvar x
4	3	cv 1641	. . . . 5 class x
5		cnnc 4374	. . . . 5 class Nn
6	4, 5	wcel 1710	. . . 4 wff x e. Nn
7	1, 4	wcel 1710	. . . 4 wff A e. x
8	6, 7	wa 358	. . 3 wff (x e. Nn /\ A e. x)
9	8, 3	cio 4338	. 2 class (iotax(x e. Nn /\ A e. x))
10	2, 9	wceq 1642	1 wff Ncfin A = (iotax(x e. Nn /\ A e. x))

This definition is referenced by:  ncfinex  4473  ncfineq  4474  ncfinprop  4475