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

Theorem nfdif 4121
Description: Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) Avoid ax-10 2129, ax-11 2146, ax-12 2166. (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 3954 . . 3 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴 ∧ ¬ 𝑦𝐵))
2 nfdif.1 . . . . 5 𝑥𝐴
32nfcri 2882 . . . 4 𝑥 𝑦𝐴
4 nfdif.2 . . . . . 6 𝑥𝐵
54nfcri 2882 . . . . 5 𝑥 𝑦𝐵
65nfn 1852 . . . 4 𝑥 ¬ 𝑦𝐵
73, 6nfan 1894 . . 3 𝑥(𝑦𝐴 ∧ ¬ 𝑦𝐵)
81, 7nfxfr 1847 . 2 𝑥 𝑦 ∈ (𝐴𝐵)
98nfci 2878 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 394  wcel 2098  wnfc 2875  cdif 3941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-v 3463  df-dif 3947
This theorem is referenced by:  nfsymdif  4245  csbdif  4529  iunxdif3  5099  boxcutc  8960  nfsup  9476  gsum2d2lem  19940  iunconn  23376  iundisj  25521  iundisj2  25522  limciun  25867  difrab2  32374  iundisjf  32458  iundisj2f  32459  suppss2f  32505  aciunf1  32530  iundisjfi  32646  iundisj2fi  32647  fedgmullem2  33459  sigapildsys  33912  vvdifopab  37862  compab  44021  iunconnlem2  44516  supminfxr2  44989  stoweidlem28  45554  stoweidlem34  45560  stoweidlem46  45572  stoweidlem53  45579  stoweidlem55  45581  stoweidlem59  45585  stirlinglem5  45604  preimagelt  46225  preimalegt  46226
  Copyright terms: Public domain W3C validator