Theorem nfdif 4104

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 3947	. 2 ⊢ (𝐴 ∖ 𝐵) = {𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵}
2		nfdif.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
3	2	nfcri 2973	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
4	3	nfn 1857	. . 3 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵
5		nfdif.1	. . 3 ⊢ Ⅎ𝑥𝐴
6	4, 5	nfrabw 3387	. 2 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵}
7	1, 6	nfcxfr 2977	1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)

Syntax hints:  ¬ wn 3   ∈ wcel 2114  Ⅎwnfc 2963  {crab 3144   ∖ cdif 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-dif 3941

This theorem is referenced by:  nfsymdif  4225  iunxdif3  5019  boxcutc  8507  nfsup  8917  gsum2d2lem  19095  iunconn  22038  iundisj  24151  iundisj2  24152  limciun  24494  difrab2  30263  iundisjf  30341  iundisj2f  30342  suppss2f  30386  aciunf1  30410  iundisjfi  30521  iundisj2fi  30522  fedgmullem2  31028  sigapildsys  31423  csbdif  34608  vvdifopab  35523  compab  40781  iunconnlem2  41276  supminfxr2  41752  stoweidlem28  42320  stoweidlem34  42326  stoweidlem46  42338  stoweidlem53  42345  stoweidlem55  42347  stoweidlem59  42351  stirlinglem5  42370  preimagelt  42987  preimalegt  42988