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

Definition df-spac 6272
Description: Define the special class generator for the disproof of the axiom of choice. Definition 6.1 of [Specker] p. 973. (Contributed by SF, 3-Mar-2015.)
Assertion
Ref Expression
df-spac Spac NC Clos1 NC NC 2cc
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-spac
StepHypRef Expression
1 cspac 6271 . 2 Spac
2 vm . . 3
3 cncs 6088 . . 3 NC
42cv 1641 . . . . 5
54csn 3737 . . . 4
6 vx . . . . . . . 8
76cv 1641 . . . . . . 7
87, 3wcel 1710 . . . . . 6 NC
9 vy . . . . . . . 8
109cv 1641 . . . . . . 7
1110, 3wcel 1710 . . . . . 6 NC
12 c2c 6094 . . . . . . . 8 2c
13 cce 6096 . . . . . . . 8 c
1412, 7, 13co 5525 . . . . . . 7 2cc
1510, 14wceq 1642 . . . . . 6 2cc
168, 11, 15w3a 934 . . . . 5 NC NC 2cc
1716, 6, 9copab 4622 . . . 4 NC NC 2cc
185, 17cclos1 5872 . . 3 Clos1 NC NC 2cc
192, 3, 18cmpt 5651 . 2 NC Clos1 NC NC 2cc
201, 19wceq 1642 1 Spac NC Clos1 NC NC 2cc
Colors of variables: wff setvar class
This definition is referenced by:  spacval  6280  fnspac  6281
  Copyright terms: Public domain W3C validator