Definition df-fi 7583

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 7582	. 2
2		vx	. . 3
3		cvv 3015	. . 3
4		vz	. . . . . . 7
5	4	cv 1669	. . . . . 6
6		vy	. . . . . . . 8
7	6	cv 1669	. . . . . . 7
8	7	cint 4154	. . . . . 6
9	5, 8	wceq 1670	. . . . 5
10	2	cv 1669	. . . . . . 7
11	10	cpw 3893	. . . . . 6
12		cfn 7273	. . . . . 6
13	11, 12	cin 3364	. . . . 5
14	9, 6, 13	wrex 2760	. . . 4
15	14, 4	cab 2475	. . 3
16	2, 3, 15	cmpt 4376	. 2
17	1, 16	wceq 1670	1

This definition is referenced by:  fival  7584