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

Theorem nfdif 3384
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 3247 . 2  |-  ( A 
\  B )  =  { y  e.  A  |  -.  y  e.  B }
2 nfdif.2 . . . . 5  |-  F/_ x B
32nfcri 2496 . . . 4  |-  F/ x  y  e.  B
43nfn 1799 . . 3  |-  F/ x  -.  y  e.  B
5 nfdif.1 . . 3  |-  F/_ x A
64, 5nfrab 2806 . 2  |-  F/_ x { y  e.  A  |  -.  y  e.  B }
71, 6nfcxfr 2499 1  |-  F/_ x
( A  \  B
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    e. wcel 1715   F/_wnfc 2489   {crab 2632    \ cdif 3235
This theorem is referenced by:  boxcutc  7002  nfsup  7349  gsum2d2lem  15434  iuncon  17371  iundisj  19120  iundisj2  19121  limciun  19459  iundisjf  23426  iundisj2f  23427  suppss2f  23452  iundisjfi  23555  iundisj2fi  23556  nfsymdif  25107  compab  27150  stoweidlem28  27283  stoweidlem34  27289  stoweidlem46  27301  stoweidlem53  27308  stoweidlem55  27310  stoweidlem59  27314  stirlinglem5  27333
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rab 2637  df-dif 3241
  Copyright terms: Public domain W3C validator