![]() |
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 4999. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 5037. Theorem intiin 5062 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 4998 | . 2 class ∩ 𝑥 ∈ 𝐴 𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1539 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2105 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wral 3060 | . . 3 wff ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2708 | . 2 class {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1540 | 1 wff ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
Colors of variables: wff setvar class |
This definition is referenced by: eliin 5002 iineq1 5014 iineq2 5017 nfiin 5028 nfiing 5030 nfii1 5032 dfiin2g 5035 cbviin 5040 cbviing 5042 intiin 5062 0iin 5067 viin 5068 iinxsng 5091 iinxprg 5092 iinuni 5101 iinabrex 32068 iineq12f 37336 |
Copyright terms: Public domain | W3C validator |