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

Definition df-iin 3888
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3887. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3920. Theorem intiin 3939 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 3886 . 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  3890  iineq1  3899  iineq2  3902  nfiinxy  3912  nfiinya  3914  nfii1  3916  dfiin2g  3918  cbviin  3923  intiin  3939  0iin  3943  viin  3944  iinxsng  3958  iinxprg  3959  iinuniss  3967  bdciin  14402
  Copyright terms: Public domain W3C validator