Theorem nfdif 4085

Description: Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) Avoid ax-10 2176, ax-11 2192, ax-12 2213. (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 3916	. . 3 ⊢ (𝑦 ∈ (𝐴 ∖ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))
2		nfdif.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2917	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfdif.2	. . . . . 6 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2917	. . . . 5 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	5	nfn 1887	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵
7	3, 6	nfan 1929	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)
8	1, 7	nfxfr 1883	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∖ 𝐵)
9	8	nfci 2913	1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)

Syntax hints:  ¬ wn 3   ∧ wa 400   ∈ wcel 2143  Ⅎwnfc 2910   ∖ cdif 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-v 3457  df-dif 3909

This theorem is referenced by:  nfsymdif  4211  csbdif  4487  iunxdif3  5062  boxcutc  8940  nfsup  9412  gsum2d2lem  20044  iunconn  23566  iundisj  25688  iundisj2  25689  limciun  26034  difrab2  32825  iundisjf  32915  iundisj2f  32916  suppss2f  32964  aciunf1  32989  iundisjfi  33122  iundisj2fi  33123  suppgsumssiun  33373  fedgmullem2  34001  sigapildsys  34533  vvdifopab  38895  compab  45134  iunconnlem2  45626  supminfxr2  46166  stoweidlem28  46725  stoweidlem34  46731  stoweidlem46  46743  stoweidlem53  46750  stoweidlem55  46752  stoweidlem59  46756  stirlinglem5  46775  preimagelt  47396  preimalegt  47397