Theorem nfdif 4124

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

Hypotheses

Ref	Expression
nfdif.1	⊢ Ⅎ𝑥𝐴
nfdif.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfdif	⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)

Proof of Theorem nfdif

Dummy variable 𝑦 is distinct from all other variables.

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

Syntax hints:  ¬ wn 3   ∈ wcel 2106  Ⅎwnfc 2883  {crab 3432   ∖ cdif 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-rab 3433  df-dif 3950

This theorem is referenced by:  nfsymdif  4245  csbdif  4526  iunxdif3  5097  boxcutc  8931  nfsup  9442  gsum2d2lem  19835  iunconn  22923  iundisj  25056  iundisj2  25057  limciun  25402  difrab2  31725  iundisjf  31807  iundisj2f  31808  suppss2f  31850  aciunf1  31875  iundisjfi  31994  iundisj2fi  31995  fedgmullem2  32703  sigapildsys  33148  vvdifopab  37116  compab  43186  iunconnlem2  43681  supminfxr2  44165  stoweidlem28  44730  stoweidlem34  44736  stoweidlem46  44748  stoweidlem53  44755  stoweidlem55  44757  stoweidlem59  44761  stirlinglem5  44780  preimagelt  45401  preimalegt  45402