Theorem nfdif 4063

Description: Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) Avoid ax-10 2154, ax-11 2170, ax-12 2191. (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 3895	. . 3 ⊢ (𝑦 ∈ (𝐴 ∖ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))
2		nfdif.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2895	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfdif.2	. . . . . 6 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2895	. . . . 5 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	5	nfn 1865	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵
7	3, 6	nfan 1907	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)
8	1, 7	nfxfr 1861	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∖ 𝐵)
9	8	nfci 2891	1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)

Syntax hints:  ¬ wn 3   ∧ wa 397   ∈ wcel 2121  Ⅎwnfc 2888   ∖ cdif 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-ex 1788  df-nf 1792  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-v 3435  df-dif 3888

This theorem is referenced by:  nfsymdif  4188  csbdif  4456  iunxdif3  5027  boxcutc  8883  nfsup  9358  gsum2d2lem  19943  iunconn  23415  iundisj  25537  iundisj2  25538  limciun  25883  difrab2  32589  iundisjf  32682  iundisj2f  32683  suppss2f  32734  aciunf1  32759  iundisjfi  32892  iundisj2fi  32893  suppgsumssiun  33157  fedgmullem2  33826  sigapildsys  34358  vvdifopab  38647  compab  44900  iunconnlem2  45393  supminfxr2  45926  stoweidlem28  46485  stoweidlem34  46491  stoweidlem46  46503  stoweidlem53  46510  stoweidlem55  46512  stoweidlem59  46516  stirlinglem5  46535  preimagelt  47156  preimalegt  47157