MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfdif Structured version   Unicode version

Theorem nfdif 3572
Description: Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.)
Hypotheses
Ref Expression
nfdif.1  |-  F/_ x A
nfdif.2  |-  F/_ x B
Assertion
Ref Expression
nfdif  |-  F/_ x
( A  \  B
)

Proof of Theorem nfdif
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dfdif2 3432 . 2  |-  ( A 
\  B )  =  { y  e.  A  |  -.  y  e.  B }
2 nfdif.2 . . . . 5  |-  F/_ x B
32nfcri 2604 . . . 4  |-  F/ x  y  e.  B
43nfn 1837 . . 3  |-  F/ x  -.  y  e.  B
5 nfdif.1 . . 3  |-  F/_ x A
64, 5nfrab 2995 . 2  |-  F/_ x { y  e.  A  |  -.  y  e.  B }
71, 6nfcxfr 2609 1  |-  F/_ x
( A  \  B
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    e. wcel 1758   F/_wnfc 2597   {crab 2797    \ cdif 3420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2599  df-rab 2802  df-dif 3426
This theorem is referenced by:  boxcutc  7403  nfsup  7799  gsum2d2lem  16567  iuncon  19145  iundisj  21142  iundisj2  21143  limciun  21482  iundisjf  26062  iundisj2f  26063  suppss2f  26085  iundisjfi  26211  iundisj2fi  26212  nfsymdif  27984  dvtanlem  28576  compab  29832  stoweidlem28  29958  stoweidlem34  29964  stoweidlem46  29976  stoweidlem53  29983  stoweidlem55  29985  stoweidlem59  29989  stirlinglem5  30008  iunconlem2  31968
  Copyright terms: Public domain W3C validator