![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > ax-1c | GIF version |
Description: State the axiom of cardinal one. This axiom guarantees the existence of the set of all singletons, which will become cardinal one later in our development. Axiom P8 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.) |
Ref | Expression |
---|---|
ax-1c | ⊢ ∃x∀y(y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vy | . . . . 5 setvar y | |
2 | vx | . . . . 5 setvar x | |
3 | 1, 2 | wel 1711 | . . . 4 wff y ∈ x |
4 | vw | . . . . . . . 8 setvar w | |
5 | 4, 1 | wel 1711 | . . . . . . 7 wff w ∈ y |
6 | vz | . . . . . . . 8 setvar z | |
7 | 4, 6 | weq 1643 | . . . . . . 7 wff w = z |
8 | 5, 7 | wb 176 | . . . . . 6 wff (w ∈ y ↔ w = z) |
9 | 8, 4 | wal 1540 | . . . . 5 wff ∀w(w ∈ y ↔ w = z) |
10 | 9, 6 | wex 1541 | . . . 4 wff ∃z∀w(w ∈ y ↔ w = z) |
11 | 3, 10 | wb 176 | . . 3 wff (y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z)) |
12 | 11, 1 | wal 1540 | . 2 wff ∀y(y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z)) |
13 | 12, 2 | wex 1541 | 1 wff ∃x∀y(y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z)) |
Colors of variables: wff setvar class |
This axiom is referenced by: 1cex 4143 |
Copyright terms: Public domain | W3C validator |