Theorem nfdif 4084

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

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   ∈ wcel 2146  Ⅎwnfc 2912   ∖ cdif 3903

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-v 3459  df-dif 3909

This theorem is used by:  nfsymdif  4210  csbdif  4488  iunxdif3  5063  boxcutc  8941  nfsup  9414  gsum2d2lem  20066  iunconn  23614  iundisj  25736  iundisj2  25737  limciun  26082  difrab2  32873  iundisjf  32963  iundisj2f  32964  suppss2f  33012  aciunf1  33037  iundisjfi  33170  iundisj2fi  33171  suppgsumssiun  33415  fedgmullem2  34043  sigapildsys  34576  vvdifopab  38947  compab  45184  iunconnlem2  45676  supminfxr2  46216  stoweidlem28  46775  stoweidlem34  46781  stoweidlem46  46793  stoweidlem53  46800  stoweidlem55  46802  stoweidlem59  46806  stirlinglem5  46825  preimagelt  47446  preimalegt  47447