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

Definition df-iin 3786
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3785. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3818. Theorem intiin 3837 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 3784 . 2 class 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1315 . . . . 5 class 𝑦
76, 3wcel 1465 . . . 4 wff 𝑦𝐵
87, 1, 2wral 2393 . . 3 wff 𝑥𝐴 𝑦𝐵
98, 5cab 2103 . 2 class {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
104, 9wceq 1316 1 wff 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
Colors of variables: wff set class
This definition is referenced by:  eliin  3788  iineq1  3797  iineq2  3800  nfiinxy  3810  nfiinya  3812  nfii1  3814  dfiin2g  3816  cbviin  3821  intiin  3837  0iin  3841  viin  3842  iinxsng  3856  iinxprg  3857  iinuniss  3865  bdciin  13004
  Copyright terms: Public domain W3C validator