SetVariable Show Code edit
thm (SetVariable
((φz y result) (φy z))
(HSUBZ (→ (= z y) (↔ φz φy)) HEXISTS (∃ result (∀ y (↔ (∈ y result) φy))))
(↔ (∈ y (abstract z φz)) φy)
HEXISTS
(∃ result (∀ y (↔ (∈ y result) φy)))
# The first step is <code>[y / z]φz ↔ φy</code>.
HSUBZ
(→ (= z y) (↔ φz φy))
makeSubstExplicit
(↔ (subst y z φz) φy)
# We now apply builders to get <code>∃ result ∀ y (y ∈ result ↔ [y / z]φz) ↔ ∃ result ∀ y (y ∈ result ↔ φy)</code>
(∈ y result) buildBiconditionalLL
(↔ (↔ (∈ y result) (subst y z φz)) (↔ (∈ y result) φy))
y buildForAll
(↔ (∀ y (↔ (∈ y result) (subst y z φz))) (∀ y (↔ (∈ y result) φy)))
result buildThereExists
(↔ (∃ result (∀ y (↔ (∈ y result) (subst y z φz)))) (∃ result (∀ y (↔ (∈ y result) φy))))
# The right hand side of this is just our existence theorem, though (which we had left on the proof stack), so we detach it.
eliminateBiconditionalForward
(→ (∃ result (∀ y (↔ (∈ y result) φy))) (∃ result (∀ y (↔ (∈ y result) (subst y z φz)))))
applyModusPonens
(∃ result (∀ y (↔ (∈ y result) (subst y z φz))))
# Applying <code>Abstraction</code> to <code><code>∃ result ∀ y (y ∈ result ↔ [y / z]φz)</code> gives <code>y ∈ {z | φz} ↔ [y / z]φz</code> and simplying the last part gives us <code>y ∈ {z | φz} ↔ φy</code>.
Abstraction
(↔ (∈ y (abstract z φz)) (subst y z φz))
HSUBZ
(→ (= z y) (↔ φz φy))
makeSubstExplicit
(↔ (subst y z φz) φy)
applyBiconditionalTransitivity
(↔ (∈ y (abstract z φz)) φy)
)
edit