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

Definition df-iin 3689
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3688. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3721. Theorem intiin 3740 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 3687 . 2  class  |^|_ x  e.  A  B
5 vy . . . . . 6  setvar  y
65cv 1284 . . . . 5  class  y
76, 3wcel 1434 . . . 4  wff  y  e.  B
87, 1, 2wral 2349 . . 3  wff  A. x  e.  A  y  e.  B
98, 5cab 2068 . 2  class  { y  |  A. x  e.  A  y  e.  B }
104, 9wceq 1285 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  3691  iineq1  3700  iineq2  3703  nfiinxy  3713  nfiinya  3715  nfii1  3717  dfiin2g  3719  cbviin  3724  intiin  3740  0iin  3744  viin  3745  iinxsng  3759  iinxprg  3760  iinuniss  3766  bdciin  10828
  Copyright terms: Public domain W3C validator