Metamath Proof Explorer

Theorem ssiun2

Description: Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion ssiun2 ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 rspe ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
2 1 ex ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
3 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
4 2 3 imbitrrdi ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
5 4 ssrdv ⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )