Theorem bnj226

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bnj226.1	⊢ 𝐵 ⊆ 𝐶
Assertion	bnj226	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶

Proof

Step	Hyp	Ref	Expression
1		bnj226.1	⊢ 𝐵 ⊆ 𝐶
2	1	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶
3		iunss	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
4	2 3	mpbir	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶