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

Definition df-iin 3904
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3903. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3936. Theorem intiin 3956 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 3902 . 2 class 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1363 . . . . 5 class 𝑦
76, 3wcel 2160 . . . 4 wff 𝑦𝐵
87, 1, 2wral 2468 . . 3 wff 𝑥𝐴 𝑦𝐵
98, 5cab 2175 . 2 class {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
104, 9wceq 1364 1 wff 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
Colors of variables: wff set class
This definition is referenced by:  eliin  3906  iineq1  3915  iineq2  3918  nfiinxy  3928  nfiinya  3930  nfii1  3932  dfiin2g  3934  cbviin  3939  intiin  3956  0iin  3960  viin  3961  iinxsng  3975  iinxprg  3976  iinuniss  3984  bdciin  15084
  Copyright terms: Public domain W3C validator