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

Definition df-fi 7528
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 7527 . 2
2 vx . . 3
3 cvv 3006 . . 3
4 vz . . . . . . 7
54cv 1661 . . . . . 6
6 vy . . . . . . . 8
76cv 1661 . . . . . . 7
87cint 4138 . . . . . 6
95, 8wceq 1662 . . . . 5
102cv 1661 . . . . . . 7
1110cpw 3878 . . . . . 6
12 cfn 7221 . . . . . 6
1311, 12cin 3352 . . . . 5
149, 6, 13wrex 2752 . . . 4
1514, 4cab 2467 . . 3
162, 3, 15cmpt 4360 . 2
171, 16wceq 1662 1
Colors of variables: wff set class
This definition is referenced by:  fival  7529
  Copyright terms: Public domain W3C validator