Theorem 19.2g

Theorem 19.2 of [Margaris] p. 89, generalized to use two setvar variables. Use 19.2 when sufficient. (Contributed by Mel L. O'Cat, 31-Mar-2008.)

Conclusion
\( \vdash \forall x \, \varphi \rightarrow \exists y \, \varphi \)
Proof
19.8a
sps _