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

Definition df-iin 3887
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3886. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3919. Theorem intiin 3938 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 3885 . 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  3889  iineq1  3898  iineq2  3901  nfiinxy  3911  nfiinya  3913  nfii1  3915  dfiin2g  3917  cbviin  3922  intiin  3938  0iin  3942  viin  3943  iinxsng  3957  iinxprg  3958  iinuniss  3966  bdciin  14287
  Copyright terms: Public domain W3C validator