| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-iin | Structured version Visualization version GIF version | ||
| 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.) |
| Ref | Expression |
|---|---|
| df-iin | ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vx | . . 3 setvar 𝑥 | |
| 2 | cA | . . 3 class 𝐴 | |
| 3 | cB | . . 3 class 𝐵 | |
| 4 | 1, 2, 3 | ciin 4992 | . 2 class ∩ 𝑥 ∈ 𝐴 𝐵 |
| 5 | vy | . . . . . 6 setvar 𝑦 | |
| 6 | 5 | cv 1539 | . . . . 5 class 𝑦 |
| 7 | 6, 3 | wcel 2108 | . . . 4 wff 𝑦 ∈ 𝐵 |
| 8 | 7, 1, 2 | wral 3061 | . . 3 wff ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 |
| 9 | 8, 5 | cab 2714 | . 2 class {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
| 10 | 4, 9 | wceq 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 |