ChangeVariableAbstraction Show Code edit
thm (ChangeVariableAbstraction
((φx y result element) (φy x result element))
(
HEXISTX (∃ result (∀ element (↔ (∈ element result) (subst element x φx))))
HEXISTY (∃ result (∀ element (↔ (∈ element result) (subst element y φy))))
HSUB (→ (= x y) (↔ φx φy))
)
(= (abstract x φx) (abstract y φy))
HEXISTX
(∃ result (∀ element (↔ (∈ element result) (subst element x φx))))
Abstraction
(↔ (∈ element (abstract x φx)) (subst element x φx))
HSUB
(→ (= x y) (↔ φx φy))
element ChangeVariableSubstitution
(↔ (subst element x φx) (subst element y φy))
applyBiconditionalTransitivity
(↔ (∈ element (abstract x φx)) (subst element y φy))
HEXISTY
(∃ result (∀ element (↔ (∈ element result) (subst element y φy))))
Abstraction
(↔ (∈ element (abstract y φy)) (subst element y φy))
swapBiconditional
(↔ (subst element y φy) (∈ element (abstract y φy)))
applyBiconditionalTransitivity
(↔ (∈ element (abstract x φx)) (∈ element (abstract y φy)))
applyExtensionality
(= (abstract x φx) (abstract y φy))
)
edit