ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-iin Unicode version

Definition df-iin 3890
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3889. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3922. Theorem intiin 3942 provides a definition of ordinary intersection in terms of indexed intersection. (Contributed by NM, 27-Jun-1998.)
Assertion
Ref Expression
df-iin  |-  |^|_ x  e.  A  B  =  { y  |  A. x  e.  A  y  e.  B }
Distinct variable groups:    x, y    y, A    y, B
Allowed substitution hints:    A( x)    B( x)

Detailed syntax breakdown of Definition df-iin
StepHypRef Expression
1 vx . . 3  setvar  x
2 cA . . 3  class  A
3 cB . . 3  class  B
41, 2, 3ciin 3888 . 2  class  |^|_ x  e.  A  B
5 vy . . . . . 6  setvar  y
65cv 1352 . . . . 5  class  y
76, 3wcel 2148 . . . 4  wff  y  e.  B
87, 1, 2wral 2455 . . 3  wff  A. x  e.  A  y  e.  B
98, 5cab 2163 . 2  class  { y  |  A. x  e.  A  y  e.  B }
104, 9wceq 1353 1  wff  |^|_ x  e.  A  B  =  { y  |  A. x  e.  A  y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  eliin  3892  iineq1  3901  iineq2  3904  nfiinxy  3914  nfiinya  3916  nfii1  3918  dfiin2g  3920  cbviin  3925  intiin  3942  0iin  3946  viin  3947  iinxsng  3961  iinxprg  3962  iinuniss  3970  bdciin  14634
  Copyright terms: Public domain W3C validator