Theorem nfdif

Description: Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003) (Revised by Mario Carneiro, 13-Oct-2016)

	Ref	Expression
Hypotheses	nfdif.1	⊢ Ⅎ 𝑥 𝐴
	nfdif.2	⊢ Ⅎ 𝑥 𝐵
Assertion	nfdif	⊢ Ⅎ 𝑥 ( 𝐴 ∖ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfdif.1	⊢ Ⅎ 𝑥 𝐴
2		nfdif.2	⊢ Ⅎ 𝑥 𝐵
3		dfdif2	⊢ ( 𝐴 ∖ 𝐵 ) = { 𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵 }
4	2	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
5	4	nfn	⊢ Ⅎ 𝑥 ¬ 𝑦 ∈ 𝐵
6	5 1	nfrabw	⊢ Ⅎ 𝑥 { 𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵 }
7	3 6	nfcxfr	⊢ Ⅎ 𝑥 ( 𝐴 ∖ 𝐵 )