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

Definition df-iin 3715
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3714. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3747. Theorem intiin 3766 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 3713 . 2  class  |^|_ x  e.  A  B
5 vy . . . . . 6  setvar  y
65cv 1286 . . . . 5  class  y
76, 3wcel 1436 . . . 4  wff  y  e.  B
87, 1, 2wral 2355 . . 3  wff  A. x  e.  A  y  e.  B
98, 5cab 2071 . 2  class  { y  |  A. x  e.  A  y  e.  B }
104, 9wceq 1287 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  3717  iineq1  3726  iineq2  3729  nfiinxy  3739  nfiinya  3741  nfii1  3743  dfiin2g  3745  cbviin  3750  intiin  3766  0iin  3770  viin  3771  iinxsng  3785  iinxprg  3786  iinuniss  3792  bdciin  11199
  Copyright terms: Public domain W3C validator