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

Theorem nfdif 3625
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 3485 . 2  |-  ( A 
\  B )  =  { y  e.  A  |  -.  y  e.  B }
2 nfdif.2 . . . . 5  |-  F/_ x B
32nfcri 2622 . . . 4  |-  F/ x  y  e.  B
43nfn 1849 . . 3  |-  F/ x  -.  y  e.  B
5 nfdif.1 . . 3  |-  F/_ x A
64, 5nfrab 3043 . 2  |-  F/_ x { y  e.  A  |  -.  y  e.  B }
71, 6nfcxfr 2627 1  |-  F/_ x
( A  \  B
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    e. wcel 1767   F/_wnfc 2615   {crab 2818    \ cdif 3473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-dif 3479
This theorem is referenced by:  boxcutc  7509  nfsup  7907  gsum2d2lem  16789  iuncon  19692  iundisj  21690  iundisj2  21691  limciun  22030  iundisjf  27118  iundisj2f  27119  suppss2f  27147  iundisjfi  27266  iundisj2fi  27267  nfsymdif  29046  dvtanlem  29639  compab  30928  stoweidlem28  31328  stoweidlem34  31334  stoweidlem46  31346  stoweidlem53  31353  stoweidlem55  31355  stoweidlem59  31359  stirlinglem5  31378  iunconlem2  32815
  Copyright terms: Public domain W3C validator