Description: Membership in indexed intersection. (Contributed by NM, 3-Sep-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | eliin | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1w | ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝐶 ↔ 𝑤 ∈ 𝐶 ) ) | |
2 | 1 | ralbidv | ⊢ ( 𝑦 = 𝑤 → ( ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝑤 ∈ 𝐶 ) ) |
3 | eleq1 | ⊢ ( 𝑤 = 𝐴 → ( 𝑤 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶 ) ) | |
4 | 3 | ralbidv | ⊢ ( 𝑤 = 𝐴 → ( ∀ 𝑥 ∈ 𝐵 𝑤 ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) ) |
5 | df-iin | ⊢ ∩ 𝑥 ∈ 𝐵 𝐶 = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 } | |
6 | 2 4 5 | elab2gw | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) ) |