MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fi Unicode version

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
StepHypRef Expression
1 cfi 7890 . 2
2 vx . . 3
3 cvv 3109 . . 3
4 vz . . . . . . 7
54cv 1394 . . . . . 6
6 vy . . . . . . . 8
76cv 1394 . . . . . . 7
87cint 4286 . . . . . 6
95, 8wceq 1395 . . . . 5
102cv 1394 . . . . . . 7
1110cpw 4012 . . . . . 6
12 cfn 7536 . . . . . 6
1311, 12cin 3474 . . . . 5
149, 6, 13wrex 2808 . . . 4
1514, 4cab 2442 . . 3
162, 3, 15cmpt 4510 . 2
171, 16wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  fival  7892
  Copyright terms: Public domain W3C validator