NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-scan GIF version

Definition df-scan 6326
Description: Define the class of strongly Cantorian sets. Unlike general Cantorian sets, this fixes a specific mapping between x and 1x. Definition from [Holmes] p. 134. (Contributed by Scott Fenton, 19-Apr-2021.)
Assertion
Ref Expression
df-scan SCan = {x (y x {y}) V}
Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-scan
StepHypRef Expression
1 cscan 6325 . 2 class SCan
2 vy . . . . 5 setvar y
3 vx . . . . . 6 setvar x
43cv 1641 . . . . 5 class x
52cv 1641 . . . . . 6 class y
65csn 3737 . . . . 5 class {y}
72, 4, 6cmpt 5651 . . . 4 class (y x {y})
8 cvv 2859 . . . 4 class V
97, 8wcel 1710 . . 3 wff (y x {y}) V
109, 3cab 2339 . 2 class {x (y x {y}) V}
111, 10wceq 1642 1 wff SCan = {x (y x {y}) V}
Colors of variables: wff setvar class
This definition is referenced by:  elscan  6330
  Copyright terms: Public domain W3C validator