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 -> ( ph <-> ps ) )
Assertion	19.8aw	|- ( ph -> E. x ph )

Proof

Step	Hyp	Ref	Expression
1		19.8aw.1	|- ( x = y -> ( ph <-> ps ) )
2		alnex	|- ( A. x -. ph <-> -. E. x ph )
3	1	notbid	|- ( x = y -> ( -. ph <-> -. ps ) )
4	3	spw	|- ( A. x -. ph -> -. ph )
5	2 4	sylbir	|- ( -. E. x ph -> -. ph )
6	5	con4i	|- ( ph -> E. x ph )