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 4915
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 4914. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 4951. Theorem intiin 4975 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 4913 . 2 class 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1527 . . . . 5 class 𝑦
76, 3wcel 2105 . . . 4 wff 𝑦𝐵
87, 1, 2wral 3138 . . 3 wff 𝑥𝐴 𝑦𝐵
98, 5cab 2799 . 2 class {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
104, 9wceq 1528 1 wff 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  eliin  4917  iineq1  4928  iineq2  4931  nfiin  4942  nfiing  4944  nfii1  4946  dfiin2g  4949  cbviin  4954  cbviing  4956  intiin  4975  0iin  4979  viin  4980  iinxsng  5002  iinxprg  5003  iinuni  5012  iineq12f  35325
  Copyright terms: Public domain W3C validator