Theorem 19.9t

Closed form of 19.9 and version of 19.3t with an existential quantifier. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 14-Jul-2020.)

Conclusion
\( \vdash \Finv x \, \varphi \rightarrow (\exists x \, \varphi \leftrightarrow \varphi) \)
Proof
id
l1
19.9d _
19.8a
impbid1 l1 _