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

Definition df-iin 3811
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3810. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3843. Theorem intiin 3862 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 3809 . 2 class 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1330 . . . . 5 class 𝑦
76, 3wcel 1480 . . . 4 wff 𝑦𝐵
87, 1, 2wral 2414 . . 3 wff 𝑥𝐴 𝑦𝐵
98, 5cab 2123 . 2 class {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
104, 9wceq 1331 1 wff 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
Colors of variables: wff set class
This definition is referenced by:  eliin  3813  iineq1  3822  iineq2  3825  nfiinxy  3835  nfiinya  3837  nfii1  3839  dfiin2g  3841  cbviin  3846  intiin  3862  0iin  3866  viin  3867  iinxsng  3881  iinxprg  3882  iinuniss  3890  bdciin  13066
  Copyright terms: Public domain W3C validator