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

Theorem nfdif 3709
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 𝑥𝐴
nfdif.2 𝑥𝐵
Assertion
Ref Expression
nfdif 𝑥(𝐴𝐵)

Proof of Theorem nfdif
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dfdif2 3564 . 2 (𝐴𝐵) = {𝑦𝐴 ∣ ¬ 𝑦𝐵}
2 nfdif.2 . . . . 5 𝑥𝐵
32nfcri 2755 . . . 4 𝑥 𝑦𝐵
43nfn 1781 . . 3 𝑥 ¬ 𝑦𝐵
5 nfdif.1 . . 3 𝑥𝐴
64, 5nfrab 3112 . 2 𝑥{𝑦𝐴 ∣ ¬ 𝑦𝐵}
71, 6nfcxfr 2759 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 1987  wnfc 2748  {crab 2911  cdif 3552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-dif 3558
This theorem is referenced by:  nfsymdif  3826  iunxdif3  4572  boxcutc  7895  nfsup  8301  gsum2d2lem  18293  iunconn  21141  iundisj  23223  iundisj2  23224  limciun  23564  iundisjf  29244  iundisj2f  29245  suppss2f  29278  aciunf1  29302  iundisjfi  29393  iundisj2fi  29394  sigapildsys  30003  csbdif  32800  compab  38124  iunconnlem2  38651  stoweidlem28  39549  stoweidlem34  39555  stoweidlem46  39567  stoweidlem53  39574  stoweidlem55  39576  stoweidlem59  39580  stirlinglem5  39599  preimagelt  40216  preimalegt  40217
  Copyright terms: Public domain W3C validator