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

Theorem nfdif 3764
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 3616 . 2 (𝐴𝐵) = {𝑦𝐴 ∣ ¬ 𝑦𝐵}
2 nfdif.2 . . . . 5 𝑥𝐵
32nfcri 2787 . . . 4 𝑥 𝑦𝐵
43nfn 1824 . . 3 𝑥 ¬ 𝑦𝐵
5 nfdif.1 . . 3 𝑥𝐴
64, 5nfrab 3153 . 2 𝑥{𝑦𝐴 ∣ ¬ 𝑦𝐵}
71, 6nfcxfr 2791 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2030  wnfc 2780  {crab 2945  cdif 3604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-dif 3610
This theorem is referenced by:  nfsymdif  3881  iunxdif3  4638  boxcutc  7993  nfsup  8398  gsum2d2lem  18418  iunconn  21279  iundisj  23362  iundisj2  23363  limciun  23703  difrab2  29465  iundisjf  29528  iundisj2f  29529  suppss2f  29567  aciunf1  29591  iundisjfi  29683  iundisj2fi  29684  sigapildsys  30353  csbdif  33301  vvdifopab  34165  compab  38962  iunconnlem2  39485  supminfxr2  40012  stoweidlem28  40563  stoweidlem34  40569  stoweidlem46  40581  stoweidlem53  40588  stoweidlem55  40590  stoweidlem59  40594  stirlinglem5  40613  preimagelt  41233  preimalegt  41234
  Copyright terms: Public domain W3C validator