Theorem 19.8aw

Description: If a wff is true, it is true for at least one instance. This is to 19.8a what spw is to sp . (Contributed by SN, 26-Sep-2024)

	Ref	Expression
Hypothesis	19.8aw.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	19.8aw	$$⊢\phi \to \exists x\phi$$

Proof

Step	Hyp	Ref	Expression
1		19.8aw.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		alnex	$$⊢\forall x\neg \phi \leftrightarrow \neg \exists x\phi$$
3	1	notbid	$$⊢x=y\to \left(\neg \phi \leftrightarrow \neg \psi \right)$$
4	3	spw	$$⊢\forall x\neg \phi \to \neg \phi$$
5	2 4	sylbir	$$⊢\neg \exists x\phi \to \neg \phi$$
6	5	con4i	$$⊢\phi \to \exists x\phi$$