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

Theorem nfdif 4045
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 3880 . 2 (𝐴𝐵) = {𝑦𝐴 ∣ ¬ 𝑦𝐵}
2 nfdif.2 . . . . 5 𝑥𝐵
32nfcri 2891 . . . 4 𝑥 𝑦𝐵
43nfn 1865 . . 3 𝑥 ¬ 𝑦𝐵
5 nfdif.1 . . 3 𝑥𝐴
64, 5nfrabw 3302 . 2 𝑥{𝑦𝐴 ∣ ¬ 𝑦𝐵}
71, 6nfcxfr 2902 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2110  wnfc 2884  {crab 3065  cdif 3868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-rab 3070  df-dif 3874
This theorem is referenced by:  nfsymdif  4166  iunxdif3  5008  boxcutc  8627  nfsup  9072  gsum2d2lem  19363  iunconn  22330  iundisj  24450  iundisj2  24451  limciun  24796  difrab2  30569  iundisjf  30652  iundisj2f  30653  suppss2f  30698  aciunf1  30725  iundisjfi  30842  iundisj2fi  30843  fedgmullem2  31430  sigapildsys  31847  csbdif  35238  vvdifopab  36141  compab  41741  iunconnlem2  42236  supminfxr2  42692  stoweidlem28  43252  stoweidlem34  43258  stoweidlem46  43270  stoweidlem53  43277  stoweidlem55  43279  stoweidlem59  43283  stirlinglem5  43302  preimagelt  43919  preimalegt  43920
  Copyright terms: Public domain W3C validator