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

Proof

Step	Hyp	Ref	Expression
1		nfiundg.1	|- F/ x ph
2		nfiundg.2	|- ( ph -> F/_ y A )
3		nfiundg.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	nfabd	|- ( ph -> F/_ y { z | E. x e. A z e. B } )
9	4 8	nfcxfrd	|- ( ph -> F/_ y U_ x e. A B )