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

Definition df-iin 3741
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3740. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3773. Theorem intiin 3792 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 3739 . 2 class 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1289 . . . . 5 class 𝑦
76, 3wcel 1439 . . . 4 wff 𝑦𝐵
87, 1, 2wral 2360 . . 3 wff 𝑥𝐴 𝑦𝐵
98, 5cab 2075 . 2 class {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
104, 9wceq 1290 1 wff 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
Colors of variables: wff set class
This definition is referenced by:  eliin  3743  iineq1  3752  iineq2  3755  nfiinxy  3765  nfiinya  3767  nfii1  3769  dfiin2g  3771  cbviin  3776  intiin  3792  0iin  3796  viin  3797  iinxsng  3811  iinxprg  3812  iinuniss  3819  bdciin  12074
  Copyright terms: Public domain W3C validator