MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-iin Structured version   Visualization version   GIF version

Definition df-iin 4994
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 4993. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 5034. Theorem intiin 5059 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 4992 . 2 class 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1539 . . . . 5 class 𝑦
76, 3wcel 2108 . . . 4 wff 𝑦𝐵
87, 1, 2wral 3061 . . 3 wff 𝑥𝐴 𝑦𝐵
98, 5cab 2714 . 2 class {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
104, 9wceq 1540 1 wff 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  eliin  4996  iineq1  5009  iineq2  5012  nfiin  5024  nfiing  5026  nfii1  5029  dfiin2g  5032  cbviin  5037  cbviing  5039  cbviinv  5041  intiin  5059  0iin  5064  viin  5065  iinxsng  5088  iinxprg  5089  iinuni  5098  iinabrex  32582  iineq1i  36197  iineq12i  36198  cbviinvw2  36234  cbviindavw  36264  cbviindavw2  36288  iineq12f  38171  iineq12dv  45111
  Copyright terms: Public domain W3C validator