Detailed syntax breakdown of Axiom ax-bj-bun
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | vt |
. . . . . . 7
setvar 𝑡 |
| 2 | | vz |
. . . . . . 7
setvar 𝑧 |
| 3 | 1, 2 | wel 2109 |
. . . . . 6
wff 𝑡 ∈ 𝑧 |
| 4 | | vx |
. . . . . . . 8
setvar 𝑥 |
| 5 | 1, 4 | wel 2109 |
. . . . . . 7
wff 𝑡 ∈ 𝑥 |
| 6 | | vy |
. . . . . . . 8
setvar 𝑦 |
| 7 | 1, 6 | wel 2109 |
. . . . . . 7
wff 𝑡 ∈ 𝑦 |
| 8 | 5, 7 | wo 848 |
. . . . . 6
wff (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦) |
| 9 | 3, 8 | wb 206 |
. . . . 5
wff (𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦)) |
| 10 | 9, 1 | wal 1538 |
. . . 4
wff
∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦)) |
| 11 | 10, 2 | wex 1779 |
. . 3
wff
∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦)) |
| 12 | 11, 6 | wal 1538 |
. 2
wff
∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦)) |
| 13 | 12, 4 | wal 1538 |
1
wff
∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦)) |
