Theorem nfdif 4138

Description: Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) Avoid ax-10 2138, ax-11 2154, ax-12 2174. (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 3972	. . 3 ⊢ (𝑦 ∈ (𝐴 ∖ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))
2		nfdif.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2894	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfdif.2	. . . . . 6 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2894	. . . . 5 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	5	nfn 1854	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵
7	3, 6	nfan 1896	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)
8	1, 7	nfxfr 1849	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∖ 𝐵)
9	8	nfci 2890	1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)

Syntax hints:  ¬ wn 3   ∧ wa 395   ∈ wcel 2105  Ⅎwnfc 2887   ∖ cdif 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-v 3479  df-dif 3965

This theorem is referenced by:  nfsymdif  4262  csbdif  4529  iunxdif3  5099  boxcutc  8979  nfsup  9488  gsum2d2lem  20005  iunconn  23451  iundisj  25596  iundisj2  25597  limciun  25943  difrab2  32525  iundisjf  32608  iundisj2f  32609  suppss2f  32654  aciunf1  32679  iundisjfi  32803  iundisj2fi  32804  fedgmullem2  33657  sigapildsys  34142  vvdifopab  38241  compab  44437  iunconnlem2  44932  supminfxr2  45418  stoweidlem28  45983  stoweidlem34  45989  stoweidlem46  46001  stoweidlem53  46008  stoweidlem55  46010  stoweidlem59  46014  stirlinglem5  46033  preimagelt  46654  preimalegt  46655