Definition df-fi 7465

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 7464	. 2
2		vx	. . 3
3		cvv 2965	. . 3
4		vz	. . . . . . 7
5	4	cv 1653	. . . . . 6
6		vy	. . . . . . . 8
7	6	cv 1653	. . . . . . 7
8	7	cint 4079	. . . . . 6
9	5, 8	wceq 1654	. . . . 5
10	2	cv 1653	. . . . . . 7
11	10	cpw 3826	. . . . . 6
12		cfn 7158	. . . . . 6
13	11, 12	cin 3308	. . . . 5
14	9, 6, 13	wrex 2713	. . . 4
15	14, 4	cab 2429	. . 3
16	2, 3, 15	cmpt 4301	. 2
17	1, 16	wceq 1654	1

This definition is referenced by:  fival  7466