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 2914	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfdif.2	. . . . . 6 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2914	. . . . 5 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	5	nfn 1890	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵
7	3, 6	nfan 1932	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)
8	1, 7	nfxfr 1886	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∖ 𝐵)
9	8	nfci 2910	1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   ∈ wcel 2145  Ⅎwnfc 2907   ∖ 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 2732

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 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-v 3452  df-dif 3902

This theorem is used by:  nfsymdif  4203  csbdif  4481  iunxdif3  5055  boxcutc  8948  nfsup  9421  gsum2d2lem  20100  iunconn  23653  iundisj  25776  iundisj2  25777  limciun  26121  difrab2  32973  iundisjf  33062  iundisj2f  33063  suppss2f  33111  aciunf1  33136  iundisjfi  33267  iundisj2fi  33268  suppgsumssiun  33512  fedgmullem2  34140  sigapildsys  34673  vvdifopab  39013  compab  45265  iunconnlem2  45757  supminfxr2  46297  stoweidlem28  46856  stoweidlem34  46862  stoweidlem46  46874  stoweidlem53  46881  stoweidlem55  46883  stoweidlem59  46887  stirlinglem5  46906  preimagelt  47527  preimalegt  47528