Theorem nfintd

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

	Ref	Expression
Hypothesis	nfintd.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
Assertion	nfintd	$$⊢\phi \to \underset{\_}{Ⅎ}x\bigcap A$$

Proof

Step	Hyp	Ref	Expression
1		nfintd.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
2		df-int	$$⊢\bigcap A=\left\{y|\forall z\left(z\in A\to y\in z\right)\right\}$$
3		nfv	$$⊢Ⅎy\phi$$
4		nfv	$$⊢Ⅎz\phi$$
5	1	nfcrd	$$⊢\phi \to Ⅎxz\in A$$
6		nfv	$$⊢Ⅎxy\in z$$
7	6	a1i	$$⊢\phi \to Ⅎxy\in z$$
8	5 7	nfimd	$$⊢\phi \to Ⅎx\left(z\in A\to y\in z\right)$$
9	4 8	nfald	$$⊢\phi \to Ⅎx\forall z\left(z\in A\to y\in z\right)$$
10	3 9	nfabdw	$$⊢\phi \to \underset{\_}{Ⅎ}x\left\{y|\forall z\left(z\in A\to y\in z\right)\right\}$$
11	2 10	nfcxfrd	$$⊢\phi \to \underset{\_}{Ⅎ}x\bigcap A$$