Theorem nfiundg

Description: Bound-variable hypothesis builder for indexed union. Usage of this theorem is discouraged because it depends on ax-13 , see nfiund for a weaker version that does not require it. (Contributed by Emmett Weisz, 6-Dec-2019) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfiundg.1	$$⊢Ⅎx\phi$$
	nfiundg.2	$$⊢\phi \to \underset{\_}{Ⅎ}yA$$
	nfiundg.3	$$⊢\phi \to \underset{\_}{Ⅎ}yB$$
Assertion	nfiundg	$$⊢\phi \to \underset{\_}{Ⅎ}y\bigcup _{x\in A}B$$

Proof

Step	Hyp	Ref	Expression
1		nfiundg.1	$$⊢Ⅎx\phi$$
2		nfiundg.2	$$⊢\phi \to \underset{\_}{Ⅎ}yA$$
3		nfiundg.3	$$⊢\phi \to \underset{\_}{Ⅎ}yB$$
4		df-iun	$$⊢\bigcup _{x\in A}B=\left\{z|\exists x\in Az\in B\right\}$$
5		nfv	$$⊢Ⅎz\phi$$
6	3	nfcrd	$$⊢\phi \to Ⅎyz\in B$$
7	1 2 6	nfrexdg	$$⊢\phi \to Ⅎy\exists x\in Az\in B$$
8	5 7	nfabd	$$⊢\phi \to \underset{\_}{Ⅎ}y\left\{z|\exists x\in Az\in B\right\}$$
9	4 8	nfcxfrd	$$⊢\phi \to \underset{\_}{Ⅎ}y\bigcup _{x\in A}B$$