Theorem nfintd

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

	Ref	Expression
Hypothesis	nfintd.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
Assertion	nfintd	⊢ ( 𝜑 → Ⅎ 𝑥 ∩ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nfintd.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2		df-int	⊢ ∩ 𝐴 = { 𝑦 ∣ ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑦 ∈ 𝑧 ) }
3		nfv	⊢ Ⅎ 𝑦 𝜑
4		nfv	⊢ Ⅎ 𝑧 𝜑
5	1	nfcrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑧 ∈ 𝐴 )
6		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝑧
7	6	a1i	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 ∈ 𝑧 )
8	5 7	nfimd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 → 𝑦 ∈ 𝑧 ) )
9	4 8	nfald	⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑦 ∈ 𝑧 ) )
10	3 9	nfabdw	⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑦 ∣ ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑦 ∈ 𝑧 ) } )
11	2 10	nfcxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 ∩ 𝐴 )