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

Theorem nfdif 4086
Description: Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) Avoid ax-10 2178, ax-11 2194, ax-12 2215. (Revised by SN, 14-May-2025.)
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 eldif 3917 . . 3 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴 ∧ ¬ 𝑦𝐵))
2 nfdif.1 . . . . 5 𝑥𝐴
32nfcri 2919 . . . 4 𝑥 𝑦𝐴
4 nfdif.2 . . . . . 6 𝑥𝐵
54nfcri 2919 . . . . 5 𝑥 𝑦𝐵
65nfn 1880 . . . 4 𝑥 ¬ 𝑦𝐵
73, 6nfan 1922 . . 3 𝑥(𝑦𝐴 ∧ ¬ 𝑦𝐵)
81, 7nfxfr 1876 . 2 𝑥 𝑦 ∈ (𝐴𝐵)
98nfci 2915 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 400  wcel 2145  wnfc 2912  cdif 3904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737
This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-v 3459  df-dif 3910
This theorem is referenced by:  nfsymdif  4212  csbdif  4482  iunxdif3  5056  boxcutc  8927  nfsup  9399  gsum2d2lem  20031  iunconn  23542  iundisj  25664  iundisj2  25665  limciun  26010  difrab2  32750  iundisjf  32840  iundisj2f  32841  suppss2f  32891  aciunf1  32916  iundisjfi  33049  iundisj2fi  33050  suppgsumssiun  33300  fedgmullem2  33932  sigapildsys  34464  vvdifopab  38771  compab  45010  iunconnlem2  45502  supminfxr2  46042  stoweidlem28  46601  stoweidlem34  46607  stoweidlem46  46619  stoweidlem53  46626  stoweidlem55  46628  stoweidlem59  46632  stirlinglem5  46651  preimagelt  47272  preimalegt  47273
  Copyright terms: Public domain W3C validator