Theorem nfdif 4066

Description: Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) Avoid ax-10 2177, ax-11 2193, ax-12 2212. (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 4049	. . 3 ⊢ (𝑦 ∈ (𝐴 ∖ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))
2		nfdif.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2914	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfdif.2	. . . . . 6 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2914	. . . . 5 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	5	nfn 1889	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵
7	3, 6	nfan 1931	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)
8	1, 7	nfxfr 1885	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∖ 𝐵)
9	8	nfci 2910	1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   ∈ wcel 2144  Ⅎwnfc 2907   ∖ cdif 4045

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-v 3452  df-dif 4047

This theorem is used by:  nfsymdif  4202  csbdif  4480  iunxdif3  5054  boxcutc  8973  nfsup  9447  gsum2d2lem  20193  iunconn  23752  iundisj  25875  iundisj2  25876  limciun  26220  difrab2  33142  iundisjf  33231  iundisj2f  33232  suppss2f  33280  aciunf1  33305  iundisjfi  33435  iundisj2fi  33436  suppgsumssiun  33680  fedgmullem2  34309  sigapildsys  34842  vvdifopab  39291  compab  45519  iunconnlem2  46011  supminfxr2  46573  stoweidlem28  47132  stoweidlem34  47138  stoweidlem46  47150  stoweidlem53  47157  stoweidlem55  47159  stoweidlem59  47163  stirlinglem5  47182  preimagelt  47803  preimalegt  47804