Metamath Proof Explorer

Theorem iinss2

Description: An indexed intersection is included in any of its members. (Contributed by FL, 15-Oct-2012)

Ref Expression
Assertion iinss2 ( 𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 eliin ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
2 1 elv ⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
3 rsp ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) )
4 3 com12 ⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐵 ) )
5 2 4 biimtrid ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐵 ) )
6 5 ssrdv ⊢ ( 𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 )