Theorem uniss

Description: Subclass relationship for class union. Theorem 61 of Suppes p. 39. (Contributed by NM, 22-Mar-1998) (Proof shortened by Andrew Salmon, 29-Jun-2011)

	Ref	Expression
Assertion	uniss	⊢ ( 𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ssel	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) )
2	1	anim2d	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) )
3	2	eximdv	⊢ ( 𝐴 ⊆ 𝐵 → ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) )
4		eluni	⊢ ( 𝑥 ∈ ∪ 𝐴 ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) )
5		eluni	⊢ ( 𝑥 ∈ ∪ 𝐵 ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) )
6	3 4 5	3imtr4g	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵 ) )
7	6	ssrdv	⊢ ( 𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵 )