Theorem nfdif 4126

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 3958	. 2 ⊢ (𝐴 ∖ 𝐵) = {𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵}
2		nfdif.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
3	2	nfcri 2891	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
4	3	nfn 1861	. . 3 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵
5		nfdif.1	. . 3 ⊢ Ⅎ𝑥𝐴
6	4, 5	nfrabw 3469	. 2 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵}
7	1, 6	nfcxfr 2902	1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)

Syntax hints:  ¬ wn 3   ∈ wcel 2107  Ⅎwnfc 2884  {crab 3433   ∖ cdif 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-rab 3434  df-dif 3952

This theorem is referenced by:  nfsymdif  4247  csbdif  4528  iunxdif3  5099  boxcutc  8935  nfsup  9446  gsum2d2lem  19841  iunconn  22932  iundisj  25065  iundisj2  25066  limciun  25411  difrab2  31738  iundisjf  31820  iundisj2f  31821  suppss2f  31863  aciunf1  31888  iundisjfi  32007  iundisj2fi  32008  fedgmullem2  32715  sigapildsys  33160  vvdifopab  37128  compab  43201  iunconnlem2  43696  supminfxr2  44179  stoweidlem28  44744  stoweidlem34  44750  stoweidlem46  44762  stoweidlem53  44769  stoweidlem55  44771  stoweidlem59  44775  stirlinglem5  44794  preimagelt  45415  preimalegt  45416