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

Definition df-iin 3889
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3888. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3921. Theorem intiin 3941 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 3887 . 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  3891  iineq1  3900  iineq2  3903  nfiinxy  3913  nfiinya  3915  nfii1  3917  dfiin2g  3919  cbviin  3924  intiin  3941  0iin  3945  viin  3946  iinxsng  3960  iinxprg  3961  iinuniss  3969  bdciin  14601
  Copyright terms: Public domain W3C validator