Theorem nfdif 4067

Description: Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) Avoid ax-10 2152, ax-11 2168, ax-12 2189. (Revised by SN, 14-May-2025.)

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		eldif 3900	. . 3 ⊢ (𝑦 ∈ (𝐴 ∖ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))
2		nfdif.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2894	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfdif.2	. . . . . 6 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2894	. . . . 5 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	5	nfn 1864	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵
7	3, 6	nfan 1906	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)
8	1, 7	nfxfr 1860	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∖ 𝐵)
9	8	nfci 2890	1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)

Syntax hints:  ¬ wn 3   ∧ wa 396   ∈ wcel 2119  Ⅎwnfc 2887   ∖ cdif 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-v 3434  df-dif 3893

This theorem is referenced by:  nfsymdif  4192  csbdif  4460  iunxdif3  5031  boxcutc  8886  nfsup  9361  gsum2d2lem  19946  iunconn  23418  iundisj  25540  iundisj2  25541  limciun  25886  difrab2  32592  iundisjf  32685  iundisj2f  32686  suppss2f  32737  aciunf1  32762  iundisjfi  32895  iundisj2fi  32896  suppgsumssiun  33160  fedgmullem2  33821  sigapildsys  34353  vvdifopab  38639  compab  44892  iunconnlem2  45385  supminfxr2  45919  stoweidlem28  46478  stoweidlem34  46484  stoweidlem46  46496  stoweidlem53  46503  stoweidlem55  46505  stoweidlem59  46509  stirlinglem5  46528  preimagelt  47149  preimalegt  47150