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

Theorem nfdif 3428
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 3289 . 2  |-  ( A 
\  B )  =  { y  e.  A  |  -.  y  e.  B }
2 nfdif.2 . . . . 5  |-  F/_ x B
32nfcri 2534 . . . 4  |-  F/ x  y  e.  B
43nfn 1807 . . 3  |-  F/ x  -.  y  e.  B
5 nfdif.1 . . 3  |-  F/_ x A
64, 5nfrab 2849 . 2  |-  F/_ x { y  e.  A  |  -.  y  e.  B }
71, 6nfcxfr 2537 1  |-  F/_ x
( A  \  B
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    e. wcel 1721   F/_wnfc 2527   {crab 2670    \ cdif 3277
This theorem is referenced by:  boxcutc  7064  nfsup  7412  gsum2d2lem  15502  iuncon  17444  iundisj  19395  iundisj2  19396  limciun  19734  iundisjf  23982  iundisj2f  23983  suppss2f  24002  iundisjfi  24105  iundisj2fi  24106  nfsymdif  25580  compab  27511  stoweidlem28  27644  stoweidlem34  27650  stoweidlem46  27662  stoweidlem53  27669  stoweidlem55  27671  stoweidlem59  27675  stirlinglem5  27694
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-dif 3283
  Copyright terms: Public domain W3C validator