Theorem nfin

Description: Bound-variable hypothesis builder for the intersection of classes. (Contributed by NM, 15-Sep-2003) (Revised by Mario Carneiro, 14-Oct-2016)

	Ref	Expression
Hypotheses	nfin.1	⊢ Ⅎ 𝑥 𝐴
	nfin.2	⊢ Ⅎ 𝑥 𝐵
Assertion	nfin	⊢ Ⅎ 𝑥 ( 𝐴 ∩ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfin.1	⊢ Ⅎ 𝑥 𝐴
2		nfin.2	⊢ Ⅎ 𝑥 𝐵
3		dfin5	⊢ ( 𝐴 ∩ 𝐵 ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵 }
4	2	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
5	4 1	nfrabw	⊢ Ⅎ 𝑥 { 𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵 }
6	3 5	nfcxfr	⊢ Ⅎ 𝑥 ( 𝐴 ∩ 𝐵 )