SeparationAsAbstraction Show Code edit
defthm (SeparationAsAbstraction object (separate x A φ) ((A z) (φ z)) ()
(= (separate x A φ) (abstract z (∧ (∈ z A) (subst z x φ))))
result element z′ A x φ SeparationWithSubst
(∃ result (∀ element (↔ (∈ element result) (subst element z′ (∧ (∈ z′ A) (subst z′ x φ))))))
result element z A x φ SeparationWithSubst
(∃ result (∀ element (↔ (∈ element result) (subst element z (∧ (∈ z A) (subst z x φ))))))
z′ z A x φ Separation-sub
(→ (= z′ z) (↔ (∧ (∈ z′ A) (subst z′ x φ)) (∧ (∈ z A) (subst z x φ))))
ChangeVariableAbstraction
(= (abstract z′ (∧ (∈ z′ A) (subst z′ x φ))) (abstract z (∧ (∈ z A) (subst z x φ))))
)
edit