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

Theorem nfdif 3470
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 3331 . 2  |-  ( A 
\  B )  =  { y  e.  A  |  -.  y  e.  B }
2 nfdif.2 . . . . 5  |-  F/_ x B
32nfcri 2568 . . . 4  |-  F/ x  y  e.  B
43nfn 1812 . . 3  |-  F/ x  -.  y  e.  B
5 nfdif.1 . . 3  |-  F/_ x A
64, 5nfrab 2891 . 2  |-  F/_ x { y  e.  A  |  -.  y  e.  B }
71, 6nfcxfr 2571 1  |-  F/_ x
( A  \  B
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    e. wcel 1726   F/_wnfc 2561   {crab 2711    \ cdif 3319
This theorem is referenced by:  boxcutc  7108  nfsup  7459  gsum2d2lem  15552  iuncon  17496  iundisj  19447  iundisj2  19448  limciun  19786  iundisjf  24034  iundisj2f  24035  suppss2f  24054  iundisjfi  24157  iundisj2fi  24158  nfsymdif  25672  dvtanlem  26268  compab  27634  stoweidlem28  27767  stoweidlem34  27773  stoweidlem46  27785  stoweidlem53  27792  stoweidlem55  27794  stoweidlem59  27798  stirlinglem5  27817  iunconlem2  29121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-dif 3325
  Copyright terms: Public domain W3C validator