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

Definition df-iin 3716
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3715. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3748. Theorem intiin 3767 provides a definition of ordinary intersection in terms of indexed intersection. (Contributed by NM, 27-Jun-1998.)
Assertion
Ref Expression
df-iin 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝑦,𝐵
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Detailed syntax breakdown of Definition df-iin
StepHypRef Expression
1 vx . . 3 setvar 𝑥
2 cA . . 3 class 𝐴
3 cB . . 3 class 𝐵
41, 2, 3ciin 3714 . 2 class 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1286 . . . . 5 class 𝑦
76, 3wcel 1436 . . . 4 wff 𝑦𝐵
87, 1, 2wral 2355 . . 3 wff 𝑥𝐴 𝑦𝐵
98, 5cab 2071 . 2 class {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
104, 9wceq 1287 1 wff 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
Colors of variables: wff set class
This definition is referenced by:  eliin  3718  iineq1  3727  iineq2  3730  nfiinxy  3740  nfiinya  3742  nfii1  3744  dfiin2g  3746  cbviin  3751  intiin  3767  0iin  3771  viin  3772  iinxsng  3786  iinxprg  3787  iinuniss  3793  bdciin  11200
  Copyright terms: Public domain W3C validator