Definition df-fi 7891

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 7890	. 2
2		vx	. . 3
3		cvv 3109	. . 3
4		vz	. . . . . . 7
5	4	cv 1394	. . . . . 6
6		vy	. . . . . . . 8
7	6	cv 1394	. . . . . . 7
8	7	cint 4286	. . . . . 6
9	5, 8	wceq 1395	. . . . 5
10	2	cv 1394	. . . . . . 7
11	10	cpw 4012	. . . . . 6
12		cfn 7536	. . . . . 6
13	11, 12	cin 3474	. . . . 5
14	9, 6, 13	wrex 2808	. . . 4
15	14, 4	cab 2442	. . 3
16	2, 3, 15	cmpt 4510	. 2
17	1, 16	wceq 1395	1

This definition is referenced by:  fival  7892