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 4921. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 4959. Theorem intiin 4983 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 4920 | . 2 class ∩ 𝑥 ∈ 𝐴 𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1536 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2114 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wral 3138 | . . 3 wff ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2799 | . 2 class {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1537 | 1 wff ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
Colors of variables: wff setvar class |
This definition is referenced by: eliin 4924 iineq1 4936 iineq2 4939 nfiin 4950 nfiing 4952 nfii1 4954 dfiin2g 4957 cbviin 4962 cbviing 4964 intiin 4983 0iin 4987 viin 4988 iinxsng 5010 iinxprg 5011 iinuni 5020 iineq12f 35457 |
Copyright terms: Public domain | W3C validator |