Theorem nfdif 4064

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 3900	. 2 ⊢ (𝐴 ∖ 𝐵) = {𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵}
2		nfdif.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
3	2	nfcri 2895	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
4	3	nfn 1863	. . 3 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵
5		nfdif.1	. . 3 ⊢ Ⅎ𝑥𝐴
6	4, 5	nfrabw 3316	. 2 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵}
7	1, 6	nfcxfr 2906	1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)

Syntax hints:  ¬ wn 3   ∈ wcel 2109  Ⅎwnfc 2888  {crab 3069   ∖ cdif 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-nf 1790  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-rab 3074  df-dif 3894

This theorem is referenced by:  nfsymdif  4185  csbdif  4463  iunxdif3  5028  boxcutc  8703  nfsup  9171  gsum2d2lem  19555  iunconn  22560  iundisj  24693  iundisj2  24694  limciun  25039  difrab2  30824  iundisjf  30907  iundisj2f  30908  suppss2f  30953  aciunf1  30979  iundisjfi  31096  iundisj2fi  31097  fedgmullem2  31690  sigapildsys  32109  vvdifopab  36378  compab  42013  iunconnlem2  42508  supminfxr2  42963  stoweidlem28  43523  stoweidlem34  43529  stoweidlem46  43541  stoweidlem53  43548  stoweidlem55  43550  stoweidlem59  43554  stirlinglem5  43573  preimagelt  44190  preimalegt  44191