Theorem ss2iundv

Description: Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020)

	Ref	Expression
Hypotheses	ss2iundv.el	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝐶 )
	ss2iundv.sub	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌 ) → 𝐷 = 𝐺 )
	ss2iundv.ss	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐺 )
Assertion	ss2iundv	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		ss2iundv.el	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝐶 )
2		ss2iundv.sub	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌 ) → 𝐷 = 𝐺 )
3		ss2iundv.ss	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐺 )
4		nfv	⊢ Ⅎ 𝑥 𝜑
5		nfv	⊢ Ⅎ 𝑦 𝜑
6		nfcv	⊢ Ⅎ 𝑦 𝑌
7		nfcv	⊢ Ⅎ 𝑦 𝐴
8		nfcv	⊢ Ⅎ 𝑦 𝐵
9		nfcv	⊢ Ⅎ 𝑥 𝐶
10		nfcv	⊢ Ⅎ 𝑦 𝐶
11		nfcv	⊢ Ⅎ 𝑥 𝐷
12		nfcv	⊢ Ⅎ 𝑦 𝐺
13	4 5 6 7 8 9 10 11 12 1 2 3	ss2iundf	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )