Theorem nfiung

Description: Bound-variable hypothesis builder for indexed union. Usage of this theorem is discouraged because it depends on ax-13 . See nfiun for a version with more disjoint variable conditions, but not requiring ax-13 . (Contributed by Mario Carneiro, 25-Jan-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfiung.1	|- F/_ y A
	nfiung.2	|- F/_ y B
Assertion	nfiung	|- F/_ y U_ x e. A B

Proof

Step	Hyp	Ref	Expression
1		nfiung.1	|- F/_ y A
2		nfiung.2	|- F/_ y B
3		df-iun	|- U_ x e. A B = { z | E. x e. A z e. B }
4	2	nfcri	|- F/ y z e. B
5	1 4	nfrex	|- F/ y E. x e. A z e. B
6	5	nfabg	|- F/_ y { z | E. x e. A z e. B }
7	3 6	nfcxfr	|- F/_ y U_ x e. A B