NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-nin Structured version   Unicode version

Definition df-nin 3211
Description: Define the anti-intersection of two classes. This operation is used implicitly after Axiom P1 of [Hailperin] p. 6, though there does not seem to be any notation for it in the literature. (Contributed by SF, 10-Jan-2015.)
Assertion
Ref Expression
df-nin &ncap
Distinct variable groups:   ,   ,

Detailed syntax breakdown of Definition df-nin
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cnin 3204 . 2 &ncap
4 vx . . . . . 6
54cv 1641 . . . . 5
65, 1wcel 1710 . . . 4
75, 2wcel 1710 . . . 4
86, 7wnan 1287 . . 3
98, 4cab 2339 . 2
103, 9wceq 1642 1 &ncap
Colors of variables: wff set class
This definition is referenced by:  elning  3217  nfnin  3228  nineq1  3234
  Copyright terms: Public domain W3C validator