Theorem nfint

Description: Bound-variable hypothesis builder for intersection. (Contributed by NM, 2-Feb-1997) (Proof shortened by Andrew Salmon, 12-Aug-2011)

	Ref	Expression
Hypothesis	nfint.1	|- F/_ x A
Assertion	nfint	|- F/_ x |^| A

Proof

Step	Hyp	Ref	Expression
1		nfint.1	|- F/_ x A
2		dfint2	|- |^| A = { y | A. z e. A y e. z }
3		nfv	|- F/ x y e. z
4	1 3	nfralw	|- F/ x A. z e. A y e. z
5	4	nfab	|- F/_ x { y | A. z e. A y e. z }
6	2 5	nfcxfr	|- F/_ x |^| A