I know that in first-order logic the following holds [see e.g. George Tourlakis, Lectures in Logic and Set Theory. Volume 2: Set Theory (2003), page 121] :
$\vdash \lnot ∃y \ ∀x \ [A(x,y) \leftrightarrow \lnot A(x,x)]$,
for any formula $A(x,y)$.
I assume that this result "transfers" to second-order logic.
A simple instance of s-o comprehension schema is:
$∃X \ ∀x \ [\varphi(x) \leftrightarrow X(x)]$
where $X$ may not occur free in $\varphi(x)$.
Thus, with $\varphi(y) := ∀x \ [A(x,y) \leftrightarrow \lnot A(x,x)]$, we get:
$\vdash ∃X \ ∀y \ [∀x \ (A(x,y) \leftrightarrow \lnot A(x,x)) \leftrightarrow X(y)]$.
May we "cook together" the two results to conclude with ?:
$\vdash ∃X \ \lnot ∃y \ X(y)$
Note : motivated also by this Wiki's talk-page.
You may do that, but I don't think it buys you anything that you don't get by letting $\varphi(y)$ be any odd contradiction such as $A(y)\land\neg A(y)$.