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	⊢ Ⅎ 𝑥 𝐴
Assertion	nfint	⊢ Ⅎ 𝑥 ∩ 𝐴

Proof

Step	Hyp	Ref	Expression
1		nfint.1	⊢ Ⅎ 𝑥 𝐴
2		dfint2	⊢ ∩ 𝐴 = { 𝑦 ∣ ∀ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 }
3		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝑧
4	1 3	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧
5	4	nfab	⊢ Ⅎ 𝑥 { 𝑦 ∣ ∀ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 }
6	2 5	nfcxfr	⊢ Ⅎ 𝑥 ∩ 𝐴