Theorem nfintd

Description: Bound-variable hypothesis builder for intersection. (Contributed by Emmett Weisz, 16-Jan-2020)

	Ref	Expression
Hypothesis	nfintd.1	|- ( ph -> F/_ x A )
Assertion	nfintd	|- ( ph -> F/_ x |^| A )

Proof

Step	Hyp	Ref	Expression
1		nfintd.1	|- ( ph -> F/_ x A )
2		df-int	|- |^| A = { y | A. z ( z e. A -> y e. z ) }
3		nfv	|- F/ y ph
4		nfv	|- F/ z ph
5	1	nfcrd	|- ( ph -> F/ x z e. A )
6		nfv	|- F/ x y e. z
7	6	a1i	|- ( ph -> F/ x y e. z )
8	5 7	nfimd	|- ( ph -> F/ x ( z e. A -> y e. z ) )
9	4 8	nfald	|- ( ph -> F/ x A. z ( z e. A -> y e. z ) )
10	3 9	nfabdw	|- ( ph -> F/_ x { y | A. z ( z e. A -> y e. z ) } )
11	2 10	nfcxfrd	|- ( ph -> F/_ x |^| A )