Description: A singleton index picks out an instance of an indexed intersection's argument. (Contributed by NM, 15-Jan-2012) (Proof shortened by Mario Carneiro, 17-Nov-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | iinxsng.1 | ⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) | |
| Assertion | iinxsng | ⊢ ( 𝐴 ∈ 𝑉 → ∩ 𝑥 ∈ { 𝐴 } 𝐵 = 𝐶 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iinxsng.1 | ⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) | |
| 2 | df-iin | ⊢ ∩ 𝑥 ∈ { 𝐴 } 𝐵 = { 𝑦 ∣ ∀ 𝑥 ∈ { 𝐴 } 𝑦 ∈ 𝐵 } | |
| 3 | 1 | eleq2d | ⊢ ( 𝑥 = 𝐴 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ) |
| 4 | 3 | ralsng | ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝐴 } 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ) |
| 5 | 4 | abbi1dv | ⊢ ( 𝐴 ∈ 𝑉 → { 𝑦 ∣ ∀ 𝑥 ∈ { 𝐴 } 𝑦 ∈ 𝐵 } = 𝐶 ) |
| 6 | 2 5 | syl5eq | ⊢ ( 𝐴 ∈ 𝑉 → ∩ 𝑥 ∈ { 𝐴 } 𝐵 = 𝐶 ) |