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

Definition df-iin 3688
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3687. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3720. Theorem intiin 3739 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 3686 . 2 class 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1258 . . . . 5 class 𝑦
76, 3wcel 1409 . . . 4 wff 𝑦𝐵
87, 1, 2wral 2323 . . 3 wff 𝑥𝐴 𝑦𝐵
98, 5cab 2042 . 2 class {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
104, 9wceq 1259 1 wff 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
Colors of variables: wff set class
This definition is referenced by:  eliin  3690  iineq1  3699  iineq2  3702  nfiinxy  3712  nfiinya  3714  nfii1  3716  dfiin2g  3718  cbviin  3723  intiin  3739  0iin  3743  viin  3744  iinxsng  3758  iinxprg  3759  iinuniss  3765  bdciin  10386
  Copyright terms: Public domain W3C validator