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

Definition df-iin 3660
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3659. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3692. Theorem intiin 3711 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 3658 . 2  class  |^|_ x  e.  A  B
5 vy . . . . . 6  setvar  y
65cv 1242 . . . . 5  class  y
76, 3wcel 1393 . . . 4  wff  y  e.  B
87, 1, 2wral 2306 . . 3  wff  A. x  e.  A  y  e.  B
98, 5cab 2026 . 2  class  { y  |  A. x  e.  A  y  e.  B }
104, 9wceq 1243 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  3662  iineq1  3671  iineq2  3674  nfiinxy  3684  nfiinya  3686  nfii1  3688  dfiin2g  3690  cbviin  3695  intiin  3711  0iin  3715  viin  3716  iinxsng  3730  iinxprg  3731  iinuniss  3737  bdciin  9999
  Copyright terms: Public domain W3C validator