Detailed syntax breakdown of Axiom ax-1c
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)) |