NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-nin GIF 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 (AB) = {x (x A x B)}
Distinct variable groups:   x,A   x,B

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