Theorem nfiu1

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003) Avoid ax-11 , ax-12 . (Revised by SN, 14-May-2025)

	Ref	Expression
Assertion	nfiu1	|- F/_ x U_ x e. A B

Proof

Step	Hyp	Ref	Expression
1		eliun	|- ( y e. U_ x e. A B <-> E. x e. A y e. B )
2		nfre1	|- F/ x E. x e. A y e. B
3	1 2	nfxfr	|- F/ x y e. U_ x e. A B
4	3	nfci	|- F/_ x U_ x e. A B