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

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
StepHypRef Expression
1 cfi 7464 . 2
2 vx . . 3
3 cvv 2965 . . 3
4 vz . . . . . . 7
54cv 1653 . . . . . 6
6 vy . . . . . . . 8
76cv 1653 . . . . . . 7
87cint 4079 . . . . . 6
95, 8wceq 1654 . . . . 5
102cv 1653 . . . . . . 7
1110cpw 3826 . . . . . 6
12 cfn 7158 . . . . . 6
1311, 12cin 3308 . . . . 5
149, 6, 13wrex 2713 . . . 4
1514, 4cab 2429 . . 3
162, 3, 15cmpt 4301 . 2
171, 16wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  fival  7466
  Copyright terms: Public domain W3C validator