Theorem nfiing

Description: Bound-variable hypothesis builder for indexed intersection. Usage of this theorem is discouraged because it depends on ax-13 . See nfiin 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	nfiing	|- F/_ y |^|_ x e. A B

Proof

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