Definition df-fi 7528

Description: Function whose value is the class of all the finite intersections of the elements of . (Contributed by FL, 27-Apr-2008.)

Assertion

Ref	Expression
df-fi

Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-fi

Step	Hyp	Ref	Expression
1		cfi 7527	. 2
2		vx	. . 3
3		cvv 3006	. . 3
4		vz	. . . . . . 7
5	4	cv 1661	. . . . . 6
6		vy	. . . . . . . 8
7	6	cv 1661	. . . . . . 7
8	7	cint 4138	. . . . . 6
9	5, 8	wceq 1662	. . . . 5
10	2	cv 1661	. . . . . . 7
11	10	cpw 3878	. . . . . 6
12		cfn 7221	. . . . . 6
13	11, 12	cin 3352	. . . . 5
14	9, 6, 13	wrex 2752	. . . 4
15	14, 4	cab 2467	. . 3
16	2, 3, 15	cmpt 4360	. 2
17	1, 16	wceq 1662	1

This definition is referenced by:  fival  7529