Theorem nfiund

Description: Bound-variable hypothesis builder for indexed union. (Contributed by Emmett Weisz, 6-Dec-2019) Add disjoint variable condition to avoid ax-13 . See nfiundg for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		nfiund.1	$$⊢Ⅎx\phi$$
2		nfiund.2	$$⊢\phi \to \underset{\_}{Ⅎ}yA$$
3		nfiund.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	nfrexdw	$$⊢\phi \to Ⅎy\exists x\in Az\in B$$
8	5 7	nfabdw	$$⊢\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$$