Theorem nfdif 4066

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 3901	. 2 ⊢ (𝐴 ∖ 𝐵) = {𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵}
2		nfdif.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
3	2	nfcri 2892	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
4	3	nfn 1858	. . 3 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵
5		nfdif.1	. . 3 ⊢ Ⅎ𝑥𝐴
6	4, 5	nfrabw 3330	. 2 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵}
7	1, 6	nfcxfr 2903	1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)

Syntax hints:  ¬ wn 3   ∈ wcel 2104  Ⅎwnfc 2885  {crab 3284   ∖ cdif 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-rab 3287  df-dif 3895

This theorem is referenced by:  nfsymdif  4186  csbdif  4464  iunxdif3  5031  boxcutc  8760  nfsup  9254  gsum2d2lem  19619  iunconn  22624  iundisj  24757  iundisj2  24758  limciun  25103  difrab2  30890  iundisjf  30973  iundisj2f  30974  suppss2f  31019  aciunf1  31045  iundisjfi  31162  iundisj2fi  31163  fedgmullem2  31756  sigapildsys  32175  vvdifopab  36442  compab  42098  iunconnlem2  42593  supminfxr2  43057  stoweidlem28  43618  stoweidlem34  43624  stoweidlem46  43636  stoweidlem53  43643  stoweidlem55  43645  stoweidlem59  43649  stirlinglem5  43668  preimagelt  44287  preimalegt  44288