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 4897
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 4896. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 4934. Theorem intiin 4958 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 4895 . 2 class 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1537 . . . . 5 class 𝑦
76, 3wcel 2114 . . . 4 wff 𝑦𝐵
87, 1, 2wral 3130 . . 3 wff 𝑥𝐴 𝑦𝐵
98, 5cab 2800 . 2 class {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
104, 9wceq 1538 1 wff 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  eliin  4899  iineq1  4911  iineq2  4914  nfiin  4925  nfiing  4927  nfii1  4929  dfiin2g  4932  cbviin  4937  cbviing  4939  intiin  4958  0iin  4962  viin  4963  iinxsng  4985  iinxprg  4986  iinuni  4995  iinabrex  30327  iineq12f  35561
  Copyright terms: Public domain W3C validator