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 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.) |
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 4913 | . 2 class ∩ 𝑥 ∈ 𝐴 𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1527 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2105 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wral 3138 | . . 3 wff ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2799 | . 2 class {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 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 |