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

Theorem nfdif 3297
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 3161 . 2  |-  ( A 
\  B )  =  { y  e.  A  |  -.  y  e.  B }
2 nfdif.2 . . . . 5  |-  F/_ x B
32nfcri 2413 . . . 4  |-  F/ x  y  e.  B
43nfn 1765 . . 3  |-  F/ x  -.  y  e.  B
5 nfdif.1 . . 3  |-  F/_ x A
64, 5nfrab 2721 . 2  |-  F/_ x { y  e.  A  |  -.  y  e.  B }
71, 6nfcxfr 2416 1  |-  F/_ x
( A  \  B
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    e. wcel 1684   F/_wnfc 2406   {crab 2547    \ cdif 3149
This theorem is referenced by:  boxcutc  6859  nfsup  7202  gsum2d2lem  15224  iuncon  17154  iundisj  18905  iundisj2  18906  limciun  19244  suppss2f  23201  iundisjfi  23363  iundisj2fi  23364  iundisjf  23365  iundisj2f  23366  nfsymdif  24366  compab  27644  stoweidlem28  27777  stoweidlem34  27783  stoweidlem46  27795  stoweidlem53  27802  stoweidlem55  27804  stoweidlem59  27808  stirlinglem5  27827
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-dif 3155
  Copyright terms: Public domain W3C validator