Theorem ss2iundv

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

	Ref	Expression
Hypotheses	ss2iundv.el	$$⊢\left(\phi \wedge x\in A\right)\to Y\in C$$
	ss2iundv.sub	$$⊢\left(\phi \wedge x\in A\wedge y=Y\right)\to D=G$$
	ss2iundv.ss	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq G$$
Assertion	ss2iundv	$$⊢\phi \to \bigcup _{x\in A}B\subseteq \bigcup _{y\in C}D$$

Proof

Step	Hyp	Ref	Expression
1		ss2iundv.el	$$⊢\left(\phi \wedge x\in A\right)\to Y\in C$$
2		ss2iundv.sub	$$⊢\left(\phi \wedge x\in A\wedge y=Y\right)\to D=G$$
3		ss2iundv.ss	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq G$$
4		nfv	$$⊢Ⅎx\phi$$
5		nfv	$$⊢Ⅎy\phi$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}yY$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}xC$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}yC$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}xD$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}yG$$
13	4 5 6 7 8 9 10 11 12 1 2 3	ss2iundf	$$⊢\phi \to \bigcup _{x\in A}B\subseteq \bigcup _{y\in C}D$$