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	|- F/ x ph
	nfiund.2	|- ( ph -> F/_ y A )
	nfiund.3	|- ( ph -> F/_ y B )
Assertion	nfiund	|- ( ph -> F/_ y U_ x e. A B )

Proof

Step	Hyp	Ref	Expression
1		nfiund.1	|- F/ x ph
2		nfiund.2	|- ( ph -> F/_ y A )
3		nfiund.3	|- ( ph -> F/_ y B )
4		df-iun	|- U_ x e. A B = { z | E. x e. A z e. B }
5		nfv	|- F/ z ph
6	3	nfcrd	|- ( ph -> F/ y z e. B )
7	1 2 6	nfrexd	|- ( ph -> F/ y E. x e. A z e. B )
8	5 7	nfabdw	|- ( ph -> F/_ y { z | E. x e. A z e. B } )
9	4 8	nfcxfrd	|- ( ph -> F/_ y U_ x e. A B )