SeparationThereExistsSubst Show Code edit
thm (SeparationThereExistsSubst
((φ result) (A y result)) ()
(∃ result (∀ y (↔ (∈ y result) (∧ (∈ y A) (subst y x φ)))))
result y A (subst y x φ) SeparationThereExistsObject
(∃ result (∀ y (↔ (∈ y result) (∧ (∈ y A) (subst y x φ)))))
)
edit