Theorem nfdif 3954

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 3801	. 2 ⊢ (𝐴 ∖ 𝐵) = {𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵}
2		nfdif.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
3	2	nfcri 2929	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
4	3	nfn 1902	. . 3 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵
5		nfdif.1	. . 3 ⊢ Ⅎ𝑥𝐴
6	4, 5	nfrab 3310	. 2 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵}
7	1, 6	nfcxfr 2932	1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)

Syntax hints:  ¬ wn 3   ∈ wcel 2107  Ⅎwnfc 2919  {crab 3094   ∖ cdif 3789

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-dif 3795

This theorem is referenced by:  nfsymdif  4071  iunxdif3  4842  boxcutc  8239  nfsup  8647  gsum2d2lem  18769  iunconn  21651  iundisj  23763  iundisj2  23764  limciun  24106  difrab2  29918  iundisjf  29982  iundisj2f  29983  suppss2f  30021  aciunf1  30045  iundisjfi  30133  iundisj2fi  30134  sigapildsys  30831  csbdif  33774  vvdifopab  34668  compab  39614  iunconnlem2  40118  supminfxr2  40618  stoweidlem28  41186  stoweidlem34  41192  stoweidlem46  41204  stoweidlem53  41211  stoweidlem55  41213  stoweidlem59  41217  stirlinglem5  41236  preimagelt  41853  preimalegt  41854