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

Theorem nfdif 3954
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 3801 . 2 (𝐴𝐵) = {𝑦𝐴 ∣ ¬ 𝑦𝐵}
2 nfdif.2 . . . . 5 𝑥𝐵
32nfcri 2929 . . . 4 𝑥 𝑦𝐵
43nfn 1902 . . 3 𝑥 ¬ 𝑦𝐵
5 nfdif.1 . . 3 𝑥𝐴
64, 5nfrab 3310 . 2 𝑥{𝑦𝐴 ∣ ¬ 𝑦𝐵}
71, 6nfcxfr 2932 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2107  wnfc 2919  {crab 3094  cdif 3789
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-dif 3795
This theorem is referenced by:  nfsymdif  4071  iunxdif3  4842  boxcutc  8239  nfsup  8647  gsum2d2lem  18769  iunconn  21651  iundisj  23763  iundisj2  23764  limciun  24106  difrab2  29918  iundisjf  29982  iundisj2f  29983  suppss2f  30021  aciunf1  30045  iundisjfi  30133  iundisj2fi  30134  sigapildsys  30831  csbdif  33774  vvdifopab  34668  compab  39614  iunconnlem2  40118  supminfxr2  40618  stoweidlem28  41186  stoweidlem34  41192  stoweidlem46  41204  stoweidlem53  41211  stoweidlem55  41213  stoweidlem59  41217  stirlinglem5  41236  preimagelt  41853  preimalegt  41854
  Copyright terms: Public domain W3C validator