Theorem nfdif 4077

Description: Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) Avoid ax-10 2178, ax-11 2194, 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 3909	. . 3 ⊢ (𝑦 ∈ (𝐴 ∖ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))
2		nfdif.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2915	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfdif.2	. . . . . 6 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2915	. . . . 5 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	5	nfn 1890	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵
7	3, 6	nfan 1932	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)
8	1, 7	nfxfr 1886	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∖ 𝐵)
9	8	nfci 2911	1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   ∈ wcel 2145  Ⅎwnfc 2908   ∖ cdif 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-v 3453  df-dif 3902

This theorem is used by:  nfsymdif  4203  csbdif  4481  iunxdif3  5055  boxcutc  8962  nfsup  9436  gsum2d2lem  20180  iunconn  23739  iundisj  25862  iundisj2  25863  limciun  26207  difrab2  33087  iundisjf  33176  iundisj2f  33177  suppss2f  33225  aciunf1  33250  iundisjfi  33381  iundisj2fi  33382  suppgsumssiun  33626  fedgmullem2  34255  sigapildsys  34788  vvdifopab  39177  compab  45410  iunconnlem2  45902  supminfxr2  46448  stoweidlem28  47007  stoweidlem34  47013  stoweidlem46  47025  stoweidlem53  47032  stoweidlem55  47034  stoweidlem59  47038  stirlinglem5  47057  preimagelt  47678  preimalegt  47679